Haskell 用于 Lambda 微积分，类型推断

Question

我在 Haskell 编程中的冒险并不全是史诗般的。我正在实现简单的 Lambda 演算，我很高兴完成了 Syntax、Evaluation 和 Substitution，希望它们是正确的。剩下的是红色框内定义的typing（在下图中），我正在寻找指导。

标题

如有错误请指正，

(1) 但我收集到的是(T-Var)，返回给定变量x 的类型。 Haskell 中的什么构造返回 type ？我知道在prelude 是:t x，但我正在寻找一个在main = do 下工作的。

(2) 如果我要定义一个函数type_of，很可能我需要定义预期和返回类型，例如， type_of (Var x) :: type1 -> type2

type1 应该是通用的，type2 必须是存储变量类型信息的任何对象类型。为此，我不知道如何定义type1 和type2。

(3) 对于 (T-APP) 和 (T-ABS)，我假设我分别对 Abstraction String Lambda 和 Application Lambda Lambda 应用替换。简化形式的类型是返回的类型。对吗？

提前谢谢...

Answer 1

从简单类型化的 lambda 演算中带走的关键是类型在 lambda 绑定器本身上进行了注释，每个 lambda 项都有一个类型。 Pierce 提供的输入规则是如何机械地type-check 表达式是否正确输入。 类型推断是他在本书后面介绍的一个主题，即从无类型表达式中恢复类型。

除此之外，Pierce 在这个例子中没有给出几个地面类型 (Bool, Int)，它们在实现算法时很有帮助，所以我们也将它们附加到我们的定义中。

t = x
  | λ x : T . t
  | t t
  | <num>
  | true
  | false

T = T -> T
  | TInt
  | TBool

如果我们把它翻译成 Haskell，我们会得到：

type Sym = String

data Expr
    = Var Sym
    | Lam Sym Type Expr
    | App Expr Expr
    | Lit Ground
     deriving (Show, Eq, Ord)

data Ground = LInt Int
            | LBool Bool
            deriving (Show, Eq, Ord)

data Type = TInt
          | TBool
          | TArr Type Type
          deriving (Eq, Read, Show)

贯穿方程式的Γ 用于类型环境，我们可以在Haskell 中将其表示为简单的列表结构。

type Env = [(Sym, Type)]

空的环境Ø 就是[]。当 Pierce 写 Γ, x : T ⊢ ... 时，他的意思是使用绑定到类型 T 的 x 的定义扩展的环境。在 Haskell 中，我们会像这样实现它：

extend :: Env -> (Sym, Type) -> Env
extend env xt = xt : env

为了从 TAPL 编写检查器，我们实现了一个小的错误单子堆栈。

data TypeError = Err String deriving Show

instance Error TypeError where
    noMsg = Err ""

type Check a = ErrorT TypeError Identity a

check :: Env -> Expr -> Check Type
check _ (Lit LInt{}) = return TInt
check _ (Lit LBool{}) = return TBool

--  x : T ∈ Γ
--  ----------
--  Γ ⊦ x : T

check env (Var x) = case (lookup x env) of
    Just e  -> return e
    Nothing -> throwError $ Err "Not in Scope"

--  Γ, x : T ⊦ e : T'
--  --------------------
--  Γ ⊦ λ x . e : T → T'

check env (Lam x t e) = do
  rhs <- (check (extend env (x,t)) e)
  return (TArr t rhs)

--  Γ ⊦ e1 : T → T'   Γ ⊦ e2 : T
--  ----------------------------
--  Γ ⊦ e1 e2 : T'

check env (App e1 e2) = do
  t1 <- check env e1
  t2 <- check env e2
  case t1 of
     (TArr t1a t1r) | t1a == t2 -> return t1r
     (TArr t1a _) -> throwError $ Err "Type mismatch"
     ty -> throwError $ Err "Trying to apply non-function"

runCheck :: Check a -> Either TypeError a
runCheck = runIdentity . runErrorT

checkExpr :: Expr -> Either TypeError Type
checkExpr x = runCheck $ check [] x

当我们在一个表达式上调用checkExpr 时，我们要么返回表达式的有效类型，要么返回一个TypeError，表明函数出了什么问题。

例如，如果我们有这个词：

(λx : Int -> Int . x) (λy : Int. y) 3
App (App (Lam "x" (TArr TInt TInt) (Var "x")) (Lam "y" TInt (Var "y"))) (Lit (LInt 3))

我们希望我们的类型检查器验证它是否具有输出类型TInt。

但是因为这样的术语而失败：

(λx : Int -> Int . x) 3
App (Lam "x" (TArr TInt TInt) (Var "x")) (Lit (LInt 3))

因为TInt 不等于(TInt -> TInt)。

这就是对 STLC 进行类型检查的全部内容。

Answer 2

基本上。我相信这是来自 TAPL（至少它看起来像来自 TAPL 的表格），所以会有一章是关于算法类型检查的。但它本质上是这样的

typeOf :: TypeEnv -> Term -> Type
typeOf typeEnv (Var x)   = x `lookup` typeEnv
typeOf typeEnv (Abs var ty x) = ty `Arrow` typeOf ((x, ty) `extending` typeEnv) x
typeOf typeEnv (App f arg) = case typeOf f of
  Arrow inp out | inp == argT -> out
  _ -> Fail Some How
  where argT = typeOf typeEnv arg

所以我们在这种类型的环境中折腾并在我们进行时对其进行扩展。这里的输入规则很容易转换为算法，因为它们与语法完全对应。例如，对于一个术语M，只有一条规则，其结论是Env |- M : T。

当子类型不是这种情况时，这会变得更加困难。