Some examples
There are several standard Church-encoded monad transformers around. For example, ContT
is basically the Church encoding of the newtype:
newtype ContT r m a = ContT ((a -> m r) -> m r)
The type signature says that this Churchy type has one constructor of type a -> m r
.
But there are more complicated types than that. This one is inspired by LogicT
:
newtype LogicT r m a = LogicT (m r -> (a -> m r -> m r) -> m r)
LogicT
represents a Church-style list. This has two constructors:
- a nullary one,
m r
, corresponding to the end of the list ([]
) - a binary one,
a -> m r -> m r
corresponding to cons (:
)
LogicT
is again a monad, and I believe this is only possible of the particular structure of the list. It is similar to "ListT
done right".
We could go on with this list. Many Church constructions don’t offer anything new over ContT
. For example I believe that the Church encoding of a Reader
is just isomorphic to ContT r m (Reader e a)
. And probably the same holds for every newtype. But there are interesting constructions that I haven’t seen in the wild yet:
newtype ChurchEitherT e r m a = ChurchEitherT ((e -> m r) -> (a -> m r) -> m r)
Is this used anywhere? I bet it’s a monad.
General question
Given a functor like Identity
, []
or Either e
, is there an automatic construction that creates a Church encoded CPS-style monad transformer from it? What structures (e.g. Applicative
, Monad
, Alternative
, …) can be lifted to that construction?
Template Haskell
I’m sure this can be done in TH with enough patience somehow. But it sounds like a lot of tedious work.
Generics & associated type families
I am fairly sure that it should be possible to define this using GHC.Generics
, with something like this:
newtype ChurchT r f m a = ChurchT {getChurchT :: Constructors f a -> m r}
class HasChurch f where
type Constructors f :: (* -> *)
liftChurch :: f a -> ChurchT r f m a
instance (HasChurch f, HasChurch g) => HasChurch (f :+: g) where
type Constructors (f :+: g) = Product (Constructors f) (Constructors g)
liftChurch (L1 a) = ChurchT $ \(Pair fa _) -> getChurchT (liftChurch a) fa
liftChurch (R1 a) = ChurchT $ \(Pair _ ga) -> getChurchT (liftChurch a) ga
But I haven’t worked it out completely yet. For example, in the Constructors
type, m
and r
should also appear, but I haven’t figured out how to navigate in partially applied type families and the like. I also don’t understand yet whether one can actually lift e.g. Monad
. In other words, does this exist:
instance (Monad f, Monad m) => Monad (ChurchT r f m a)
If yes, we’d have a new generic way to combine two monads. (I’d suspect that this must be known already, if it works.)
Directly as a type constructor
It would be awesome if one could write a datatype that generalises ContT
in some way such that it is the Church encoding of a type constructor. Like type ChurchT r f m a = ContT r m (f a)
, but cleverer and correct for the multi-constructor case. I’m not sure this can work. But if it could, it would be mind-boggling for sure.