Untyped lambda-calculus (Haskell)

gistfile1.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
data Nat = Z | Suc Nat

data Fin n where
    FZ :: Fin (Suc n)
    FS :: Fin n -> Fin (Suc n)

inj :: Fin n -> Fin (Suc n)
inj FZ = FZ
inj (FS f) = FS (inj f)

data Exp n where
    Var :: Fin n -> Exp n
    Lam :: Exp (Suc n) -> Exp n
    (:@:) :: Exp n -> Exp n -> Exp n

Example usage:

_flip :: Exp Z
_flip = Lam $ Lam $ let x = Var (FS FZ)
                        f = Var (inj FZ)
                    in f :@: x

Actually you don't even need the injection there:

_flip :: Exp Z
_flip = Lam $ Lam $ let x = Var (FS FZ)
                        f = Var FZ
                    in f :@: x