Language.Lambda.SystemF.TypeCheck

Documentation

type UniqueSupply n = [n]

type Context' n t = Map n t

typecheck :: (Ord name, Pretty name) => SystemFExpr name name -> Typecheck name (Ty name)

typecheckVar :: Ord name => name -> Typecheck name (Ty name)

typecheckAbs :: (Ord name, Pretty name) => name -> Ty name -> SystemFExpr name name -> Typecheck name (Ty name)

typecheckApp :: (Ord name, Pretty name) => SystemFExpr name name -> SystemFExpr name name -> Typecheck name (Ty name)

typecheckTyAbs :: (Ord name, Pretty name) => name -> SystemFExpr name name -> Typecheck name (Ty name)

typecheckTyApp :: (Ord name, Pretty name) => SystemFExpr name name -> Ty name -> Typecheck name (Ty name)

unique :: Typecheck name name

substitute :: Eq n => Ty n -> n -> SystemFExpr n n -> SystemFExpr n n

substituteTy :: Eq name => Ty name -> name -> Ty name -> Ty name

tyMismatchError :: (Pretty t1, Pretty t2) => t1 -> t2 -> LambdaException