PHOAS For Free

9 Dec 2013 Edward Kmett View Markdown source

As of March 2020, School of Haskell has been switched to read-only mode.

Sections

Back in 2008 I wrote an article entitled "Rotten Bananas" about how to convert between the different forms of catamorphisms over "exponential" data types that arise when we go to work with Higher Order Abstract Syntax (HOAS).

Today I want to go back and revisit that post in light of my current understanding of profunctors from working on lens.

My goal today is to go through and reformulate Parametric HOAS slightly differently by using profunctors to tease apart the positive and negative occurences of the type variable.

By doing so, we can show the connection between Fegaras and Sheard's catamorphism and the free monad that laid so close to the surface in the original formulation, and we can derive a variant on Weirich and Washburn's efficient catamorphism by using an alternate encoding of the free monad that I've already blogged about before in my series on "Free Monads for Less".

Folding Invariants

If we take the base functor for an expression type that has both positive and negative occurences of a variable, there isn't much we can do with our standard tools. It isn't even a Functor, so it can't be Foldable or Traversable, Applicative or a Monad.

data ExpF a
  = App a a
  | Lam (a -> a)

To work with it, you can define a rather unsatisfying

class Invariant f where
  invmap :: (a -> b) -> (b -> a) -> f a -> f b
  
instance Invariant ExpF where
  invmap ab ba (App x y) = App (ab x) (ab y)
  invmap ab ba (Lam aa)  = Lam (ab.aa.ba)

I described this in my 2008 post as ExpFunctor, based on a similar operation in Weirich and Washburn. It is packaged up in the invariant package on Hackage as Invariant, with a method named invmap, if you find you really want to use it.

One of my goals today is to show that we can get away without it!

Erik Meijer and Graham Hutton showed in "Bananas in Space" that you can define a catamorphism over that data type if you can also define a corresponding anamorphism that serves as its inverse. E.g. to define a pretty printer for this type with Meijer/Hutton's catamorphism you also need a parser. ಠ__ಠ

newtype Mu f = In { out :: f (Mu f) } 

cata :: Invariant f => (f a -> a) -> (a -> f a) -> Mu f -> a
cata f g (In x) = f (invmap (cata f g) (ana f g) x)

ana :: Invariant f => (f a -> a) -> (a -> f a) -> a -> Mu f
ana f g x = In (invmap (ana f g) (cata f g) (g x))

Fegaras and Sheard showed that if you change the domain of the problem a bit, you can get away with a 'fake' anamorphism, by adding a constructor that you agree never to use, because the anamorphism is only ever used as a right inverse to our catamorphism. They then proceeded to provide a type system for checking this. Adopting the notation from Weirich and Washburn's take on Fegaras and Sheard's catamorphism, this would be:

data Rec f a = Place a | Roll (f (Rec f a))

cata :: Invariant f => (f a -> a) -> Rec f a -> a
cata f (Roll x) = f (invmap (cata f) Place x)
cata f (Place x) = x

You can clearly see that Place forms a right inverse of cata f:

cata f . Place = id

Now you can define smart constructors for the running Exp example, using Roll.

type Exp = Rec ExpF

lam :: (Exp a -> Exp a) -> Exp a
lam f = Roll (Lam f)

app :: Exp a -> Exp a -> Exp a
app x y = Roll (App x y)

Weirich and Washburn noted that you can prevent the accidental use of the type parameter a by quantifying over it.

Finally, Weirich and Washburn reimplemented Rec.

type Rec f a = (f a -> a) -> a

This made cata ridiculously simple:

cata :: (f a -> a) -> Rec f a -> a
cata f x = x f

But we don't have Roll any more, so we need to move the complexity into an explicit roll combinator:

roll :: Invariant f => f (Rec f a) -> Rec f a
roll x f = f (invmap (cata f) place x)

We no longer have Place either, but nothing says (f a -> a) -> a has to use the supplied function, when we know a!

place :: a -> Rec f a
place = const

Then we can see:

type Exp a = Rec ExpF a

lam :: (Exp a -> Exp a) -> Exp a
lam f = roll (Lam f)

app :: Exp a -> Exp a -> Exp a
app x y = roll (App x y)

var :: a -> Exp a
var = place

Again, in particular in both the Fegaras-Sheard and Weirich-Washburn forms, you can denote a closed term safely using

