λ→のtyping & unification algorithm

この記事のunification algorithmは間違っているので
λμのTypeCheckerの実装 - Just $ A sandboxを参考にしてください

λ→のtypingアルゴリズム.
variableとabstractionは型が一意に決まるので, 問題はapplication.
MN:aからM:?x -> aの?xをどうやって決定するかという問題になる.

holeの導入

型変数とは別に, hole(goal)を導入する.
holeは確定していない型で, どんな型も入ることができる. さらにtypingが下から上に, 左から右に進む関係上, typingが進むにつれて段々確定していく.

例:

|- λf. λx. f x : ??
-> f:?0, x:?1 |- f x : ??  <-- abstractionした
-> f:?0, x:?1 |- f:?0  f:?0, x:?1 |- x:?1  <-- application
-> f:?1 -> ?2, x:?1 |- f x :?2  <-- fは関数型なので{?0 = ?1 -> ?2}を代入した
-> |- λ(f: ?1 -> ?2). λ(x: ?1). f x : (?1 -> ?2) -> ?1 -> ?2  <-- abstractionした

applicationの時にholeの代入が必要になる.
この時, holeの等式を代入するという操作をするが, これはbase(|-の左側)と現在確定している型の中身にも代入する必要がある.
このように, 等式が与えられるとそれらに含まれるような最大の型を取ってくるという操作が必要になり, これをunificationという.

unificationは失敗することもある.

x:?0 |- x x : ??
-> x:?0 |- x:?0  x:?0 |- x:?0  <-- {?0 = ?0 -> ?1}はunification不可能

typing algorithm

実際のtyping algorithmは次のような感じになるはず.

-- var
G |- x : ??
-> G |- x : G(x)

-- abs
G |- λx. e : ??
-> G, x:?n |- e : Type(e)
-> G |- λx. e : ?n -> Type(e)

-- app
G |- M N : ??
-> G |- M : Type(M)  G |- N : Type(N)
-> unify {Type(M) = Type(N) -> ?n}
-> G |- M N : ?n

unification algorithmは必要な部分で左辺を右辺に置き換える処理を書くだけのはず.

data Typ = TVar String | TArr Typ Typ | Hole Int
data Untyped = Var String | App Untyped Untyped | Abs String Untyped
type Base = [(String, Typ)]

data Checking = Checking {
  _base :: Base,
  _freshHole :: Int,
  _holes :: [(Int, Typ)]
  }

makeLenses ''Checking

fresh :: (Monad m) => StateT Checking m Int
fresh = do
  n <- use freshHole
  freshHole += 1
  return n

typing :: Untyped -> Either String Typ
typing t = flip evalStateT (Checking [] 0 []) $ go t where
  go :: Untyped -> StateT Checking (Either String) Typ
  go (Var v) = do
    gs <- use base
    case lookup v gs of
      Just t -> return t
      Nothing -> lift $ Left $ "Not in scope: " ++ v ++ " in " ++ show gs
  go (Abs x e) = do
    n <- fresh
    base <>= [(x, Hole n)]
    t <- go e
    hs <- use holes
    return $ apply hs $ TArr (Hole n) t
  go (App e1 e2) = do
    t1 <- go e1
    t2 <- go e2
    n <- fresh
    unify t1 (TArr t2 (Hole n))
    hs <- use holes
    return $ apply hs (Hole n)

  apply :: [(Int, Typ)] -> Typ -> Typ
  apply bs (Hole n) = case lookup n bs of
    Just t -> apply bs t
    Nothing -> Hole n
  apply bs (TVar a) = TVar a
  apply bs (TArr t1 t2) = TArr (apply bs t1) (apply bs t2)

  replace :: Int -> Typ -> Base -> Base
  replace n typ = fmap (second go) where
    go :: Typ -> Typ
    go (TVar a) = TVar a
    go (Hole m)
      | m == n = typ
      | otherwise = Hole m
    go (TArr t1 t2) = TArr (go t1) (go t2)

  allHoles :: Typ -> [Int]
  allHoles (Hole n) = [n]
  allHoles (TArr x y) = allHoles x ++ allHoles y
  allHoles _ = []

  unify :: Typ -> Typ -> StateT Checking (Either String) ()
  unify (Hole n1) t = if n1 `elem` allHoles t
    then lift $ Left $ "Unification failed: " ++ show (Hole n1) ++ " in " ++ show t
    else base %= replace n1 t >> holes <>= [(n1,t)]
  unify t1 (Hole n) = unify (Hole n) t1
  unify (TVar a) (TVar b)
    | a == b = return ()
    | otherwise = lift $ Left $ "Type mismatch: " ++ a ++ " /= " ++ b
  unify (TArr t1 t1') (TArr t2 t2') = unify t1 t2 >> unify t1' t2'
  unify (x@(TArr _ _)) y = lift $ Left $ "Unification failed: " ++ show x ++ " and " ++ show y

動かす

なんかこんな感じになる.

λx. x : Right ?0 -> ?0
λx. λy. y x : Right ?0 -> (?0 -> ?2) -> ?2
λf. λg. λx. f (g x) x : Right (?3 -> ?2 -> ?5) -> (?2 -> ?3) -> ?2 -> ?5
λx. x x : Left "Unification failed: ?0 in ?0 -> ?1"
λx. x y : Left "Not in scope: y in [(\"x\",?0)]"
λf. λx. f (x x) : Left "Unification failed: ?1 in ?1 -> ?2"