church (empty) → 0.1.0.0
raw patch · 5 files changed
+396/−0 lines, 5 filesdep +base
Dependencies added: base
Files
- Church.hs +115/−0
- Church/FromChurch.hs +85/−0
- Church/TF.hs +63/−0
- Church/ToChurch.hs +99/−0
- church.cabal +34/−0
+ Church.hs view
@@ -0,0 +1,115 @@+{-# 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)
+ Church/FromChurch.hs view
@@ -0,0 +1,85 @@+{-# language UndecidableInstances #-}+module Church.FromChurch where+import GHC.Generics+import Church.TF+import Prelude++data Traverse a c = Meta a c a | InL a a | InR a a | Term a++type family PathArg (t :: [Traverse * Meta]) where+ PathArg (Term a ': '[] ) = a+ PathArg ('Meta a b p ': rest) = PathArg rest+ PathArg (InR l p ': rest) = PathArg rest+ PathArg (InL r p ': rest) = PathArg rest++-- | Construct a product type where all the fields are+-- _|_+class GEmpty a where empty :: a+instance GEmpty (U1 p) where empty = U1+instance GEmpty (K1 a t p) where empty = K1 (error "Error! The impossible has happened.")+instance GEmpty (f p) => GEmpty (M1 a b f p) where empty = M1 empty+instance (GEmpty (l p), GEmpty (r p)) => GEmpty ((:*:) l r p) where empty = empty :*: empty++type family MakeProdPaths v (m :: [Traverse * Meta]) (r :: [ [Traverse * Meta] ]) :: [[Traverse * Meta]] where+ MakeProdPaths (K1 a t p) s all = Reverse (Term (K1 a t p) ': s) ': all+ MakeProdPaths (M1 a b f p) s all = MakeProdPaths (f p) ('Meta a b p ': s) all+ MakeProdPaths ((:*:) l r p) s all =+ Append (MakeProdPaths (l p) (InL (r p) p ': s) '[])+ (Append (MakeProdPaths (r p) (InR (l p) p ': s) '[]) all)++class GUpdate (path :: [Traverse * Meta]) a where update :: a -> PathArg path -> a+instance GUpdate (Term (K1 a t p) ': '[]) (K1 a t p) where update _ a = a+instance GUpdate rest (l p) => GUpdate (InL (r p) p ': rest) ((:*:) l r p) where+ update (l :*: r) a = update @rest l a :*: r+instance GUpdate rest (r p) => GUpdate (InR (l p) p ': rest) ((:*:) l r p) where+ update (l :*: r) a = l :*: update @rest r a +instance GUpdate rest (f p) => GUpdate ('Meta a b p ': rest) (M1 a b f p) where+ update (M1 f) a = M1 (update @rest f a)++type family Fill (paths :: [[Traverse * Meta]]) r where+ Fill (x ': xs) r = StripK (PathArg x) -> Fill xs r+ Fill '[] r = r++class GFill (paths :: [[Traverse * Meta]]) a where+ fill :: (a -> r) -> a -> Fill paths r+instance GFill '[] a where+ fill f a = f a+instance (PathArg x ~ K1 m t p, StripK (PathArg x) ~ t, GUpdate x a, GFill xs a) =>+ GFill (x ': xs) a where+ fill f a = \x -> fill @xs f $ update @x a (K1 x)++type family MakePaths v (m :: [Traverse * Meta]) (r :: [ [Traverse * Meta] ]) :: [[Traverse * Meta]] where+ MakePaths ((:+:) l r p) s all =+ Append (MakePaths (l p) (InL (r p) p ': s) '[])+ (Append (MakePaths (r p) (InR (l p) p ': s) '[]) all)+ MakePaths (M1 a b f p) s all = MakePaths (f p) ('Meta a b p ': s) all+ MakePaths (K1 a t p) s all = Reverse (Term (K1 a t p) ': s) ': all+ MakePaths (U1 p) s all = Reverse (Term (U1 p) ': s) ': all+ MakePaths ((:*:) l r p) s all = Reverse (Term ((:*:) l r p) ': s) ': all++type family ReconstructPath (t :: [Traverse * Meta]) where+ ReconstructPath (InL r p ': rest) = (WithoutParam (ReconstructPath rest) :+: WithoutParam r) p+ ReconstructPath (InR l p ': rest) = (WithoutParam l :+: WithoutParam (ReconstructPath rest)) p+ ReconstructPath ('Meta a b p ': rest) = M1 a b (WithoutParam (ReconstructPath rest)) p+ ReconstructPath (Term a ': '[]) = a++class GPath' (p :: [Traverse * Meta]) where path' :: PathArg p -> ReconstructPath p+instance GPath' (Term a ': '[]) where path' = id+instance ((WithoutParam (ReconstructPath rest)) p ~ ReconstructPath rest, GPath' rest)+ => GPath' (InR r p ': rest) where path' a = R1 $ path' @rest a+instance ((WithoutParam (ReconstructPath rest)) p ~ ReconstructPath rest, GPath' rest)+ => GPath' (InL l p ': rest) where path' a = L1 $ path' @rest a+instance ((WithoutParam (ReconstructPath rest)) p ~ ReconstructPath rest, GPath' rest)+ => GPath' ('Meta a b p ': rest) where path' a = M1 $ path' @rest a++class GBuild (paths :: [[Traverse * Meta]]) f r where build :: f -> r+-- | Unit case. This represents constructors with no arguments+instance (ReconstructPath x ~ r, GPath' x, GBuild xs f' r, PathArg x ~ U1 p)+ => GBuild (x ': xs) (r -> f') r where build f = build @xs $ f (path' @x U1)+instance ((f -> g) ~ Fill (MakeProdPaths (PathArg x) '[] '[]) r,+ ReconstructPath x ~ r, GEmpty (PathArg x), GBuild xs f' r,+ (GFill (MakeProdPaths (PathArg x) '[] '[]) (PathArg x)),+ GPath' x)+ => GBuild (x ': xs) ((f -> g) -> f') r where+ build f = build @xs $ f (fill @(MakeProdPaths (PathArg x) '[] '[]) (path' @x) empty)+instance GBuild '[] r r where build = id
+ Church/TF.hs view
@@ -0,0 +1,63 @@+{-# language UndecidableInstances #-}+module Church.TF where+import GHC.Generics++-- | This is isomorphic to @()@ with a more interesting+-- kind. It's used to annotate the end of pseudolists formed+-- by combining @:*:@ and @:+:@'s.+data ListTerm p = ListTerm++-- | 'GHC.Generic' annotates types with an extra type parameter+-- this type family removes that extra parameter and returns+-- the constructor of kind @* -> *@+type family WithoutParam v :: * -> * where+ WithoutParam ((:+:) l r p) = l :+: r+ WithoutParam ((:*:) l r p) = l :*: r+ WithoutParam (U1 p) = U1+ WithoutParam (M1 a b f p) = M1 a b f+ WithoutParam (K1 a t p) = K1 a t+ WithoutParam (ListTerm p) = ListTerm+++-- | Remove the meta information (@M1@ constructors) from a type.+type family StripMeta v where+ StripMeta (M1 a b f p) = StripMeta (f p)+ StripMeta (K1 a t p) = K1 a t p+ StripMeta ((:+:) l r p) =+ (:+:) (WithoutParam (StripMeta (l p))) (WithoutParam (StripMeta (r p))) p+ StripMeta ((:*:) l r p) =+ (:*:) (WithoutParam (StripMeta (l p))) (WithoutParam (StripMeta (r p))) p+ StripMeta (U1 p) = U1 p++class GStripMeta a where+ stripMeta :: a -> StripMeta a+instance GStripMeta (f p) => GStripMeta (M1 a b f p) where+ stripMeta (M1 f) = stripMeta f+instance GStripMeta (K1 a t p) where+ stripMeta = id+instance GStripMeta (U1 p) where+ stripMeta = id+instance (GStripMeta (l p), GStripMeta (r p),+ (WithoutParam (StripMeta (l p))) p ~ StripMeta (l p),+ (WithoutParam (StripMeta (r p))) p ~ StripMeta (r p)) =>+ GStripMeta ((:*:) l r p) where+ stripMeta (l :*: r) = stripMeta l :*: stripMeta r+instance (GStripMeta (l p), GStripMeta (r p),+ (WithoutParam (StripMeta (l p))) p ~ StripMeta (l p),+ (WithoutParam (StripMeta (r p))) p ~ StripMeta (r p)) =>+ GStripMeta ((:+:) l r p) where+ stripMeta (L1 l) = L1 $ stripMeta l+ stripMeta (R1 r) = R1 $ stripMeta r++-- | Strip away the extra information that annotates leaves in GHC.Generics+type family StripK v where StripK (K1 a t p) = t++-- | Append for type level lists+type family Append (xs :: [k]) (ys :: [k]) :: [k] where+ Append '[] ys = ys+ Append (x ': xs) ys = x ': Append xs ys++-- | Reverse for type level lists+type family Reverse (xs :: [k]) :: [k] where+ Reverse '[] = '[]+ Reverse (x ': xs) = Append (Reverse xs) (x ': '[])
+ Church/ToChurch.hs view
@@ -0,0 +1,99 @@+{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Church.ToChurch where+import GHC.Generics+import Church.TF+import Prelude+++-- | Eliminate a product type+type family ChurchProd v c where+ ChurchProd (K1 a t p) c = t -> c+ ChurchProd (U1 p) c = c+ ChurchProd ((:*:) l r p) c = ChurchProd (l p) (ChurchProd (r p) c)+ ChurchProd (ListTerm p) c = c++-- | Reorder a product type into a list rather than+-- a balanced tree+type family ToListProd v rest where+ ToListProd ((:*:) l r' p) r = ToListProd (l p) (ToListProd (r' p) r)+ ToListProd (K1 a t p) r = (K1 a t :*: WithoutParam r) p+ ToListProd (U1 p) r = U1 p++-- | Given a product type and a tail, reorder the product type+-- into a list according to 'ToListProd'.+class GListProd a r where+ toListProd :: a -> r -> ToListProd a r+instance (WithoutParam r) p ~ r => GListProd (U1 p) r where+ toListProd = const+instance (WithoutParam r) p ~ r => GListProd (K1 a t p) r where+ toListProd = (:*:)+instance (GListProd (l p) (ToListProd (r' p) r), GListProd (r' p) r) => GListProd ((:*:) l r' p) r where+ toListProd (l :*: r) rest = toListProd l (toListProd r rest)++-- | Eliminate a product type+class GChurchProd a where prod :: a -> ChurchProd a r -> r+instance GChurchProd (U1 p) where prod _ f = f+instance GChurchProd (K1 a t p) where prod (K1 r) f = f r+instance GChurchProd (r p) => GChurchProd ((K1 a t :*: r) p) where+ prod (K1 l :*: r) f = prod r (f l)+instance GChurchProd (ListTerm p) where prod _ f = f++-- | Reorder a sum type into a list rather than a balanced+-- tree of '(:+:)'s.+type family ToList v rest where+ ToList ((:+:) l r' p) r = ToList (l p) (ToList (r' p) r)+ ToList (K1 a t p) r = (K1 a t :+: WithoutParam r) p+ ToList ((:*:) l r' p) r = ((l :*: r') :+: WithoutParam r) p+ ToList (U1 p) r = (U1 :+: WithoutParam r) p++-- | Given an optional sum type and a tail, reorder the+-- sum type into a list like structure.+class GList a r where+ toList :: Maybe a -> r -> ToList a r+instance (WithoutParam r) p ~ r => GList (U1 p) r where+ toList Nothing r = R1 r+ toList (Just a) _ = L1 a+instance (WithoutParam r) p ~ r => GList (K1 a t p) r where+ toList Nothing r = R1 r+ toList (Just a) _ = L1 a+instance (WithoutParam r) p ~ r => GList ((l :*: r') p) r where+ toList Nothing r = R1 r+ toList (Just a) _ = L1 a+instance (GList (l p) (ToList (r' p) r),+ GList (r' p) r) => GList ((l :+: r') p) r where+ toList (Just sum@(L1 l)) r = toList (Just l) (toList (rNot sum) r)+ where rNot :: forall l r p. (l :+: r) p -> Maybe (r p)+ rNot _ = Nothing+ toList (Just sum@(R1 r')) r = toList (lNot sum) (toList (Just r') r)+ where lNot :: forall l r p. (l :+: r) p -> Maybe (l p)+ lNot _ = Nothing+ toList m r = toList (lNot m) (toList (rNot m) r)+ where lNot :: forall l r p. Maybe ((:+:) l r p) -> Maybe (l p)+ lNot _ = Nothing+ rNot :: forall l r p. Maybe ((:+:) l r p) -> Maybe (r p)+ rNot _ = Nothing++-- | The actual church representation of a type+-- once it's been properly reordered.+type family ChurchSum v c where+ ChurchSum ((:+:) l r p) c = ChurchProd (ToListProd (l p) (ListTerm ())) c -> ChurchSum (r p) c+ ChurchSum (ListTerm p) c = c++-- | An odd version of `const` which will swallow+-- all arguments to a church representation and return+-- a value previously given to it.+class Swallow a where swallow :: c -> ChurchSum a c+instance Swallow (ListTerm p) where swallow c = c+instance Swallow (r p) => Swallow ((:+:) l r p) where swallow c = \_ -> swallow @(r p) c++-- | Transform a reordered sum value into a church representation.++class GChurchSum a r where elim :: a -> ChurchSum a r+instance (GListProd (l p) (ListTerm ()), GChurchProd (ToListProd (l p) (ListTerm ())),+ GChurchSum (r' p) r, Swallow (r' p)) =>+ GChurchSum ((l :+: r') p) r where+ elim sum@(L1 l) = \f -> swallow @(r' p) (prod @_ @r (toListProd l (ListTerm :: ListTerm ())) f)+ elim (R1 r) = \_ -> elim @_ @r r+instance GChurchSum (ListTerm p) r where elim _ = error "Malformed generic instance"
+ church.cabal view
@@ -0,0 +1,34 @@+cabal-version: 2.2+name: church+homepage: https://github.com/exordium/church#readme+version: 0.1.0.0+category: Generics+synopsis: Automatically convert Generic instances to and from church representations+description: This package provides a type 'ChurchRep' to generically construct + the type of the church representation.++ Additionally, it provides a type class 'Church' which contains+ a pair of functions for mapping back and forth between the two+ representations.+ Both the @ChurchRep@ and the @Church@ instance are be automatically constructed+ for all types with a @Generic@ instance.++ Based on code by Danny Gratzer.++stability: cursed+bug-reports: https://github.com/exordium/church/issues+author: Dai+maintainer: daig@sodality.cc+copyright: 2018 Sodality+license: MIT++source-repository head+ type: git+ location: https://github.com/exordium/church++library+ exposed-modules: Church+ other-modules: Church.TF, Church.ToChurch, Church.FromChurch+ build-depends: base ^>= 4.12.0.0+ default-language: Haskell2010+ default-extensions: AllowAmbiguousTypes, TypeApplications, TypeFamilies, ScopedTypeVariables, DataKinds, FlexibleContexts, DefaultSignatures, TypeOperators, MultiParamTypeClasses, PolyKinds, FlexibleInstances