---
format: markdown+lhs
...
> {-# 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](https://www.reddit.com/r/haskell/comments/29c9dt/interpreters_how_should_it_be_done/ciji6ch)
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
```