Type-safe reification of simply typed lambda terms with atomic types E (entity) and T (boolean) into Haskell functions. I could extend this by replacing these atomic types with a user-provided universe, but then we couldn't encode propositional logic anymore.

STL.hs

{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, DataKinds #-}
{-# LANGUAGE KindSignatures, TypeOperators, MultiParamTypeClasses #-}

module STL where

import Prelude hiding (True,False)
import qualified Data.Bool as B

type Name = String
type Entity = Int

data Nat where
  Nz :: Nat
  Ns :: Nat -> Nat

data Nat' (n :: Nat) where
  Nz' :: Nat' Nz
  Ns' :: Nat' n -> Nat' (Ns n)

data Type where
  E :: Type
  T :: Type
  (:->:) :: Type -> Type -> Type

type family LookupByNat (n :: Nat) (c :: [Type]) :: Type
type instance LookupByNat Nz (t ': ts) = t
type instance LookupByNat (Ns n) (t ': ts) = LookupByNat n ts

lookupByNat :: Env c -> Nat' n -> Hask (LookupByNat n c)
lookupByNat (Cons e _) (Nz') = e
lookupByNat (Cons _ es) (Ns' n) = lookupByNat es n

data Env :: [Type] -> * where
  Nil  :: Env '[]
  Cons :: Hask t -> Env c -> Env (t ': c)

data Exp :: [Type] -> Type -> * where
  Var :: Nat' n -> Exp c (LookupByNat n c)
  Abs :: Exp (t1 ': c) t2 -> Exp c (t1 :->: t2)
  App :: Exp c (t1 :->: t2) -> Exp c t1 -> Exp c t2

  True   :: Exp c T
  False  :: Exp c T
  Not    :: Exp c T -> Exp c T
  (:/\:) :: Exp c T -> Exp c T -> Exp c T
  (:\/:) :: Exp c T -> Exp c T -> Exp c T
  (:=>:) :: Exp c T -> Exp c T -> Exp c T
  (:==:) :: Exp c T -> Exp c T -> Exp c T

type family Hask (t :: Type) :: *
type instance Hask T = Bool
type instance Hask E = Entity
type instance Hask (t1 :->: t2) = Hask t1 -> Hask t2

reify :: Env c -> Exp c t -> Hask t
reify c (Var n)      = lookupByNat c n
reify c (Abs e1)     = \x -> reify (Cons x c) e1
reify c (App e1 e2)  = (reify c e1) (reify c e2)
reify _  True        = B.True
reify _  False       = B.False
reify c (Not e1)     = not (reify c e1)
reify c (e1 :/\: e2) = reify c e1 && reify c e2
reify c (e1 :\/: e2) = reify c e1 || reify c e2
reify c (e1 :=>: e2) = not (reify c e1) || reify c e2
reify c (e1 :==: e2) = reify c e1 == reify c e2

type Zero  = Nat' 'Nz
type One   = Nat' ('Ns 'Nz)
type Two   = Nat' ('Ns ('Ns 'Nz))
type Three = Nat' ('Ns ('Ns ('Ns 'Nz)))
type Four  = Nat' ('Ns ('Ns ('Ns ('Ns 'Nz))))
type Five  = Nat' ('Ns ('Ns ('Ns ('Ns ('Ns 'Nz)))))
type Six   = Nat' ('Ns ('Ns ('Ns ('Ns ('Ns ('Ns 'Nz))))))
type Seven = Nat' ('Ns ('Ns ('Ns ('Ns ('Ns ('Ns ('Ns 'Nz)))))))
type Eight = Nat' ('Ns ('Ns ('Ns ('Ns ('Ns ('Ns ('Ns ('Ns 'Nz))))))))
type Nine  = Nat' ('Ns ('Ns ('Ns ('Ns ('Ns ('Ns ('Ns ('Ns ('Ns 'Nz)))))))))

zero  :: Zero
zero  = Nz'
one   :: One
one   = Ns' zero
two   :: Two
two   = Ns' one
three :: Three
three = Ns' two
four  :: Four
four  = Ns' three
five  :: Five
five  = Ns' four
six   :: Six
six   = Ns' five
seven :: Seven
seven = Ns' six
eight :: Eight
eight = Ns' seven
nine  :: Nine
nine  = Ns' eight

id :: Exp '[] (E :->: E)
id = Abs (Var zero)

const :: Exp '[] (E :->: (E :->: E))
const = Abs (Abs (Var one))