用Haskell实现一些简单的类型系统的酷酷方法

总所周知, 类型论的操作语义可以用一堆写成大横线的规则来表示, 这篇文章会教你如何把大横线转换成haskell代码.

先从STLC开始, 首先是两颗语法树, 一个代表项, 一个代表类型,

type Id = String

data Type = Int | Type :-> Type
  deriving (Show, Eq)

data Term = Lam Id Type Term -- λ x : T . body
          | App Term Term   -- f x 
          | IntLit Int
          | Var Id 
          deriving (Show, Eq)

类型化

非常简单, 现在实现一下类型检查.

我们随便抽一个 STLC 的 typing rule 看一看,

\[ \dfrac{\Gamma \vdash f : A\to B\quad \Gamma \vdash x : A}{\Gamma\vdash f \ x : B} \]

可以看到赋型谓词 _⊢_:_ 有三个槽, 前两个槽可以看作输入, 最后一个槽是输出, 这样第一个输入的类型是一个语境(就是变量和类型的对应表), 第二个输入的类型是Term, 输出的类型就是Type.

这样我们的类型检查函数的类型就是 Map Id Type -> Term -> Maybe Type. 如果可以赋型, 那么返回正确的类型, 如果类型错误返回 Nothing, 如果你想携带一些错误信息, 就可以把Maybe单子换成Either之类的东东, 这里我们就用最简单的Maybe即可.

这样我们可以把上面的规则转换成如下代码:


type TypingRule = Map Id Type -> Term -> Maybe Type

typingApp :: TypingRule
typingApp ctx (App f x) = do -- Maybe 是个单子
  fT <- typing ctx f 
  case fT of 
    (a :-> b) -> do 
      xT <- typing ctx x
      if xT == a then 
        return b
      else 
        empty -- Maybe 是个 Alternative
    _ -> empty
typingApp ctx _ = empty

如果要包含一些错误信息, 可以把类型改作: MonadFail m => Map Id Type -> Term -> m Type, 并把 empty 换成 fail, 并填入错误信息.

如法炮制出其他的规则,

typingLam :: TypingRule
typingLam ctx (Lam x t b) = do 
  bT <- typing (insert x t ctx) b
  return (t :-> bT)
typingLam ctx _ = empty

typingInt :: TypingRule 
typingInt _ (IntLit _) = return Int 
typingInt _ _ = empty

typingVar :: TypingRule
typingVar ctx (Var x) = lookup x ctx
typingVar ctx _ = empty

最后再组合起来,

1 2	`typing :: TypingRule typing = typingApp <\|> typingLam <\|> typingInt <\|> typingVar`

这个写法的好处是可以很容易地看出来rule和代码的对应.

那我们可不可以用某种方法自动地把规则转换成代码? 答案是有的可以, 有的不可以, 这里STLC的类型化规则是可以的.

下面的表达式是一个词法上合法的haskell表达式,

1
2
3

   Γ ⊢ f : a ⇒ b /\ Γ ⊢ x : t /\ a == t
|---------------------------------------------| {- T app -} 
              Γ ⊢ App f x : b

我们可以用元编程的方式将其转换成对应的代码, 这比较复杂, 笔者已经帮大家写好了 https://github.com/KonjacSource/RuleNotation.

这样, 可以直接从类型规则生成函数.

typeofFunc :: Function
typeofFunc = Function
  { funcName = "typing"
  , aboveDefs = [ define [e| (c :* expr) ⊢ (x :* expr)  : (t :* patt) |] `bindTo` [e| t .<- typing c x |]
                , define [e| (x :* expr) : (t :* patt) ∈ (c :*expr) |] `bindTo` [e| t .<- liftMaybe (M.lookup x c) |]
                ]
  , belowDefs = [ define [e| (c :* expr) ⊢ (x :* expr)  : (t :* patt) |] `bindTo` [e| typing c x .:= t |]
                ]
  , bothDefs  = [ define [e| λ (x :* expr) : (t :* expr) ↦ (b :* expr) |] `bindTo` [e| Lam x t b |]
                , define [e| Γ |] `bindTo` [e| gamma |]
                , define [e| (a :* expr) ⇒ (b :* expr) |] `bindTo` [e| a :-> b |]
                , define [e| (c :* expr) <| (x :* expr) : (t :* expr) |] `bindTo` [e| insert x t c |]
                ]
  , rules     = [ [e|
                                       True
                      |---------------------------------------------| {- T int -}
                               Γ ⊢ IntLit n : Int
                  |]
                , [e|
                                   Γ <| x : s ⊢ b : t
                      |---------------------------------------------| {- T abs -} 
                                Γ ⊢ (λ x : s ↦ b) : s ⇒ t
                  |]
                , [e|
                         Γ ⊢ f : a ⇒ b /\ Γ ⊢ x : t /\ a == t
                     |---------------------------------------------| {- T app -} 
                                   Γ ⊢ App f x : b
                  |]
                , [e|
                                         x : t ∈ Γ
                      |---------------------------------------------| {- T var -}
                                      Γ ⊢ Var x : t
                  |]
                ]
  , argNames  = ["c", "t"]
  }

