Type checking and co

The 12 problems
Unification
Type inference in λ_→
Type inhabitation in λ_→
Other systems
Type checking fully annotated terms
Type checking modes
Bidirectional type checking

Primitive type checker

import Control.Monad.Trans.Except

module Nine where


type VarName = String
type Context = [(VarName, Type)]

infixr 1 :->:
data Type = TVar VarName | Type :->: Type
          | TBool
  deriving (Eq, Show)

infixl 8 :@:
infixr 8 :-
data Term = Var VarName | Lam VarName Term | Term :@: Term | Term :- Type
          | TTrue | TFalse | TIf Term Term Term
  deriving Show



deriveType :: Context -> Term -> Except String Type
deriveType ctx (Var x) = case lookup x ctx of
  Nothing -> throwE $ "Variable not in scope: " ++ x
  Just t  -> pure t
deriveType ctx (p :@: q) = do
  tp <- deriveType ctx p
  case tp of
    sigma :->: tau -> do
      checkType ctx q sigma
      pure tau
    _ -> throwE $ "Function type expected"
deriveType _ TTrue  = pure TBool
deriveType _ TFalse = pure TBool
deriveType ctx (p :- sigma) = checkType ctx p sigma >> pure sigma
deriveType _ t = throwE $ "Cannot derive type of " ++ show t

checkType :: Context -> Term -> Type -> Except String ()
checkType ctx (Lam x p) (sigma :->: tau) = checkType ((x, sigma) : ctx) p tau
checkType ctx (TIf c1 c2 c3) sigma = do
  checkType ctx c1 TBool
  checkType ctx c2 sigma
  checkType ctx c3 sigma
checkType ctx t sigma = do
  sigma' <- deriveType ctx t
  if sigma == sigma'
  then pure ()
  else throwE $ "Type mismatch; expected " ++ show sigma ++ ", actual " ++ show sigma'