🌐 Read in English

9장의 배경지식.

힌들리-밀너, 차근차근

이 글은 힌들리-밀너 일반에 대한 튜토리얼이 아니다 — 교과서적인 HM에는 일반화, 발생 검사(occurs check), let 다형성이 처음부터 갖춰져 있다. 이 글이 다루는 것은 MicroHs가 실제로 처음 내놓은 특정 검사기, 즉 cc57346e("First version with type checking."(타입 검사가 들어간 첫 버전), 2023-08-06) 시점의 src/MicroHs/TypeCheck.hs다. 아래의 모든 주장은 그 파일, 그 커밋을 기준으로, 또는 cc57346e 빌드를 통해 실제로 실행한 프로그램을 기준으로 검증되었다.

타입도 항이다

핵심이자 다른 모든 절이 의지하는 사실: MicroHs에는 별도의 타입 구문용 AST가 없다. 33b009fa("Use Expr for EType."(EType에 Expr을 쓰기), 2023-07-21)는 8장의 db418344 이래로 있어 왔던 세 생성자짜리 EType(TVar/TConstr/TUVar)을 지우고, 이미 항을 표현하고 있는 바로 그 Expr에 대한 타입 동의어로 바꿔친다 (33b009fa:src/MicroHs/Parse.hs 99–111행, 전문 인용):

-- Expr restricted to
--  * after desugaring: EApp and EVar
--  * before desugaring: EApp, EVar, ETuple, EList
type EType = Expr

validType :: Expr -> Bool
validType ae =
  case ae of
    EVar _ -> True
    EApp f a -> validType f && validType a
    EList es -> length es <= 1 && all validType (take 1 es)
    ETuple es -> all validType es
    _ -> False

타입이란 그저 validType을 만족하는 Expr일 뿐이다 — 타입 변수와 타입 생성자는 둘 다 EVar이고, 타입 적용(Maybe Int, [a], a -> b)은 EApp이며, 타입을 위한 별도의 파서 생성 규칙은 아예 없다: pType은 평범한 식 파서를 그대로 돌려서 돌아온 결과에 validType을 검사할 뿐이다(33b009fa:src/MicroHs/Parse.hs 450–454행). 이는 검사기 안까지 그대로 이어진다 — 메타변수(교과서 HM의 α, β, ...)는 같은 Expr 타입 위의 생성자 하나가 더 있는 것일 뿐이다 (cc57346e:src/MicroHs/Parse.hs 56–78행, 일부 인용, ...는 중간에 생략된 생성자를 표시):

data Expr
  = EVar Ident
  | EApp Expr Expr
  ...
  | EBad
  -- Only while type checking
  | EUVar Int
  -- Constructors after type checking
  | ECon ConTyInfo Ident
  --Xderiving (Show, Eq)

Type 모듈이 따로 없을 뿐 아니라 별도의 Kind 타입조차 없다 — type EKind = EType(cc57346e:src/MicroHs/Parse.hs 133행). 항, 타입, 카인드가 처음부터 끝까지 하나의 재귀적 데이터 타입이다.

메타변수와 치환, 구현된 그대로

미지의 타입은 EUVar Int, 그저 정수 태그일 뿐이다. 그 태그를 풀어내는 치환은 검사기 자신의 상태 안에 있는 단 하나의 IM.IntMap EType이다 (cc57346e:src/MicroHs/TypeCheck.hs 132행):

data TCState = TC IdentModule Int TypeTable ValueTable (IM.IntMap EType)

그 옆의 Int는 새 이름을 위한 카운터다; newUVar가 이를 하나 올리고 EUVar n을 돌려준다(cc57346e:src/MicroHs/TypeCheck.hs 338–342행). 해를 기록하는 것은 평범한 맵 삽입인 addUVar다 (cc57346e:src/MicroHs/TypeCheck.hs 254–262행, 전문 인용):

addUVar :: Int -> EType -> T ()
addUVar i t = T.do
  let
    add = T.do
      TC mn n tenv venv sub <- get
      put (TC mn n tenv venv (IM.insert i t sub))
  case t of
    EUVar j -> if i == j then T.return () else add
    _ -> add

여기서의 유일한 검사는 i == j다 — i ↦ EUVar i 삽입을 거부한다. 이것이 안전망의 전부다; 더 깊은 발생 검사는 없으며, 아래 "이 검사기가 빠뜨린 것"이 그 대가를 보여준다. 기록된 해를 다시 읽어내는 것은 맵을 재귀적으로 따라간다(derefUVar, cc57346e:src/MicroHs/TypeCheck.hs 291–300행, 전문 인용):