type ClosedExp = forall x. Exp x

The safety of this is really the subject of the "Boxes Go Bananas" paper.

Based on the observations about the price of substitution into free monads by Janis Voigtländer, one should probably favor Weirich and Washburn's construction if you're going to be doing substitution on your HOAS representation -- and if you're not doing substitution, then why are you using HOAS in the first place?!

Weak HOAS

Everything I've mentioned above is a "strong" HOAS variants. You can perform substitution just by passing in the expression you want.

In weak HOAS (and PHOAS) the decision is made to deal with negative occurences differently than in what we've done so far.

Instead of taking a full Exp a in negative position, we're just going to take an a.

Written monolithically, it would look something like:

data Exp a
  = Var a
  | Lam (a -> Exp a)
  | App (Exp a) (Exp a)

Then our smart constructors change a bit:

lam :: (Exp a -> Exp a) -> Exp a

weakens to

lam :: (a -> Exp a) -> Exp a

We still have both positive and negative occurences of a, but we no longer have Exp occurring in both positive and negative position.

This is particularly popular in the Coq and Agda communities because it can pass the positivity checker, but unlike strong HOAS can be a bit more painful to work with.

Parametric HOAS

Adam Chlipala does a lot of work with Parametric HOAS, which is based on a weak HOAS variant of Weirich and Washburn's Boxes Go Bananas: Encoding Higher-Order Abstract Syntax with Parametric Polymorphism, which I talked about in that post. His Lambda Tamer is based on this model.

One issue is that neither of these really gives us a free Monad, due to the fact that the a occurs in both positive and negative position and so we can't even derive a Functor instance.

Adam's work doesn't really feel this pinch, because in Coq he can define custom tactics for ltac to use and you generally don't try to factor out this pattern into a library, but when you switch to Agda and have to do everything by hand, the lack of common abstractions comes to bite you.

P is for Profunctor

Dan Piponi wrote a nice article on Profunctors in Haskell introducing profunctors to the Haskell community, and they now form the basis of much of lens. Liyang HU also has a more tongue in cheek introduction here on the School of Haskell that he originally presented back in April at a benkyoukai about various libraries of mine in Japan.

To say something is a Profunctor in Haskell is just to say it is contravariant in the first argument and covariant in the second.

class Profunctor p where
  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d

This argument order is a bit reversed from how it is usually tackled in category theory, but by lining things up this way we match up with the variances for Arrow and (->).

For convenience we also provide class methods for:

lmap :: Profunctor p => (a -> b) -> p b c -> p a c
rmap :: Profunctor p => (b -> c) -> p a b -> p a c

Notice when I wrote the Weak HOAS definition, I had to keep it monolithic? To factor out Var / Place, it winds up needing two type parameters, since now both a and Exp a occur inside the expression.

So, if we go back to the start and separate positive and negative occurences of these, we're left with something like

data ExpF a b 
  = App b b 
  | Lam (a -> b)

This forms a valid Profunctor.

instance Profunctor ExpF where
  dimap f g (App x y) = App (g x) (g y)
  dimap f g (Lam h)   = Lam (g.h.f)

PHOAS Is Free

Now we can revisit the Exp we were talking about in the section on Weak HOAS and we can rip apart the old:

data Exp a
  = Var a
  | Lam (a -> Exp a)
  | Abs (Exp a) (Exp a)

into the application of a Fegaras and Sheard free-monad-like construction

data Rec p a b
  = Place b
  | Roll (p a (Rec p a b))

to our base profunctor ExpF, so now

type Exp = Rec ExpF

But now, we're no longer free-monad like, we're actually a free monad!

We can even define this Monad, by cribbing the definition from free.

instance Profunctor p => Monad (Rec p a) where
  return = Place
  Place b  >>= f = f b
  Roll bs >>= f = Roll $ rmap (>>= f) bs

This Monad even performs capture avoiding substitution.

The Fegaras-Sheard catamorphism doesn't change much

cata :: Profunctor p => (p a b -> b) -> Rec p a b -> b
cata phi (Place b)  = b
cata phi (Roll bs) = phi (rmap (cata phi) bs)

However, it now just turns a p a-algebra into a Rec p a-algebra, and doesn't need to use Place at all!

And we get weak HOAS style smart constructors:

