Church-Encode a Datatype, Generically
Church-encoding of datatypes is a common pattern you’ll see in Haskell. It’s possible to do it generically, by using a sum-of-products encoding.
Some preamble:
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
module ChurchGen where
import GHC.Generics
import Data.Proxy
import Prelude hiding (take)
import Data.Void
The Church-encoding of something like Bool
looks
like this:
-- | >>> bool False 1 0
-- 1
False f t = f
bool True f t = t bool
Kind of like a flipped if statement. To replicate it in generics takes some work:
class Summable c where
type Sum c a r :: *
take :: c p -> (a -> r) -> Sum c a r
ignore :: Proxy c -> Proxy a -> r -> Sum c a r
class Prodable c where
type Prod c r :: *
strip :: c p -> Prod c r -> r
class ChurchGen c where
type FoldGen c a :: *
foldGen:: c a -> FoldGen c a
instance Summable c => Summable (M1 i t c) where
type Sum (M1 i t c) a r = Sum c a r
take (M1 x) = take x
_ :: Proxy (M1 i t c)) = ignore (Proxy :: Proxy c)
ignore (
instance Prodable c => Prodable (M1 i t c) where
type Prod (M1 i t c) r = Prod c r
M1 x) = strip x
strip (
instance ChurchGen c => ChurchGen (M1 i t c) where
type FoldGen (M1 i t c) a = FoldGen c a
M1 x) = foldGen x
foldGen (
instance Summable (K1 i c) where
type Sum (K1 i c) a r = (c -> a) -> r
take (K1 x) k f = k (f x)
= r
ignore _ _ r _
instance Summable U1 where
type Sum U1 a r = a -> r
take U1 k f = k f
= r
ignore _ _ r _
instance Prodable U1 where
type Prod U1 r = r
U1 x = x
strip
instance ChurchGen U1 where
type FoldGen U1 a = a -> a
U1 x = x
foldGen
instance Summable V1 where
type Sum V1 a r = r
take x = case x of
= id
ignore _ _
instance Prodable V1 where
type Prod V1 r = Void -> r
= case x of
strip x
instance Prodable (K1 i c) where
type Prod (K1 i c) r = c -> r
K1 x) f = f x
strip (
instance ChurchGen (K1 i c) where
type FoldGen (K1 i c) a = (c -> a) -> a
K1 x) f = f x
foldGen(
instance (Summable li, Summable ri) => Summable (li :+: ri) where
type Sum (li :+: ri) a r = Sum li a (Sum ri a r)
take (L1 x) (k :: a -> r) = take x (ignore (Proxy :: Proxy ri) (Proxy :: Proxy a) . k)
take (R1 x) (k :: a -> r) = ignore (Proxy :: Proxy li) (Proxy :: Proxy a) (take x k)
= ignore (Proxy :: Proxy li) a (ignore (Proxy :: Proxy ri) a x)
ignore p a x
instance (Summable li, Summable ri) => ChurchGen (li :+: ri) where
type FoldGen (li :+: ri) a = Sum li a (Sum ri a a)
x :: (li :+: ri) a) = take x (id :: a -> a)
foldGen(
instance (Prodable li, Prodable ri) => Prodable (li :*: ri) where
type Prod (li :*: ri) a = Prod li (Prod ri a)
:*: ri) f = strip ri (strip li f)
strip (li
instance (Prodable li, Prodable ri) => ChurchGen (li :*: ri) where
type FoldGen (li :*: ri) a = Prod li (Prod ri a) -> a
:*: ri) f = strip ri (strip li f)
foldGen(li
instance (Prodable li, Prodable ri) => Summable (li :*: ri) where
type Sum (li :*: ri) a r = Prod li (Prod ri a) -> r
take x k = k . strip x
= r
ignore _ _ r _
class Church c where
type Fold c a :: *
type Fold c a = FoldGen (Rep c) a
fold :: Proxy a -> c -> Fold c a
fold :: (Generic c, ChurchGen (Rep c), FoldGen (Rep c) a ~ Fold c a) => Proxy a -> c -> Fold c a
default= defaultFold
fold
defaultFold :: (Generic c, ChurchGen (Rep c)) => proxy a -> c -> FoldGen (Rep c) a
p :: proxy a) (x :: c) = foldGen (from x :: Rep c a) defaultFold (
After all of that, we can write the church-encoded bool function like so:
instance Church Bool
-- | >>> fold (Proxy :: Proxy Int) False 0 1
-- 0