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 a
s 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!