Example of Invariant Functor?

Question

I'm reading documentation on monad layers package and my brain is going to boil up.

In the mmtl section of this document the author talks about invariant functor. It's method invmap is like fmap of Functor but it takes an inverse morphism (b -> a) also. I understand why author says that hoist of MFunctor is more powerful than tmap of Invariant but i don't see what's the point of that inverse morphism.

Is there any example of an Invariant which can't be an instance of Functor?

Answer 1

Here's a standard place where Invariant shows up---higher order abstract syntax (HOAS) for embedding lambda calculus. In HOAS we like to write expression types like

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

-- ((\x . x) (\x . x)) is sort of like
ex :: ExpF (ExpF a)
ex = App (Lam id) (Lam id)

-- we can use tricky types to make this repeat layering of `ExpF`s easier to work with

We'd love for this type to have structure like Functor but sadly it cannot be since Lam has as in both positive and negative position. So instead we define

instance Invariant ExpF where
  invmap ab ba (App x y) = App (ab x) (ab y)
  invmap ab ba (Lam aa)  = Lam (ab . aa . ba)

This is really tragic because what we would really like to do is to fold this ExpF type in on itself to form a recursive expression tree. If it were a Functor that'd be obvious, but since it's not we get some very ugly, challenging constructions.

To resolve this, you add another type parameter and call it Parametric HOAS

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

And we end up finding that we can build a free monad atop this type using its Functor instance where binding is variable substitution. Very nice!