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