lam :: (a -> Exp a b) -> Exp a b
lam f = Roll (Lam f)

app :: Exp a b -> Exp a b -> Exp a b
app x y = Roll (App x y)

Now, var is the only thing that crosses the streams and causes the two type arguments to unify

var :: b -> Exp a b
var = return

Notice the difference between the type of the argument of lam and the signature of var. This causes actual expressions that use any variable they bind to wind up with the types agreeing:

foo :: Exp a a
foo = lam $ \x -> lam $ \y -> app (var x) (var y)

Take The End

Now instead of talking about a closed term in terms of quantifying over a single parameter that can only vary with an isomorphism, we take an end over our Profunctor instead:

type End p = forall x. p x x

iter0 :: Profunctor p => (p a a -> a) -> End (Rec p) -> a
iter0 phi x = cata phi x

I intend to write up a post on how to "read" universal properties as types, to help folks see where this definition for End comes from.

This was the Free monad I just said you probably don't want to use for substitution, so let's go try the other one.

Boxes Go Bananas For Less

Recall Weirich and Washburn's Rec:

type Rec f a = (f a -> a) -> a

When we go to turn that into a Profunctor directly we get stuck.

We could make

newtype Rec p a b = Rec { runRec :: (p a b -> a) -> b }

and get the variances right for a Profunctor.

instance Profunctor p => Profunctor (Rec p) where
  dimap f g (Rec h) = Rec $ \pab2a -> g $ h $ f . pab2a . dimap f g

But this doesn't look much like the instance I derived from Fegaras and Sheard's construction, and doesn't give us a Monad!

They could pull this off because a and b were interchangeable in either direction. We're a bit more constrained.

We could turn to Codensity of my weak variant of the Fegaras-Sheard construction, but as I've blogged about before, Codensity (Free f) is bigger than it needs to be.

Fortunately, that same series ended showing how you can get there with just Yoneda. Armed with that, we can borrow the Church-Free monad and get a Weirich and Wasburn-style Profunctor for Rec.

data Rec p a b = Rec 
  { runRec :: forall r. 
    (b -> r) -> (p a r -> r) -> r 
  }

instance Profunctor p => Profunctor (Rec p) where
  dimap f g m = Rec $ \kp kf -> runRec m (kp.g) (kf.lmap f)

We retain the Monad we won by splitting our type parameters in the weak Fegaras-Sheard variant above:

instance Profunctor p => Monad (Rec p a) where
  return b = Rec $ \ br _ -> br b
  m >>= f  = Rec $ \kp kf -> 
    runRec m (\a -> runRec (f a) kp kf) kf

and we can define the rest of the catamorphism machinery:

type End p = forall x. p x x

cata :: Profunctor p => (p a b -> b) -> Rec p a b -> b
cata phi m = runRec m id phi

roll :: Profunctor p => p a (Rec p a b) -> Rec p a b
roll w = Rec $ \kp kf -> kf (rmap (\r -> runRec r kp kf) w)

iter0 :: Profunctor p => (p a a -> a) -> End (Rec p) -> a
iter0 phi x = cata phi x

Now we can put together our smart constructors

lam :: (a -> Exp a b) -> Exp a b
lam f = roll (Lam f)

app :: Exp a b -> Exp a b -> Exp a b
app x y = roll (App x y)

var :: b -> Exp a b
var = return

and we can build expressions

foo :: Exp a a
foo = lam $ \x -> lam $ \y -> app (var x) (var y)

Conclusion

There is a lot more we can play with here.

Many expression types will admit a Strong instance. Now that we've split the input and output parameters can we perhaps use that or something like it to more easily manipulate environments?

Just like with bound we can build an indexed version of this construction that permits us to write strongly typed EDSLs. That is how PHOAS is usually presented in Coq after all.

There is also probably a lot more to be said about dinaturality here.

I still generally prefer working with bound to working in HOAS these days, because it is much easier to work under lambdas, and it is easier to grab all your free variables using Foldable and Traversable and harder to make mistakes with.

That said it is good to finally be able to merge together the notion of Fegaras and Sheard's construction and the standard free monad.

This also strikes me as a good first step towards being able to turn PHOAS into something that can be encoded usefully in Haskell as a library rather than a design pattern.

-[-](-)Edward Kmett

September 18th, 2013

comments powered by Disqus