Church

churchEncode and churchDecode form an isomorphism between a type and its church representation of a type Simply define an empty instance of Church (or using DeriveAnyClass) for a type with a Generic instance and defaulting magic will take care of the rest. For example:

 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveAnyClass #-}
 data MyType = Foo Int Bool | Bar | Baz Char deriving (Generic, Church, Show)

>>> churchEncode (Foo 1 True) (\int bool -> int + 1) 0 (const 1)
2

>>> churchDecode (\foo bar baz -> bar) :: MyType
Bar

Recursive datastructures only unfold one level:

data Nat = Z | S Nat deriving (Generic,Church,Show)

>>> :t churchEncode N
r -> (Nat -> r) -> r

But we can still write recursive folds over such data:

nat2int :: Nat -> Int
nat2int a = churchEncode a 0 ((+1) . nat2int)

>>> nat2int (S (S (S Z)))
3

Decoding recursive data is more cumbersome due to the Rep wrappings, but fortunately should not need to be done by hand often.

decodeNat :: (Rep Nat () -> (Rep Nat () -> Rep Nat ()) -> Rep Nat ()) -> Nat decodeNat k = churchDecode (z s -> k z (s . to))

>>> decodeNat (\z s -> s . s . s . s $ z)
S (S (S (S Z)))

Documentation

type ChurchRep t r = ChurchSum (ToList (StripMeta (Rep t ())) (ListTerm ())) r

This is the central type for this package. Unfortunately, it's built around type families so it's not so easy to read. A helpful algorithm for figuring out what the ChurchRep of a type Foo is,

1. For each constructor, write out its type signature
2. Replace the Foo at the end of each signature with r
3. Join these type signatures together with arrows (a -> b -> r) -> r -> ...
4. Append a final -> r to the end of this

For example, for Maybe

1. Nothing :: Maybe a and Just :: a -> Maybe a.
2. We then have r and a -> r.
3. Joining these gives r -> (a -> r)
4. r -> (a -> r) -> r is our church representation

class Church a where

Minimal complete definition

Nothing

Methods

churchEncode :: forall r. a -> ChurchRep a r

Reify a type to its church representation

churchEncode :: forall r. (Generic a, GStripMeta (Rep a ()), GList (StripMeta (Rep a ())) (ListTerm ()), GChurchSum (ToList (StripMeta (Rep a ())) (ListTerm ())) r) => a -> ChurchRep a r

Reify a type to its church representation

churchDecode :: ChurchRep a (Rep a ()) -> a

Create a value from its church representation. This method may require an explicit signature.

churchDecode :: (Generic a, GBuild (MakePaths (Rep a ()) '[] '[]) (ChurchRep a (Rep a ())) (Rep a ())) => ChurchRep a (Rep a ()) -> a

Create a value from its church representation. This method may require an explicit signature.

Instances

Church Bool

Defined in Church

Methods

churchEncode :: Bool -> ChurchRep Bool r

churchDecode :: ChurchRep Bool (Rep Bool ()) -> Bool

Church Ordering

Defined in Church

Methods

churchEncode :: Ordering -> ChurchRep Ordering r

churchDecode :: ChurchRep Ordering (Rep Ordering ()) -> Ordering

Church ()

Defined in Church

Methods

churchEncode :: () -> ChurchRep () r

churchDecode :: ChurchRep () (Rep () ()) -> ()

Church [a]

Defined in Church

Methods

churchEncode :: [a] -> ChurchRep [a] r

churchDecode :: ChurchRep [a] (Rep [a] ()) -> [a]

Church (Maybe a)

Defined in Church

Methods

churchEncode :: Maybe a -> ChurchRep (Maybe a) r

churchDecode :: ChurchRep (Maybe a) (Rep (Maybe a) ()) -> Maybe a

Church (Either a b)

Defined in Church

Methods

churchEncode :: Either a b -> ChurchRep (Either a b) r

churchDecode :: ChurchRep (Either a b) (Rep (Either a b) ()) -> Either a b

Church (a, b)

Defined in Church

Methods

churchEncode :: (a, b) -> ChurchRep (a, b) r

churchDecode :: ChurchRep (a, b) (Rep (a, b) ()) -> (a, b)

Church (a, b, c)

Defined in Church

Methods

churchEncode :: (a, b, c) -> ChurchRep (a, b, c) r

churchDecode :: ChurchRep (a, b, c) (Rep (a, b, c) ()) -> (a, b, c)

Church (a, b, c, d)

Defined in Church

Methods

churchEncode :: (a, b, c, d) -> ChurchRep (a, b, c, d) r

churchDecode :: ChurchRep (a, b, c, d) (Rep (a, b, c, d) ()) -> (a, b, c, d)

Church (a, b, c, d, e)

Defined in Church

Methods

churchEncode :: (a, b, c, d, e) -> ChurchRep (a, b, c, d, e) r

churchDecode :: ChurchRep (a, b, c, d, e) (Rep (a, b, c, d, e) ()) -> (a, b, c, d, e)

Church (a, b, c, d, e, f)

Defined in Church

Methods

churchEncode :: (a, b, c, d, e, f) -> ChurchRep (a, b, c, d, e, f) r

churchDecode :: ChurchRep (a, b, c, d, e, f) (Rep (a, b, c, d, e, f) ()) -> (a, b, c, d, e, f)

Church (a, b, c, d, e, f, g)

Defined in Church

Methods

churchEncode :: (a, b, c, d, e, f, g) -> ChurchRep (a, b, c, d, e, f, g) r

churchDecode :: ChurchRep (a, b, c, d, e, f, g) (Rep (a, b, c, d, e, f, g) ()) -> (a, b, c, d, e, f, g)

churchCast :: forall a b. (Church a, Church b, ChurchRep a (Rep b ()) ~ ChurchRep b (Rep b ())) => a -> b

Since types with the same church representation are identical, we can cast between them.