Name Binding in EDSLs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}

I’ve recently become interested in building DSLs that have the ability to create binders, as Edward Kmett suggests that this is a good way to model graph-like structures in Haskell. There appear to be a wide array of different techniques, and in this page I’m capturing my notes as I learn how each of these work.

PHOAS

Parametric Higher-Order Abstract Syntax (PHOAS) is work from Adam Chlipala, published at ICFP 2008.

PHOAS and the Simply Typed Lamba Calculus

I have seen (and am able to write) syntax trees using PHOAS, but I’m interested in more guarantees - namely that expressions are well typed. The following is a translation of an implementation of the simply typed lambda calculus, from Adam’s paper.

Types are either the base type - Bool - or type arrows. We use -XDataKinds to promote this declaration to the type level.

data Ty = TyBool | TyArr Ty Ty

Now we can use type information as we build up terms:

data PTerm :: (Ty -> *) -> Ty -> * where
Var :: v t -> PTerm v t
Tru :: PTerm v 'TyBool
Fals :: PTerm v 'TyBool
App :: PTerm v ('TyArr t1 t2) -> PTerm v t1 -> PTerm v t2
Abs :: (v t1 -> PTerm v t2) -> PTerm v ('TyArr t1 t2)

Now we use parametricity to limit us to only variable introduction through Abs.

newtype Term t = Term (forall v. PTerm v t)

We can do a few things with this. The obvious choice is an evaluator. We need a way to go from the type description to a type in the host language,

type family InterpTy (t :: Ty) :: * where
InterpTy 'TyBool = Bool
InterpTy ('TyArr x y) = InterpTy x -> InterpTy y

We also need to choose a functor for variables. We can use a variant of Id - however we need to translate from our embedded language into types in the host language:

newtype V a = V { unV :: InterpTy a }
eval :: Term t -> InterpTy t
eval (Term pterm) = eval' pterm
where
eval' :: PTerm V t -> InterpTy t
eval' (Var a) = unV a
eval' Tru = True
eval' Fals = False
eval' (App x y) = (eval' x) (eval' y)
eval' (Abs f) = eval' . f . V

Example usage

eval (Term (App (App (Abs (\x -> (Abs \y -> Var x))) Tru) Fals))
True

An interesting aspect in PHOAS comes from the use of the higher-rank type. This lets us choose any type of variable we want, which can lead to more interesting inteprerations of expressions. For example, depsite using a Haskell function, we can still show this function:

data Const a b = Const a

showT :: Term t -> String
showT (Term pterm) = show' 'a' pterm
where
show' :: Char -> PTerm (Const Char) t -> String
show' _ (Var (Const c)) = [c]
show' _ Tru = "True"
show' _ Fals = "False"
show' s (App x y) = "(" ++ show' s x ++ ") " ++ show' s y
show' s (Abs f) = [s] ++ ". " ++ show' (succ s) (f (Const s))

Evaluating the above expression through showT produces:

shoW (Term (App (App (Abs (\x -> (Abs \y -> Var x))) Tru) Fals))
((a. b. a) True) False