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