[Haskell-cafe] Type-system fun: a type-safe embedding of System F Lambda Calculus into Haskell

[Ryan Ingram]

 (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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20071230/a081aec6/attachment.htm