# Automatic Church encoding of datatypes as monad transformers?

**URL:** <https://discourse.haskell.org/t/automatic-church-encoding-of-datatypes-as-monad-transformers/7094>\
**Category:** Learn\
**Created:** [July 25, 2023, 9:26am UTC](https://discourse.haskell.org/t/automatic-church-encoding-of-datatypes-as-monad-transformers/7094 "2023-07-25T09:26:52Z")\
**Posts on this page:** 8\
**Page:** 1

<div class="post-metadata">

**Author:** ![turion](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/turion/32/989_2.png) [@turion](https://discourse.haskell.org/u/turion)\
**Post date:** [July 25, 2023, 9:26am UTC](https://discourse.haskell.org/t/automatic-church-encoding-of-datatypes-as-monad-transformers/7094/1 "2023-07-25T09:26:52Z")

</div>

## Some examples

There are several standard Church-encoded monad transformers around. For example, `ContT` is basically the Church encoding of the newtype:

```haskell
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`](https://hackage.haskell.org/package/logict):

```haskell
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:

```haskell
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`](https://hackage.haskell.org/package/base/docs/GHC-Generics.html), with something like this:

```haskell
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:

```haskell
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.

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [July 25, 2023, 11:14am UTC](https://discourse.haskell.org/t/automatic-church-encoding-of-datatypes-as-monad-transformers/7094/2 "2023-07-25T11:14:19Z")

</div>

> [@turion](#):
>
> For example, `ContT` is basically the Church encoding of the newtype:
> 
> ```haskell
> newtype ContT r m a = ContT ((a -> m r) -> m r)
> 
> ```

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.

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [July 25, 2023, 11:28am UTC](https://discourse.haskell.org/t/automatic-church-encoding-of-datatypes-as-monad-transformers/7094/3 "2023-07-25T11:28:21Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![turion](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/turion/32/989_2.png) [@turion](https://discourse.haskell.org/u/turion)\
**Post date:** [July 25, 2023, 11:37am UTC](https://discourse.haskell.org/t/automatic-church-encoding-of-datatypes-as-monad-transformers/7094/4 "2023-07-25T11:37:02Z")

</div>

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`:

```haskell
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`.

---

<div class="post-metadata">

**Author:** ![glguy](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/glguy/32/3359_2.png) [@glguy](https://discourse.haskell.org/u/glguy)\
**Post date:** [July 25, 2023, 3:35pm UTC](https://discourse.haskell.org/t/automatic-church-encoding-of-datatypes-as-monad-transformers/7094/5 "2023-07-25T15:35:39Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![turion](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/turion/32/989_2.png) [@turion](https://discourse.haskell.org/u/turion)\
**Post date:** [July 25, 2023, 6:34pm UTC](https://discourse.haskell.org/t/automatic-church-encoding-of-datatypes-as-monad-transformers/7094/6 "2023-07-25T18:34:56Z")

</div>

> [@glguy](#):
>
> I’d try tackling this one with generics-sop

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.

---

<div class="post-metadata">

**Author:** ![glguy](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/glguy/32/3359_2.png) [@glguy](https://discourse.haskell.org/u/glguy)\
**Post date:** [July 25, 2023, 7:55pm UTC](https://discourse.haskell.org/t/automatic-church-encoding-of-datatypes-as-monad-transformers/7094/7 "2023-07-25T19:55:07Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![blamario](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/blamario/32/860_2.png) [@blamario](https://discourse.haskell.org/u/blamario)\
**Post date:** [July 26, 2023, 5:50pm UTC](https://discourse.haskell.org/t/automatic-church-encoding-of-datatypes-as-monad-transformers/7094/8 "2023-07-26T17:50:35Z")

</div>

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.