# 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
```