derefUVar :: EType -> T EType
derefUVar at =
  case at of
    EApp f a -> EApp <$> expandType f <*> expandType a
    EUVar i -> T.do
      sub <- gets uvarSubst
      case IM.lookup i sub of
        Nothing -> T.return at
        Just t -> derefUVar t
    _ -> T.return at

expandType(270–273행)은 derefUVar 다음에 expandSyn을 잇는 것으로, 다른 맵 — 타입 동의어 — 에 대해 같은 종류의 조회를 한다. 그리고 이름 있는 타입 변수를 치환하는 것(forall 인스턴스화가 필요로 하는 것)은 또 별개다: subst, 평범한 구문적 순회다 (cc57346e:src/MicroHs/Parse.hs 759–768행, 전문 인용):

subst :: [(Ident, Expr)] -> Expr -> Expr
subst s =
  let
    sub ae =
      case ae of
        EVar i -> fromMaybe ae $ lookupBy eqIdent i s
        EApp f a -> EApp (sub f) (sub a)
        EUVar _ -> ae
        _ -> error "subst unimplemented"
  in sub

세 가지 메커니즘, 세 조각의 상태, 모두 하나의 Expr 타입 위에 있다.

단일화, 손으로 추적하기

unify/unifyR(cc57346e:src/MicroHs/TypeCheck.hs 302–330행, 전문 인용)이 알고리즘의 전부다 — 양쪽을 역참조한 다음, 구조적으로 비교한다:

unify :: HasCallStack => EType -> EType -> T ()
unify a b = T.do
  aa <- expandType a
  bb <- expandType b
  unifyR aa bb
  
unifyR :: HasCallStack => EType -> EType -> T ()
unifyR a b = T.do
  venv <- gets valueTable
  tenv <- gets typeTable
  let bad = error $ "Cannot unify " ++ showExpr a ++ " and " ++ showExpr b ++ "\n" ++
                    show a ++ " - " ++ show b ++ "\n" ++
                    show tenv ++ "\n" ++
                    show venv
  case a of
    EVar ia ->
      case b of
        EVar ib  -> if eqIdent ia ib then T.return () else bad
        EApp _ _ -> bad
        EUVar i  -> addUVar i a
        _        -> impossible
    EApp fa xa ->
      case b of
        EVar _     -> bad
        EApp fb xb -> T.do { unify fa fb; unify xa xb }
        EUVar i    -> addUVar i a
        _          -> impossible
    EUVar i -> addUVar i b
    _ -> impossible

디슈가링된 EType은 EVar/EApp/EUVar만 담으므로, 케이스는 네 개뿐이다: 두 생성자 이름은 식별자로 정확히 일치해야 한다; 두 적용은 머리와 인자를 따로따로 단일화한다(tArrow a r = EApp (EApp (EVar "Primitives.->") a) r이므로, a -> b와 Int -> Char가 이렇게 둘로 갈라진다); 어느 한쪽이라도 메타변수면 그저 바인딩을 기록할 뿐이다.

추적 1 — 호출 const 5 'x'에서, const :: forall a b . a -> b -> a는 사용 지점에서 EUVar 2 -> EUVar 3 -> EUVar 2로 새로 인스턴스화된 상태다(아래 tInst 참고) — 이 적용의 결과 메타변수 τ(EUVar 1)는 tInst가 스킴을 인스턴스화하기 전에 할당되므로, 가장 높은 번호가 아니라 가장 낮은 새 번호를 갖는다. 이 적용을 검사하는 것은 새로 인스턴스화된 스킴을 Int -> (Char -> τ)에 대해 단일화한다: unify (EUVar 2) Int → addUVar 2 Int; unify (EUVar 3) Char → addUVar 3 Char; unify (EUVar 1) (EUVar 2) → unify는 먼저 양쪽에 expandType을 돌리는데, 2 ↦ Int가 이미 맵에 있으므로 기록되는 바인딩은 곧바로 addUVar 1 Int다 — 두 단계를 거쳐 따라갈 필요가 없다. 이후 τ를 역참조하면 1 ↦ Int를 읽는다 — 이 호출의 결과 타입은 Int다.

추적 2 — 실제로 실행해 본, 실패하는 단일화: bad2 :: forall a b . a -> b -> a; bad2 x y = x + 1은 Cannot unify a and Primitives.Int로 실패한다 — bad2 자신의 본문 안에서는 시그니처의 a가 그대로, 인스턴스화되지 않은 EVar 이름이기 때문이다(이유는 다음 절에서). unifyR의 EVar/EVar 케이스가 ia = "a", ib = "Primitives.Int"로 실행되고, eqIdent가 거짓이 되어 bad가 발동한다. 메타변수는 전혀 관여하지 않는다.

forall, 인스턴스화, 그리고 고정된 타입 변수

