λbje - Church encoding of a monoid

This article shows how a Church encoding can be derivied from an abstract data type, and intuitively but not rigorously demonstrates their equivalence.

{-# LANGUAGE GADTs, RankNTypes #-}

We start out by defining a sum type for a monoid, with empty, embed, and append operations. To ease the transformation to Church encoding, we use GADTs to give explicit type signatures to the three constructors.

data MonoidAST a where
    MEmbed :: a -> MonoidAST a
    MEmpty :: MonoidAST a
    MAppend :: MonoidAST a -> MonoidAST a -> MonoidAST a

A Church encoding represents the interpretation of a data structure; for each construction in the type, the Church encoding will require a function to interpret that construction. Thus, the Church encoding of the above structure can be obtained by replacing MonoidAST a with a type variable $r$ , and describing a function which takes one function for each of the ADT constructors, finally returning an $r$ :

newtype CEMonoid a = CEMonoid { mrun ::
    forall r.        -- ≡ MonoidAST
    (a -> r)         -- ≡ MEmbed
    -> r             -- ≡ MEmpty
    -> (r -> r -> r) -- ≡ MAppend
    -> r }

The mrun function will take a Church encoded monoid and the functions for each interpretation, and produce a monoidal value. If we consider CEMonoid Int, we might wish to take the sum monoid (mrun _ id 0 (+)) or the product monoid (mrun _ id 1 (*)). Of special note here is that $a$ and $r$ are not necessarily the same type. We could execute a monoid which first transforms the integer value to something else, such as mrun _ show "" (++).

Now we have a way to execute a monoid, but not to construct one. We provide functions for constructors, effectively taking the lower-case of the ADT’s constructors:

membed' a = CEMonoid $ \ d _ _ -> d a
mempty' = CEMonoid $ \ _ e _ -> e
mappend' a b = CEMonoid $ \ d e f -> f (mrun a d e f) (mrun b d e f)

To demonstrate the equivalence of these constructors to the ADT’s value constructors, we can inspect the types of the functions and observe their similarity to the ADT:

:t mempty'
:t membed'
:t mappend'

mempty’ :: forall a. CEMonoid a

membed’ :: forall a. a -> CEMonoid a

mappend’ :: forall a. CEMonoid a -> CEMonoid a -> CEMonoid a

Now we have all the elements in place to create and run a few monoids:

let mon = membed' 5 `mappend'` membed' 3 in
    (mrun mon id 0 (+), mrun mon id 1 (*), mrun mon show "" (++))

(8,15,"53")

When transforming to the Church encoding, at the type level we exchanged a definition of how to construct the type for a definition of how to interpret the type, and needed to provide functions to construct values in the type.

Conversely, the ADT describes at the type level how to construct values, and so needs a function to interpret those values:

runM MEmpty d e f = e
runM (MEmbed a) d e f = d a
runM (MAppend a b) d e f = f (runM a d e f) (runM b d e f)
:t runM
let mon = MEmbed 3 `MAppend` MEmbed 5 in
    (runM mon id 0 (+), runM mon id 1 (*), runM mon show "" (++))

runM :: forall t t1. MonoidAST t -> (t -> t1) -> t1 -> (t1 -> t1 -> t1) -> t1

(8,15,"35")