Haskell for Lambda Calculus, Type Inferencing

Question

My adventure in Haskell programming hasn't been all epic. I am implementing Simple Lambda Calculus, and I am glad to have finished Syntax, Evaluation, as well as Substitution, hoping they are correct. What remains is typing as defined inside the red box (in the figure below), for which I am looking for guidance.

Heading

Please correct me if I am wrong,

(1) but what I gathered is that (T-Var), returns the type of given a variable x. What construct in Haskell returns type ? I know that in prelude it is :t x, but I am looking for one that works under main = do.

(2) If I were to define a function type_of, it's most likely that I need to define the expected and return type, as an example, type_of (Var x) :: type1 -> type2

type1 should be generic and type2 must be whatever object type that stores type information of a variable. For this, I am lost on how to define type1 and type2.

(3) For (T-APP) and (T-ABS), I assume I apply substitution on Abstraction String Lambda and Application Lambda Lambda respectively. The type of the reduced form is the returned type. Is that correct?

Thanks in advance...

Answer 1

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.

Answer 2

Basically. I believe this is from TAPL (it looks like a table from TAPL at least) so there's a chapter coming up on algorithmic typechecking. But it essentially goes like

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

So we toss around this type environment and extend it as we go. The typing rules here are easy to translate to an algorithm because they correspond to the syntax exactly. EG, for a term M there is exactly one rule with the conclusion that Env |- M : T.

This becomes much harder when this isn't the case with for example subtyping.