부분식은 순방향으로, 타입(및 타입 오류)은 역방향으로 흐른다는 관점에서 STLC의 양방향 타입체커를 Haskell의 Control.Lens를 이용해 하나의 옵틱으로 구현한다. 질문-응답 프로토콜, 어플리커티브와 모나딕 트래버설의 차이, 에러 처리 전략, 그리고 파이프라인 결합까지 살펴본다.
한동안 타입 검사는 옵틱이어야 한다는 직관을 가지고 있었다. 부분식은 앞으로 흐르고, 부분식의 타입(그리고 타입 오류)은 뒤로 흐르는 식이다. 이 글에서는 Haskell의 Control.Lens를 사용해 단순형 람다 계산(STLC)의 양방향 타입체커를 하나의 옵틱으로 구현함으로써 이 아이디어를 설명해 본다.
여기 나오는 내용은 사실 타입검사, 양방향 여부와 크게 상관없다. 잘 정의된 트리 탐색 문제의 깔끔한 예시에 지나지 않으며, 제목이 재밌다는 점 말고는 특별할 게 없다. 나는 이 망치를 아주 다양한 적용처에 대해 오랫동안 저울질해 왔다. 증명 개념으로 꼭 해보고 싶은 한 가지는 비디오게임의 NPC AI 스크립팅인데, 밈으로 말하자면 “메탈 기어 솔리드는 렌즈다”이다(잠입 게임은 AI가 현실적으로 행동하는 것이 평소보다 더 중요한 장르의 한 예다).
양방향 타입검사의 출발점은 언어의 항(term)을 두 부류로 나누는 것이다. 바로 타입이 알고리즘적으로 합성(synthesis) 가능한 항과, 타입이 알고리즘적으로 검사(check) 가능한 항이다. STLC에서 변수 x는 합성 가능한 항이다. 적용 t u는 t가 합성 가능이고 u가 검사 가능할 때 합성 가능하다. 추상 λ x.t는 t가 검사 가능할 때 검사 가능하다(일부 STLC 전개와 달리, 여기서 추상된 변수 x는 타입 주석을 갖지 않는다). 또한 어떤 합성 가능한 항도 검사 가능한 것으로 간주할 수 있고, 어떤 검사 가능한 항도 타입 주석과 함께라면 합성 가능한 것으로 간주할 수 있다.
Haskell로 쓰면 별 거 없다:
data Type = TVar String | Unit | Function Type Type
deriving (Eq, Show)
data TermSyn = Var String | App TermSyn TermChk | Down Type TermChk
deriving (Show)
data TermChk = Lambda String TermChk | Up TermSyn
deriving (Show)
양방향 STLC의 규칙을 전통적인 프로그래밍 언어 표기법으로 써 보자. t가 합성 가능한 항이고 그 타입을 합성한 결과가 a라면 t∈a라고 쓴다. t가 검사 가능한 항이고 t가 타입 a임을 성공적으로 검사했다면 a∋t라고 쓴다(기호 ∋는 “니”라고 발음하며 LaTeX/MathJax에서도 그렇게 쓴다. 그래서 Conor Mc Bride의 논문 The Types Who Say Ni 제목이 그렇다). “타입 a가 항 t를 받아들인다”고도 말한다.
Γ,x:a⊢x∈a(Var)
Γ⊢t∈a→b Γ⊢a∋u Γ⊢t u∈b(App)
Γ,x:a⊢b∋t Γ⊢a→b∋λ x.t(Lam)
Γ⊢a∋t Γ⊢↓t:a∈a(Down)
Γ⊢t∈b a=b Γ⊢a∋↑t(Up)
이 모든 것을 하나의 옵틱으로 구성하려면, Blass의 고전 논문에 등장하는 아주 이른 아이디어로 돌아가야 한다. 바로 질문과 답변으로 이루어진 경계다. 우리는 옵틱에 질문을 한다. 그러면 옵틱은 반대쪽 경계로 질문을 던질 수 있고, 답을 받은 다음, 최종적으로 우리에게 답한다. 여기서 우리가 할 수 있는 질문은 “이 합성 가능한 항의 타입은 무엇인가?”와 “이 검사 가능한 항이 이 타입을 만족하는가?”이다:
type Context = [(String, Type)]
data Question = Synthesise Context TermSyn | Check Context Type TermChk
deriving (Show)
data Answer = Synthesised Type | Checked | TypeError
deriving (Show)
일단은 “타입 오류”가 추가 정보를 담지 않도록 했다. 하지만 실패 경로를 어떻게 다루는 게 최선인지에 대해서는 나중에 다시 돌아오겠다. 이 문제는 이론과 구현 사이의 긴장을 만든다.
아래는 이런 “질문-답변 프로토콜”을 Haskell에서 펑터 렌즈로 구현한 예시로, (Lam) 규칙을 보여준다:
lam :: forall f. (Functor f) => (Question -> f Answer) -> Question -> f Answer
lam k (Check ctx (Function a b) (Lambda x t)) = k (Check ((x, a) : ctx) b t)
여기서는 CPS스러운 반 라르호번(Van Laarhoven) 표현이(간만에!) 프로토콜을 그대로 반영해 주기 때문에 유용하다고 느꼈다. 우리는 렌즈에 Check ctx (Function a b) (Lambda x t)라는 질문을 한다. 렌즈는 자신의 컨티뉴에이션에 Check ((x, a) : ctx) b t라는 질문을 던진다. 답을 받은 다음, 그 답을 변경 없이 우리에게 돌려준다.
이 세미나에서 Bob Atkey에게서 배운 매우 미묘하지만 유용한 직관이 있다. 바로 렌즈의 상위 클래스들은 컨티뉴에이션에 접근할 수 있는 “양(quantity)”이 다르다는 것이다. 렌즈는 컨티뉴에이션을 정확히 한 번 호출해야 한다. 어파인 트래버설은 기껏해야 한 번까지만 호출할 수 있고, 트래버설은 유한 횟수만큼 호출할 수 있다. 반 라르호번 인코딩에서 렌즈는 최소 한 번은 컨티뉴에이션을 호출해야 한다. 그렇지 않으면 알 수 없는 펑터 f 안의 값을 얻을 수 없기 때문이다. 또한 두 번 이상 호출해서 나온 결과를 결합할 방법이 없으니, 오직 하나만 반환할 수 있다. 어파인 트래버설에서는 포인티드 펑터(pointed functor)를 쓰는데, 이는 컨티뉴에이션을 호출하지 않고도 펑터 안으로 들어갈 수 있게 해 주지만, 여전히 서로 다른 두 호출의 결과를 합칠 수는 없다. 트래버설에서는 애플리커티브(applicative)를 쓰는데, 둘 다 가능하다.
이 모든 말을 요약하면, 나는 가설이 2개인 (App) 규칙이 트래버설일 것이라고 “기대”했다는 것이다. 즉 다음과 같은 타입을 가질 거라고 말이다.
app :: forall f. (Applicative f) => (Question -> f Answer) -> Question -> f Answer
그런데 막상 작성하려고 하니 예상치 못한 미묘함이 있었다. 트래버설은 컨티뉴에이션을 여러 번 호출할 수 있지만, 그 호출들은 서로 “독립적”이어야 한다. (App) 규칙은 “t u의 타입은 무엇인가?”라는 질문에 답해야 한다. 이를 위해 먼저 “t의 타입은 무엇인가?”라고 묻고, 그 답으로 “a”를 받으면 이어서 “u는 타입 a인가?”라는 후속 질문을 한다. 즉 두 번째 질문은 첫 번째 답변에 의존한다. 이것이 바로 트래버설로는 할 수 없는 일이다.
(App) 규칙을 표현하려면 처음 보면 너무나 자명한, 트래버설의 상위 클래스처럼 보이는 타입 시그니처가 필요하다:
app :: forall f. (Monad f) => (Question -> f Answer) -> Question -> f Answer
app k (Synthesise ctx (App t u)) = do
Synthesised (Function a b) <- k (Synthesise ctx t)
Checked <- k (Check ctx a u)
return (Synthesised b)
do 블록 두 번째 줄의 a가 바로 애플리커티브로는 할 수 없는 그 무엇이다.
이 부류의 옵틱은 이름이 없는 듯하지만, 아이디어 자체는 몇몇 사람이 제안해 왔다. 나는 이미 각각 역방향이 클라이슬리 범주에 있는 렌즈와 모나oidal 옵틱 전체가 클라이슬리 범주에 있는 옵틱에 대해 “모나딕 렌즈”와 “모나딕 옵틱”이라는 용어를 쓰고 있다. Zanzi의 제안처럼 이를 “모나딕 트래버설”이라고 부르는 게 마음에 든다. 트래버설 법칙을 만족하는 비자명한 모나딕 트래버설은 없다는1 얘기도 있다. 즉 모나딕 트래버설이 법칙을 만족한다면 이미 보통의 트래버설이라는 뜻이다. 다행히도, 내 경력 대부분은 옵틱 법칙들에 침을 뱉으며 보내 왔다. 더 핵심적으로, 이런 질문-답변 옵틱은 가장 일반화된 의미로조차 “의미 있게” 합법적일 수 없다고 거의 확신한다. 왜냐하면 하나의 답이 그에 대한 표준적인 후속 질문을 결정하지 못하기 때문이다. 그럼에도 불구하고 이것들은 많은 응용에서 여전히 매우 중요하다.
나는 아래 옵틱
type MonadicTraversal s t a b = forall f. (Monad f) => (a -> f b) -> s -> f t
이 다음과 같은 구체적 구현과 동형이라고 추측한다:
type MonadicTraversal s t a b = s -> Interaction a b t
data Interaction a b t = Done t
| More a (b -> Interaction a b t)
Interaction a b t는 t 타입의 답으로 종료할 수도 있고, a 타입의 질문을 던질 수도 있다. 그리고 각 b 타입의 답마다 “연속 상호작용”을 갖는다. 이는 보통의 트래버설에서 FunList(펑터 인코딩에서는 Bazaar라고도 함)에 해당하는, 모나딕 트래버설 버전이다.
이제 모든 준비가 끝났으니, 모나딕 트래버설로 타입체커 전체를 구현해 보자:
rules :: MonadicTraversal Question Answer Question Answer
rules _ (Synthesise ctx (Var x)) = case lookup x ctx of
Just a -> return (Synthesised a)
Nothing -> return TypeError
rules k (Synthesise ctx (App t1 t2)) = k (Synthesise ctx t1) >>= \case
Synthesised (Function a b) -> k (Check ctx a t2) >>= \case
Checked -> return (Synthesised b)
_ -> return TypeError
_ -> return TypeError
rules k (Synthesise ctx (Down a t)) = k (Check ctx a t) >>= \case
Checked -> return (Synthesised a)
_ -> return TypeError
rules k (Check ctx (Function a b) (Lambda x t)) = k (Check ((x, a) : ctx) b t)
rules _ (Check _ _ (Lambda _ _)) = return TypeError
rules k (Check ctx a (Up t)) = k (Synthesise ctx t) >>= \case
Synthesised b -> if a == b then return Checked else return TypeError
_ -> return TypeError
이 옵틱은, 부분식에 대한 타입검사를 수행하는 또 다른 옵틱과 뒤에서 합성(post-compose)되면 타입검사를 구현한다. 실제 람다 항은 부분식이 유한하지만 임의의 깊이로 중첩되므로, 필요한 것은 이 옵틱을 자기 자신과 합성하고 고정점(fixpoint)을 취하는 것이다. 반 라르호번 인코딩된 옵틱은 역함수 합성으로 합성된다는 점을 기억하자:
stlc :: MonadicTraversal Question Answer Question Answer
stlc = rules . stlc
개인적으로 이 무한 합성 사슬은 우리가 벨만 반복을 옵틱 합성으로 구현했던 방식과 놀라울 만큼 비슷하다고 느낀다.
이제 표준 Control.Lens 콤비네이터를 사용해 이 렌즈를 호출하여 타입체커를 쓸 수 있다:
typecheck :: Question -> Answer
typecheck q = q & stlc .~ TypeError
그리고 잘 동작한다! 다음은 컨텍스트 x:a에서 람다 항 (λ y.y)x에 대해 실행한 모습이다:
ghci> typecheck $ Synthesise [("x", TVar "a")]
$ App (Down (Function (TVar "a") (TVar "a")) (Lambda "y" (Up (Var "y"))))
(Up (Var "x"))
Synthesised (TVar "a")
함수 typecheck에서 무한 합성 사슬의 맨 끝에 있는 역방향 입력 TypeError는 실제로 사용되지 않는다. 우리 람다 항의 부분식 깊이에 도달하기 전에 이미 반환하기 때문이다. 이를 undefined로 바꿔도 모든 것이 여전히 올바르게 동작한다. 이는 렌즈로 하는 벨만 반복과 거의 똑같다. 그 경우 역방향 입력은 임의의 실수인데, 무한히 할인되어 0이 된다.
이론적으로는 여기서 끝이지만, 실제로는 타입 오류를 매우 나쁘게 다루고 있다. 구현의 절반 정도가 타입 오류 처리이고, 그럼에도 불구하고 우리는 모든 타입 오류를 단일 값으로 붕괴시키고, 호출자에게 유용한 정보를 돌려주지 못하고 있다.
그냥 재미로, 첫 번째 문제는 해결하고 두 번째는 무시하는 아이디어를 하나 소개하겠다. Haskell이 do-표기를 desugar하는 방식을 강하게 남용하는 것이다. Prelude에는 MonadFail이라는 클래스가 있는데, 과거 호환성 때문에 존재하며, 모나드 시그니처에 fail :: String -> m a를 추가한다. Haskell은 do 블록 안의 특정 형태의 실패 가능성 있는 패턴 매치를 MonadFail로 desugar하는데, 이때 문자열에는 실패한 매치에 대한 정보가 들어간다.
모나딕 트래버설이 불편한 독자는 다음 코드 블록은 건너뛰길 권한다. 나는 지금 MonadFail을 위한 옵틱을 투입하려고 한다. 이것은 내가 Haskell에서 해 본 것 중 꽤나 무시무시한 일에 속한다.
주의할 점은 이 “기능”이 반쯤만 완성되어 있거나, 아마도 더 그럴듯하게는 반쯤만 제거된 상태라는 것이다. <-의 왼쪽에 있는 패턴 매치는 fail로 desugar되지만, let 형태의 패턴 매치는 대신 Prelude.error로 desugar된다. 따라서 이것이 동작하려면 let x = y를 x <- return y로 바꿔야 한다.
rules :: forall f. (MonadFail f) => (Question -> f Answer) -> Question -> f Answer
rules _ (Synthesise ctx (Var x)) = do
Just a <- return (lookup x ctx)
return (Synthesised a)
rules k (Synthesise ctx (App t u)) = do
Synthesised (Function a b) <- k (Synthesise ctx t)
Checked <- k (Check ctx a u)
return (Synthesised b)
rules k (Synthesise ctx (Down a t)) = do
Checked <- k (Check ctx a t)
return (Synthesised a)
rules k (Check ctx a (Lambda x t)) = do
Function b c <- return a
k (Check ((x, b) : ctx) c t)
rules k (Check ctx a (Up t)) = do
Synthesised b <- k (Synthesise ctx t)
if a == b then return Checked
else fail $ unwords ["Could not match", show a, "and", show b]
stlc :: forall f. (MonadFail f) => (Question -> f Answer) -> Question -> f Answer
stlc = rules . stlc
typecheck :: Question -> Maybe Answer
typecheck = stlc (const Nothing)
마지막 부분은 Maybe가 내장된 MonadFail 인스턴스를 가진다는 사실을 이용한다(오류 문자열을 무시한다).
실제 공학의 세계로 돌아오자면, 실패 경로를 올바르게 다루는 최선의 방법은 TypeError 타입을 정의하고(원하는 만큼 정보를 담을 수 있다), mtl의 이 클래스 Control.Monad.Except.MonadError TypeError를 위한 옵틱을 사용하는 것이라고 생각한다. 그리고 당연히, 위의 장난질 대신 명시적으로 유익한 타입 오류를 감지하고 던지는 작업을 한다. 아직 실제로 만들지는 않았다. mtl의 클래스를 위한 옵틱이 “정말로” 좋은 생각인지 확신이 서지 않기 때문이다. 하지만 아직 그보다 더 나은 아이디어도 없다.
최근 André가 컴파일러 파이프라인에 대한 글을 썼고, 같은 일을 렌즈로 하는 후속 글을 준비 중이다. 예를 들어, 타입검사는 스코프 검사에 이어지고 코드 생성이 뒤따르는, 컴파일러 파이프라인의 한 단계다.
내가 이 글에서 한 일은 여기에 스패너를 던진다. 나는 코도메인 경계에 실제로 도달하지 않는 무한 합성 사슬의 옵틱을 사용하고 있기 때문이다. 그래서 그것들을 끝에서 끝으로 합성하는 게 말이 되지 않는다.
내 직감으로는 트래버설 위에 어떤(비대칭) 모노이달 곱이 있어야 하고, 그것이 이런 식으로 정의된 것들을 시퀀싱하는 “정답”이어야 한다. 아직 찾지 못했기 때문에, 옳다고는 생각하지 않지만 동작하는 방식을 하나 보여 주겠다.
타입검사 외에도 다음과 같은 타입의 또 다른 모나딕 트래버설이 있다고 하자:
data ScopeCheckQuestion = ScopeCheckQuestion
data ScopeCheckAnswer = WellScoped | ScopeError
scopecheck :: MonadicTraversal ScopeCheckQuestion ScopeCheckAnswer
ScopeCheckQuestion ScopeCheckAnswer
스코프 검사와 타입검사 트래버설의 쌍대곱(coproduct)을 취해야 한다. 옵틱의 쌍대곱을 제대로 쓰려면 의존 타입이 필요하지만, Haskell에서 우리가 쓸 수 있는 가장 가까운 것은 타입이 걸러주지 못하는 실패 가능 패턴 매치를 포함한 다음 형태다:
plus :: (Functor f)
=> ((a -> f b) -> s -> f t) -> ((a' -> f b') -> s' -> f t')
-> (Either a a' -> f (Either b b') -> Either s s' -> f (Either t t'))
plus l _ k (Left s) = Left <$> l (\a -> fmap (\(Left s) -> s) (k (Left a))) s
plus _ l' k (Right s') = Right <$> l' (\a' -> fmap (\(Right s') -> s') (k (Right a'))) s'
이제 올바른 순서로 두 부분을 호출하는 모나딕 트래버설을 앞쪽에 합성(precompose)할 수 있다:
data OverallAnswer = ScopeError' | TypeError' | Type Type
pipeline :: MonadicTraversal (Context, TermSyn)
OverallAnswer
(Either ScopeCheckQuestion Question)
(Either ScopeCheckAnswer Answer)
pipeline k (ctx, t) = k (Left ScopeCheckQuestion) >>= \case
Left ScopeError -> return ScopeError'
Left WellScoped -> k (Right (Synthesise ctx t)) >>= \case
Right TypeError -> return TypeError'
Right (Synthesised a) -> return (Type a)
이건 완전히 만족스럽지는 않다. 부재한 의존 타입을 되돌려 넣는다 해도 마찬가지다. 하지만 동작은 한다. 더 정준적인 파이프라인 단계 시퀀싱 방법은 미래에 맡겨 두겠다.