(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