Haskell 用于 Lambda 演算、类型推断

Question

我在 Haskell 编程中的冒险并不都是史诗般的。我正在实现简单的 Lambda 演算，我很高兴完成了语法、评估以及替换，希望它们是正确的。剩下的就是红色框中定义的打字(如下图所示)，我正在寻找指导。

标题

如有错误，请指正

(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)，我假设我分别对抽象字符串 Lambda 和应用程序 Lambda Lambda 应用替换。简化形式的类型是返回的类型。这是正确的吗？

提前致谢...

Answer 1

从简单类型的 lambda 演算中得到的关键是，类型在 lambda 绑定(bind)器本身上进行注释，每个 lambda 项都有一个类型。 Pierce 提供的打字规则是如何机械地类型检查表达式的类型是否正确。 类型推断是他在本书后面讨论的一个主题，即从非类型化表达式中恢复类型。

此外，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)]

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

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

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

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 类型检查的全部内容。