Haskell for Lambda Calculus, Type Inferencing

functional-programming, haskell, lambda, lambda-calculus, types

Solution

The key thing to take away from the simply typed lambda calculus is that the types are annotated on the lambda binders itself, every lambda term has a type. The typing rules that Pierce provides are are how to mechanically type-check that the expression is well-typed. type inference is a topic he covers later in the book, which is recovering the types from untyped expressions.

Aside, what Pierce doesn't give in this example is a couple ground types (`Bool`, `Int`) , which are helpful when implementing the algorithm, so we'll just append those to our definition as well.

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

T = T -> T
  | TInt
  | TBool

If we translate this into Haskell we get:

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)

The `Γ` that pierce threads through the equations is for type environment which we can represent in Haskell as a simple list structure.

type Env = [(Sym, Type)]

The empty environment `Ø` is then simply `[]`. When Pierce writes `Γ, x : T ⊢ ...` he means the environment extended with the definition of `x` bound to the type `T`. In Haskell we would implement it like:

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

To write the checker from TAPL we implement a little error monad stack.

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

When we call `checkExpr` on a expression we either get back the valid type of the expression or a `TypeError` indicating what is wrong with the function.

For instance if we have the term:

(λ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))

We expect our type checker to validate that it it has output type `TInt`.

But to fail for a term like:

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

Since `TInt` is not equal to `(TInt -> TInt)`.

That's all there really is to typechecking the STLC.

Problem

Original source