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