## Thursday, July 31, 2014

### Rank-2 PHOAS

Lately I've been experimenting with finally-tagless (typed) representations and made an attempt to model the (implicitly typed) lambda calculus. However, I wanted to use the parametric higher-order abstract syntax (PHOAS) technique to obtain variable bindings that are automatically well-scoped.
I arrived at this formulation:

``` class LC rep where   var :: p → rep   lam :: (forall p . p → rep) → rep ```

(I am ignoring applications as they are not important for making my point.)
As Andres Löh has pointed out to me this is not the final-tagless formulation of the regular PHOAS form, as that would add the `p` type variable as the second class parameter and the rank-2 `forall` would appear from "outside".
But I liked my simple formulation and the obviously and explicitly parametric lambda body. So I started implementing a rudimentary visualisation instance given a name supply:

``` instance LC ([String] → String) where   var = ??? -- const "VAR"   lam f = \supply → ... ```

It turns out that implementing `var` is only possible by giving a constant result, and for `lam` I am in trouble, because I cannot call `f` as it expects a polymorphic argument. Both problems are due to the fact that `p` is too polymorphic. Can we have it a bit less polymorphic in order to make some progress?
Thinking about it I came up with the idea of giving each instance a way to constrain the `p` variable as it fits. So I changed `class LC` such:

``` class LC rep where   type Restricted rep p :: Constraint   var :: Restricted rep p ⇒ p → rep   lam :: (forall p . Restricted rep p ⇒ p → rep) → rep ```

Now my instance can pick the restriction as it fits:

``` instance LC ([String] → String) where   type Restricted ([String] → String) p = ([String] → String) ~ p   var = id   lam f = \supply → ... ```

As you see I chose the restriction to be type equality which essentially cancels parametricity in this instance and gives me simple HOAS. Filling in `p` becomes easy now.

```   lam f = \(n:ns) → "\\" ++ n ++ "." ++ (f \$ const n) ns ```

Let's try it out! But in order to do that we need an instance of `Show` for name supplies. This could be one:
``` instance Show ([String] → String) where   show f = f \$ map (('v':) . show) [0..] ```

Now we can interpret a lambda term as a name supply.
``` *Main› lam (\x → lam \$ \y → var x) :: [String] → String \v0.\v1.v0 ```

It works™ :-)

But I can go further. After implementing several other instances I observed that I always wanted to destroy parametricity completely and implement `var` as the identity. So why not have these as defaults and reduce the boilerplate by a nice margin? Here is the final class definition that I arrived at:

``` class LC rep where   type Restricted rep p :: Constraint   type Restricted rep p = rep ~ p   var :: Restricted rep p ⇒ p → rep   default var :: rep ~ p ⇒ p → rep   var = id   lam :: (forall p . Restricted rep p ⇒ p → rep) → rep ```

I like it so far.

PS: Here are the prerequisites if you want to compile the above yourself:
``` {-# LANGUAGE UnicodeSyntax, ConstraintKinds, TypeFamilies, RankNTypes, FlexibleInstances, DefaultSignatures #-} import GHC.Exts ```