Embedding System F

SystemF.markdown

Embedding F with a twist.

First we witness membership (I follow Richard's lead here, make sure to check out his dissertation for more info):

import Data.Kind

data Elem :: [a] -> a -> Type where
  EZ :: Elem (x:xs) x
  ES :: Elem    xs  x
     -> Elem (y:xs) x

-- Example
ex :: Elem [Int, Bool, (), Double] ()
ex = ES (ES EZ)

And now we can implement standard encoding of a typed lambda calculus

data Exp :: [Type] -> Type -> Type where
  Var :: Elem xs a -> Exp xs a
  Lam :: Exp (x:xs) a -> Exp xs (x -> a)
  App :: Exp xs (a -> b) -> (Exp xs a -> Exp xs b)

so we can capture functions as

expId :: Exp '[] (a -> a)
expId = Lam (Var EZ)

but we lack the polymorphism of System F, we cannot define “Exp '[] (forall x. x -> x).