genFuncion typeofFunc 
-- 这会生成 typing :: (Monad f, Alternative f) => Map String Type -> Term -> f Type

上面的 define [e| (c :* expr) ⊢ (x :* expr) : (t :* patt) |] `bindTo` [e| t .<- typing c x |] 可以理解成宏定义, 会把形如 c ⊢ x : t 的表达式替换成 t .<- typing x, 后者会进一步被转换成 do-notation 中的 t <- typing x.

宏定义被分成横线上下两部分的定义, 比如c ⊢ x : t出现在横线上面的时候意味着调用 typing , 而在下面的时候意味着定义 typing.

求值

求值的规则也可以直接转换成代码.

这是小步求值的定义, 要求你提前定义好subst函数, 这个也可以用模板元自动生成.

infixl 6 -->
(-->) = undefined

infix 7 :=
data (:=) = (:=)

smallstepFunc :: Function
smallstepFunc = Function
  { funcName = "smallstep"
  , aboveDefs = [ define [e| (a :* expr) --> (b :* patt) |] `bindTo` [e| b .<- smallstep a |]
                ]
  , belowDefs = [ define [e| (a :* patt) --> (b :* expr) |] `bindTo` [e| smallstep a .:= b |]
                ]
  , bothDefs  = [ define [e| λ (x :* expr) : (t :* expr) ↦ (b :* expr) |] `bindTo` [e| Lam x t b |]
                , define [e| (a :* expr) ⇒ (b :* expr) |] `bindTo` [e| Func a b |]
                , define [e| (c :* expr) <| (x :* expr) : (t :* expr) |] `bindTo` [e| insert x t c |]
                , define [e| (a:*expr) ((b:*expr) := (c:*expr)) |] `bindTo` [e| subst (b,c) a |]
                ]
  , rules     = [ [e|
                            t1 --> t1'
                    |-------------------------|
                      App t1 t2 --> App t1' t2
                  |]
                , [e|
                            t2 --> t2'
                    |-------------------------|
                      App t1 t2 --> App t1 t2'
                  |]
                , [e|
                                      True
                    |---------------------------------------------|
                        App (λ x : s ↦ b) v --> b (x := v)
                  |]
                ]
  , argNames  = ["t"]

  }

大步求值可以用 NBE 实现,

infix 6 ⇓
(⇓) = undefined

data Value = VInt Int
           | VLam Ty (forall m. (Monad m, Alternative m) => Value -> m Value)
           | NVar String

asTerm :: (Monad m, Alternative m) => Value -> m Term
asTerm x = helper [] x
  where helper _ (NVar v) = pure $ Var v
        helper _ (VInt i) = pure $ IntLit i
        helper names (VLam t f) = let n = genName names "x" in do
          v' <- f (NVar n)
          v <- helper (n:names) v'
          pure $ Lam n t v

instance Show Value where
  show x = maybe "Nothing" show (asTerm @Maybe x)

evalFunc :: Function
evalFunc = Function
  { funcName = "eval"
  , aboveDefs = [ define [e| (c :* expr) ⊢ (x :* expr)  ⇓ (t :* patt) |] `bindTo` [e| t .<- eval c x |]
                , define [e| (x :* expr) := (t :* patt) ∈ (c :*expr) |] `bindTo` [e| t .<- maybeAlt (M.lookup x c) |]
                ]
  , belowDefs = [ define [e| (c :* patt) ⊢ (x :* patt)  ⇓ (t :* expr) |] `bindTo` [e| eval c x .:= t |]
                ]
  , bothDefs  = [ define [e| λ (x :* expr) : (t :* expr) ↦ (b :* expr) |] `bindTo` [e| Lam x t b |]
                , define [e| (a :* expr) ⇒ (b :* expr) |] `bindTo` [e| Func a b |]
                , define [e| (c :* expr) <| (x :* expr) := (t :* expr) |] `bindTo` [e| insert x t c |]
                ]
  , rules     = [ [e|
                        x := v ∈ c
                    |---------------|
                      c ⊢ Var x ⇓ v
                  |]
                , [e|
                                           True
                    |-----------------------------------------------------------------|
                     c ⊢ Lam x t v ⇓ VLam t (\xv -> maybeAlt $ eval (c <| x := xv) v)
                  |]
                , [e|
                             True
                    |-------------------------|
                      c ⊢ IntLit x ⇓ VInt x
                  |]
                , [e|
                      c ⊢ f ⇓ VLam _ fun /\ c ⊢ x ⇓ xv /\ ret .<- fun xv
                    |-------------------------------------------------------|
                                     c ⊢ App f x ⇓ ret
                  |]
                ]
  , argNames  = ["c","x"]
  }

