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