{-# OPTIONS_HADDOCK show-extensions #-} -- | @'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))) module Church (ChurchRep, Church(churchEncode, churchDecode), churchCast) where import Church.ToChurch import Church.FromChurch import Church.TF import GHC.Generics -- | 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 type ChurchRep t r = ChurchSum (ToList (StripMeta (Rep t ())) (ListTerm ())) r class Church a where -- | Reify a type to its church representation churchEncode :: forall r. a -> ChurchRep a r default churchEncode :: forall r. (Generic a, GStripMeta (Rep a ()), GList (StripMeta (Rep a ())) (ListTerm ()), GChurchSum (ToList (StripMeta (Rep a ())) (ListTerm ())) r) => a -> ChurchRep a r churchEncode = elim @_ @r . (`toList` (ListTerm @())) . Just . stripMeta . from @_ @() -- | Create a value from its church representation. -- This method may require an explicit signature. churchDecode :: ChurchRep a (Rep a ()) -> a default churchDecode :: (Generic a, (GBuild (MakePaths (Rep a ()) '[] '[]) (ChurchRep a (Rep a ())) (Rep a ()))) => ChurchRep a (Rep a ()) -> a churchDecode c = to (build @(MakePaths (Rep a ()) '[] '[]) c :: Rep a ()) -- | Since types with the same church representation are -- identical, we can cast between them. churchCast :: forall a b. (Church a, Church b, ChurchRep a (Rep b ()) ~ ChurchRep b (Rep b ())) => a -> b churchCast = churchDecode @b . churchEncode @a @(Rep b ()) instance Church Bool instance Church Ordering instance Church [a] instance Church () instance Church ((,) a b) instance Church ((,,) a b c) instance Church ((,,,) a b c d) instance Church ((,,,,) a b c d e) instance Church ((,,,,,) a b c d e f) instance Church ((,,,,,,) a b c d e f g) instance Church (Maybe a) instance Church (Either a b)