f7db30f1("Add lots of type signatues and forall."(타입 시그니처와 forall을 왕창 추가), 2023-07-23)는 표준 라이브러리 전체에 forall을 추가한다 — 파일 9개, 추가 134줄, 삭제 74줄, 전부 lib/ 및 Makefile 아래다. 손댄 함수 대부분은 이미 시그니처를 갖고 있었다; 새로 생긴 것은 한정 기호다(f7db30f1:lib/Data/Function.hs, 일부 인용: 첫 번째 ... 뒤에 .와 id가, 두 번째 ... 뒤에 flip이, fix 뒤에 uncurry가 생략됨 — 이 넷은 각각 ($)와 같은 방식으로 그저 forall을 얻을 뿐이다):

-($) :: (a -> b) -> a -> b
+($) :: forall a b . (a -> b) -> a -> b
...
-const :: a -> b -> a
+const :: forall a b . a -> b -> a
...
+fix :: forall a . (a -> a) -> a
 fix = primFix

한정 기호가 중요한 이유는 기계적이다. ETypeScheme [Ident] EType은 속박된 이름의 명시적인 목록을 나른다(cc57346e:src/MicroHs/Parse.hs 130행), 그리고 파서는 그 키워드를 볼 때만 이를 채운다 (cc57346e:src/MicroHs/Parse.hs 484–488행, 전문 인용):

pTypeScheme :: P ETypeScheme
pTypeScheme = P.do
  vs <- (pKeyword "forall" *> esome pLIdent <* pSym '.') <|< pure []
  t <- pType
  pure $ ETypeScheme vs t

시그니처를 검사하는 것(TypeCheck.hs의 tcTypeScheme, 485–488행)은 정확히 vs 안의 이름들만 스코프에 들여온다; 한 번도 한정되지 않은 이름은 그냥 스코프에 없다. cc57346e 워크트리에서 const의 시그니처에서 한정 기호를 지우고(const :: a -> b -> a, forall 없음) 이를 사용하는 프로그램을 컴파일해 확인했다:

mhs: undefined variable a
CallStack (from HasCallStack):
  error, called at src/MicroHs/TypeCheck.hs:354:16 in main:MicroHs.TypeCheck

— 검사기는 const의 시그니처에서 실패하고, 본문에는 아예 도달하지 못한다. forall이 없으면 다형적으로 보이는 시그니처는 그 자체로 잘못된 형태이며, 이것이 cc57346e가 무엇이든 받아들일 수 있게 되기 두 주 전에 f7db30f1이 라이브러리를 훑어야 했던 이유다.

그렇다면 이 파일 어디에도 일반화 단계가 없는데, 무엇이 정의를 다형적으로 만드는가? tInst는 스킴의 속박된 이름들을 오직 사용 지점에서만 새 메타변수로 새로 고친다 — 모든 EVar 참조는 tLookupInst를 거친다(cc57346e:src/MicroHs/TypeCheck.hs 364–371행, 전문 인용):

tInst :: ETypeScheme -> T EType
tInst as =
  case as of
    ETypeScheme vs t ->
      if null vs then T.return t
      else T.do
        us <- mapM (const newUVar) (replicate (length vs) ())
        T.return (subst (zip vs us) t)

하지만 검사기가 정의 자체를 검증할 때는, tcDefValue(526–536행)가 본문을 선언된 타입에 대해 그대로 검사한다 — 여전히 새 메타변수가 아니라 리터럴 식별자 a/b를 그대로 담은 채로. unifyR의 EVar/EVar 케이스가 동일한 이름을 요구하므로, a는 그 정의 하나를 검사하는 동안 고정되고 불투명한 상수처럼 동작한다 — 정확히 위의 bad2 실패가 보여주는 것이다. 두 가지 결과가 따른다: (1) 다형성 = 정의에서의 고정 검사 더하기 모든 호출 지점에서의 새 인스턴스화 (검증됨: const 5 'x'와 const "hi" 42를 호출하는 프로그램 하나가 컴파일되어 5, 그다음 "hi"를 출력한다); (2) 일반화가 없으므로, 모든 최상위 바인딩이 검사되려면 명시적 시그니처가 필요하다 — 다음 절이 시그니처가 없을 때의 대가를 보여준다.

이 검사기가 빠뜨린 것

파일을 직접 확인한 것이지, "진짜" 힌들리-밀너에 대한 익숙함에서 가정한 것이 아니다:

