9 Dec 2013

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