{-# LANGUAGE ScopedTypeVariables, FlexibleContexts, DataKinds #-}
{-# LANGUAGE DefaultSignatures, AllowAmbiguousTypes, TypeFamilies #-}
-- | This module provides two functions, @'toChurch'@ and @'fromChurch'@. These form
-- an isomorphism between a type and its church representation of a type
-- To use this, simply define an empty instance of @'ChurchRep'@ for a type with a
-- 'Generic' instance and defaulting magic will take care of the rest. For example
--
-- > {-# LANGUAGE DeriveGeneric #-}
-- > data MyType = Foo Int Bool | Bar | Baz Char
-- > deriving(Generic, Show)
-- >
-- > instance ChurchRep MyType
--
-- Then if we fire up GHCi
--
-- >>> toChurch (Foo 1 True) (\int bool -> int + 1) 0 (const 1)
-- 2
--
-- >>> fromChurch (\foo bar baz -> bar) :: MyType
-- Bar
module Data.Church (Church,
ChurchRep(toChurch, fromChurch),
toChurchP,
fromChurchP,
churchCast,
churchCastP) where
import Data.Church.Internal.ToChurch
import Data.Church.Internal.FromChurch
import Data.Church.Internal.TF
import Data.Proxy
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 'Church' 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 @c@
--
-- 3. Join these type signatures together with arrows @(a -> b -> c) -> c -> ...@
--
-- 4. Append a final @ -> c@ to the end of this
--
-- For example, for 'Maybe'
--
-- 1. @'Nothing' :: Maybe a@ and @'Just' :: a -> Maybe a@.
--
-- 2. We then have @c@ and @a -> c@.
--
-- 3. Joining these gives @c -> (a -> c)@
--
-- 4. @c -> (a -> c) -> c@ is our church representation
type Church t c = ChurchSum (ToList (StripMeta (Rep t ())) (ListTerm ())) c
class ChurchRep a where
-- | Reify a type to its church representation
toChurch :: forall r. ChurchRep a => a -> Church a r
toChurch = toChurchHelper (Proxy :: Proxy r)
-- | Create a value from its church representation.
-- This method may require an explicit signature.
fromChurch :: Church a (Rep a ()) -> a
default
fromChurch :: (Generic a,
(GBuild (MakePaths (Rep a ()) '[] '[])
(Church a (Rep a ()))
(Rep a ()))) =>
Church a (Rep a ()) -> a
fromChurch c = to (build p c :: Rep a ())
where p = Proxy :: Proxy (MakePaths (Rep a ()) '[] '[])
-- | Reify a type to it's church equivalent. This is a hack
-- to avoid a bug in GHC 7.6 where -XDefaultSignatures and
-- -XScopedTypeVariables together will crash. This exists purely
-- so we can give 'toChurch's default signature.
toChurchHelper :: Proxy r -> a -> Church a r
default
toChurchHelper :: (Generic a, GStripMeta (Rep a ()),
GList (StripMeta (Rep a ())) (ListTerm ()),
GChurchSum (ToList (StripMeta (Rep a ())) (ListTerm ())) r) =>
Proxy r -> a -> Church a r
toChurchHelper p = elim p
. flip toList (ListTerm :: ListTerm ())
. Just
. stripMeta
. from'
where from' :: Generic a => a -> Rep a ()
from' = from
toChurchP :: ChurchRep a => Proxy r -> a -> Church a r
toChurchP = toChurchHelper
fromChurchP :: ChurchRep a => Proxy a -> Church a (Rep a ()) -> a
fromChurchP Proxy = fromChurch
-- | Since types with the same church representation are
-- identical, we can cast between them.
churchCast :: forall a b. (ChurchRep a, ChurchRep b,
Church a (Rep b ()) ~ Church b (Rep b ()))
=> a -> b
churchCast = fromChurchP (Proxy :: Proxy b) . toChurchP (Proxy :: Proxy (Rep b ()))
-- | A more explicit version of @churchCast@ that let's you specify
-- the target of the cast with a @Proxy@.
churchCastP :: forall a b. (ChurchRep a, ChurchRep b,
Church a (Rep b ()) ~ Church b (Rep b ()))
=> Proxy b -> a -> b
churchCastP Proxy = churchCast
-- And now a ton of instances
instance ChurchRep Bool
instance ChurchRep Ordering
instance ChurchRep [a]
instance ChurchRep ()
instance ChurchRep ((,) a b)
instance ChurchRep ((,,) a b c)
instance ChurchRep ((,,,) a b c d)
instance ChurchRep ((,,,,) a b c d e)
instance ChurchRep ((,,,,,) a b c d e f)
instance ChurchRep ((,,,,,,) a b c d e f g)
instance ChurchRep (Maybe a)
instance ChurchRep (Either a b)