(The full code used for this message is available at http://ryani.freeshell.org/haskell/systemf.hs) System F is the polymorphically typed lambda calculus. It is strongly typed but allows polymorphic functions like "id". id is represented as follows:
eId = EGamma "A" (ELam "x" TVar EVar)
which represents
\A -> \x:A -> x
that is, a function that takes a type and a single argument of that type and returns its argument. This embedding only allows well-typed terms to be constructed; the Haskell typechecker verifies that a term is well-typed. I include a full compiler which converts terms into Haskell functions (albeit not-very-efficient ones). A sample session with GHCi follows: GHCi, version 6.8.1: http://www.haskell.org/ghc/ :? for help Loading package base ... linking ... done. Ok, modules loaded: SystemF. Prelude SystemF> eId \A a:A -> a Prelude SystemF> :t eId eId :: NExpr (a :-> (a -> a)) Prelude SystemF> :t eBottom eBottom :: NExpr (a :-> a) Prelude SystemF> eBottom \A -> fix (\a:A -> a) Prelude SystemF> putStrLn $ showExprExplicit eBottom (EGamma "A" (EFix (ELam "a" TVar EVar))) Prelude SystemF> tInt I# Prelude SystemF> :t (TPrim "I#" (undefined :: Integer)) (TPrim "I#" (undefined :: Integer)) :: TypRep Integer ts Prelude SystemF> :t tInt tInt :: TypRep Integer ts Prelude SystemF> eK \A B a:A b:B -> a Prelude SystemF> eFact fix (\rec:(I#->I#) z:I# -> (\A -> if#) I# (eq# z 0) 1 (times# z (rec (minus# z 1)))) Prelude SystemF> :t eFact eFact :: NExpr (Integer -> Integer) Prelude SystemF> compile eFact 5 120 Prelude SystemF> putStrLn $ showExprExplicit eFat <interactive>:1:28: Not in scope: `eFat' Prelude SystemF> putStrLn $ showExprExplicit eFact (EFix (ELam "rec" (TArrow (TPrim I#) (TPrim I#)) (ELam "z" (TPrim I#) (EAp (EAp (EAp (ETypAp (EGamma "A" (EPrim if#)) (TPrim I#)) (EAp (EAp (EPrim eq#) EVar) (EPrim 0))) (EPrim 1)) (EAp (EAp (EPrim times#) EVar) (EAp (EPush EVar) (EAp (EAp (EPrim minus#) EVar) (EPrim 1)))))))) Prelude SystemF> :t (whnf (EAp eFact (EPrim "6" 6))) (whnf (EAp eFact (EPrim "6" 6))) :: Expr Integer NDecl NDecl Prelude SystemF> (whnf (EAp eFact (EPrim "6" 6))) if#*** Prelude SystemF> extractPrim (whnf (EAp eFact (EPrim "6" 6))) Just 720