Automatic Church encoding of datatypes as monad transformers?

Learn
#1

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:

  1. a nullary one, m r, corresponding to the end of the list ([])
  2. 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.

2 Likes
#2

I don’t quite understand this. The newtype you show is ContT. I don’t think you intended to say that it is the Church encoding of itself, but I can’t quite grasp what you did intend to say.

#3

Maybe "ContT is basically the Church encoding of m"?

#4

Sorry, I was very terse here. I used the word “newtype” in two distinct contexts. It’s just a coincidence that I also used newtype in the code, because it is idiomatic.

Church encoding basically says "look at the types of all the constructors, say a -> b -> t, c -> t, d -> e -> f -> t, and then write a CPS version of the type t you want to encode: forall x . (a -> b -> x) -> (c -> x) -> (d -> e -> x) -> x. In this case I have chosen not to do forall x, and instead replaced x by m r. (One could later still do forall m r, and indeed LogicT does at least forall r.)

Now if I create a newtype, it has one constructor with one argument. For example, a well-known newtype from base:

newtype Identity a = Identity a

The type of (the constructor) Identity is a -> Identity a. So if I were to make a Church encoding of the type Identity, it would look like forall x . (a -> x) -> x. And now if I insert m r for x, I get ContT r m a. That’s why I said that ContT is the Church encoding of the newtype, meaning any newtype like e.g. Identity.

2 Likes
#5

I’d try tackling this one with generics-sop. Having the types in a list instead of a tree will fit nicely with the functions you’re going to want to work with.

I think you can ignore the m part while doing your lifting. That only comes up writing the MonadLift instance for these types. Start building the nontransformer version first and you should be able to get the transformer version more easily afterwards.

2 Likes
#6

I tried, but so far it’s a mess with ambiguous types. Probably one needs to understand the heterogeneous generic classes like HAp and so on.

#7

You don’t have to use the confusing combinations, you can just use the more convenient Rep types.

#8

You may be interested in codensity transformation. It’s not quite the same thing as Church encoding, but you’ll find it informative if you haven’t run into it already.

3 Likes