Haskell for Lambda微积分,类型推理

从简单类型的lambda演算中取出的关键是在lambda绑定器本身上注释类型,每个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)]

Ø那么空的环境就是这么简单[].当皮尔斯写道时,?, x : T ? ...他意味着环境扩展了x绑定到类型的定义T.在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进行攻击.

基本上.我相信这是来自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

因此,我们抛弃这种类型的环境,并在我们去的时候扩展它.这里的输入规则很容易转换为算法,因为它们完全对应于语法.EG,对于一个术语M,只有一条规则得出结论Env |- M : T.

当不是例如子类型的情况时,这变得更加困难.