{-# 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)