Haskell for Lambda Calculus，类型推断

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)和(T)，我假设我分别在Abstraction String Lambda和Application Lambda Lambda上应用替代。还原表单的类型是返回的类型。对吗？

提前谢谢..。

Answer 1

从简单类型的lambda演算中取下来的关键是，类型是在lambda绑定器本身上注释的，每个lambda项都有一个类型。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)]

然后，空环境Ø就是[]。当皮尔斯写Γ, 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。

例如，当这种情况与子类型不同时，这就变得更加困难了。