依值类型

语法树,


data Term = Var Id 
          | U Int
          | Pi Id Term Term
          | Lam Id Term Term 
          | App Term Term 
          deriving (Show, Eq)

依值类型里面涉及到的判定相等相关的规则就不能直接转换成代码, 比如传递性规则,

\[ \dfrac{A \equiv B \quad B \equiv C }{A \equiv C} \]

这类规则若想搜索需要枚举B, 这太恐怖了. 补救方法是比较两者的normal form. 于是有如下的代码,

normalize :: Term -> Term
normalize term = runIdentity (travTerm1 help (fromMaybe term (help1 term)))
  where help1 :: Term -> Maybe Term
        -- If you defined more eliminator, add it here.
        help1 (App f arg) = case normalize f of
          Lam x t b -> pure $ normalize (subst (x, normalize arg) b)
          f' -> pure $ App f' (normalize arg)
        help1 _ = Nothing
        help x = case help1 x of
          Just x' -> pure x'
          _ -> pure $ normalize x

-- Alpha equivalent
infix 4 =*=
(=*=) :: Term -> Term -> Bool 
(=*=) = alphaCtx M.empty 
  where 
    alphaCtx vars (Var a) (Var b) = case M.lookup a vars of 
      Just a' -> a' == b 
      _ -> a == b 
    alphaCtx vars (U l1) (U l2) = l1 == l2 
    alphaCtx vars (Pi n t b) (Pi n' t' b') = let vars' = insert n n' vars in
      alphaCtx vars t t' && alphaCtx vars' b b' 
    alphaCtx vars (Lam n t b) (Lam n' t' b') = let vars' = insert n n' vars in 
      alphaCtx vars t t' && alphaCtx vars' b b' 
    alphaCtx vars (App f x) (App f' x') = alphaCtx vars f f' && alphaCtx vars x x' 
    alphaCtx _ _ _ = False

-- Judgemental equality
infix 4 =~ 
(=~) :: Term -> Term -> Bool 
t =~ t' = normalize t =*= normalize t'

然后我们依然可以直接翻译类型规则

typeofFunc :: Function
typeofFunc = Function
  { funcName = "typeof"
  , aboveDefs = [ define [e| (c :* expr) ⊢ (x :* expr)  : (t :* patt) |] `bindTo` [e| t .<- typeof c x |]
                , define [e| (x :* expr) : (t :* patt) ∈ (c :*expr) |] `bindTo` [e| t .<- maybeAlt (M.lookup x c) |]
                , define [e| (c :* expr ) ⊢ (t :* term) : U (l :* patt) |] `bindTo` [e| l .<- levelOf c t |]
                ]
  , belowDefs = [ define [e| (c :* expr) ⊢ (x :* expr)  : (t :* patt) |] `bindTo` [e| typeof c x .:= t |]
                ]
  , bothDefs  = [ define [e| λ (x :* expr) : (t :* expr) ↦ (b :* expr) |] `bindTo` [e| Lam x t b |]
                , define [e| Π ((x :* expr) : (t :* expr)) . (b :* expr) |] `bindTo` [e| Pi x t b |]
                , define [e| Γ |] `bindTo` [e| gamma |]
                , define [e| (c :* expr) <| (x :* expr) : (t :* expr) |] `bindTo` [e| insert x t c |]
                ]
  , rules     = [ [e|
                                       True
                      |---------------------------------------------|
                               Γ ⊢ U n : U (n + 1)
                  |]
                , [e| 
                                      x : t ∈ Γ
                      |---------------------------------------------|
                                    Γ ⊢ Var x : t
                  |]
                , [e| 
                         Γ ⊢ t : U l1 /\ (Γ <| x : t) ⊢ b : U l2
                      |---------------------------------------------|
                           Γ ⊢ (Π (x : t) . b) : U (max l1 l2)
                  |]
                , [e| 
                                  (Γ <| x : s) ⊢ b : t
                      |---------------------------------------------|
                           Γ ⊢ (λ x : s ↦ b) : (Π (x : s) . t)
                  |]
                , [e| 
                         Γ ⊢ f : (Π (y : s) . t) /\ Γ ⊢ x : s' /\ s =~ s'
                      |-------------------------------------------------------|
                                     Γ ⊢ App f x : t
                  |]
                ]
  , argNames  = ["c", "t"]
  }

#Haskell #编程 #计算机 #类型论

用Haskell实现一些简单的类型系统的酷酷方法

http://konjacsource.github.io/2024/07/15/用Haskell实现一些简单的类型系统/

作者

KonjacSource

发布于

2024年7月15日

许可协议

依值类型下的归纳类型和模式匹配的实现笔记上一篇

如何形式化验证一场技术面试下一篇