• 발생 검사가 없다. addUVar의 유일한 방어는 i ↦ EUVar i 그 자체이며, t 안에 EUVar i가 더 깊이 중첩되어 있는지는 결코 검사하지 않는다. \x -> x x는 x의 메타변수를 x의-메타변수 -> τ와 단일화하는데, addUVar는 이 순환을 태연히 기록한다 — "무한 타입" 오류는 없다. 실제로 실행해 보면(cc57346e 빌드, ulimit -v 2000000): 그 람다를 쓰지 않는 let 안에 넣은 프로그램은 mhs: out of memory로 죽는데, derefUVar가 치환 자신의 순환을 뒤쫓는 것이다. (한도 없이 두면, 같은 실행이 죽임당하기 전까지 호스트 RAM을 수십 기가바이트 소비했다 — 가상의 이야기가 아니라 진짜 종료되지 않는 것이다.)
• 지역 바인딩에는 let 다형성이 없다. tcBinds는 각 지역 바인딩에 빈 스킴 ETypeScheme [] 안의 새 메타변수 하나를 준다 (cc57346e:src/MicroHs/TypeCheck.hs 708행), 그래서 이에 대한 tInst는 null vs 케이스가 되어 — 새로 고침이 결코 일어나지 않는다. 두 개의 다른 타입으로 쓰이는 지역 함수 — 교과서적인 let 일반화가 존재하는 이유 그 자체 — 는 여기서 그냥 "Cannot unify" 오류가 된다.
• 상호 재귀는, 코드 스스로 인정하듯, 열린 구멍이다. tcBinds는 -- XXX No mutual recursion yet(703행)를 달고 있다. cc57346e에서 테스트해 보면: 단독으로 자기 재귀하는 지역 함수는 동작하지만 (let countdown n = if n == 0 then 0 else countdown (n - 1)은 0까지 실행된다), 서로를 호출하는 두 지역 함수는 실패한다 — 타입 검사 다음 단계인 이름 해석에서: src/MicroHs/Main.hs의 링킹 패스가 내는 mhs: undefined: isOdd.
• 타입 클래스가 없다. cc57346e 시점의 Parse.hs와 TypeCheck.hs에 grep -in "class"를 돌려도 아무것도 나오지 않는다 — AST 케이스도, 딕셔너리도 없다. do 표기법은 여전히 Monad 제약이 아니라 명시적 모듈 한정자(3장)로 (>>=)/(>>)를 해소한다.
• 카인드가 있긴 하지만, 겨우 있는 정도다. EKind는 다시 EType이며, 단일 센티널 kType = EVar "Type"(228–229행)에 대해 검사된다 — data Foo a = Foo (a Int) 같은 애리티 불일치를 거부할 정도는 되지만, 모든 타입 변수는 카인드 Type을 가지며 * -> * 이상을 다루는 장치는 없다.

예제로 풀어보기: const

lib/Data/Function.hs(cc57346e):

const :: forall a b . a -> b -> a
const x _ = x

tcDefValue가 하는 방식대로 손으로 추론해 보면 — ELam "x" (ELam "_" (EVar "x"))를 선언된 a -> b -> a에 대해 순회하며, a/b는 고정된 이름으로 스코프에 있다:

1. 바깥쪽 ELam "x" e, 기대 타입은 a -> (b -> a). 새 메타변수 τ₁이 x의 타입을 나타낸다; 본문은 기대 타입 없이 검사되고 (ELam 케이스는 Nothing으로 재귀하고 나중에 단일화한다), 환경에는 x : τ₁이 들어간다.
2. 안쪽 ELam "_" (EVar "x"): _를 위한 새 τ₂; 본문은 x를 찾아보고 τ₁을 돌려준다. 안쪽 람다의 타입은 τ₂ -> τ₁이다.
3. 바깥쪽 람다의 구성된 타입 τ₁ -> (τ₂ -> τ₁)을 a -> (b -> a)에 대해 단일화한다: τ₁ ↦ a, τ₂ ↦ b, 그리고 반환 위치의 unify τ₁ a는 unifyR (EVar "a") (EVar "a")로 귀결되어 — eqIdent에 의해 성공한다.

모든 메타변수가 시그니처 자신의 a/b로 해소되고, 모순은 없다 — 본문은 소스와 일치하는 forall a b . a -> b -> a에 대해 검사를 통과한다. 실제 검사기를 통해 확인(cc57346e 워크트리, 실제 lib/ 트리에 -ilib):

$ cat > ConstDemo.hs <<'EOF'
module ConstDemo(module ConstDemo) where
import Prelude

main :: IO ()
main = do
  putStrLn (showInt (const 5 'x'))
  putStrLn (const "hi" 42)
EOF
$ nix develop $MICROHS -c ./bin/mhs -ilib ConstDemo
$ nix develop $MICROHS -c ./bin/eval
5
hi

const 5 'x'는 a ↦ Int, b ↦ Char로 인스턴스화되고; const "hi" 42는 a ↦ [Char], b ↦ Int로 인스턴스화된다 — 고정 검사된 하나의 정의에 대한 두 개의 독립적인 인스턴스화이며, tInst가 예측하는 그대로다.