diff --git a/Church.hs b/Church.hs
new file mode 100644
--- /dev/null
+++ b/Church.hs
@@ -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)
diff --git a/Church/FromChurch.hs b/Church/FromChurch.hs
new file mode 100644
--- /dev/null
+++ b/Church/FromChurch.hs
@@ -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
diff --git a/Church/TF.hs b/Church/TF.hs
new file mode 100644
--- /dev/null
+++ b/Church/TF.hs
@@ -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 ': '[])
diff --git a/Church/ToChurch.hs b/Church/ToChurch.hs
new file mode 100644
--- /dev/null
+++ b/Church/ToChurch.hs
@@ -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"
diff --git a/church.cabal b/church.cabal
new file mode 100644
--- /dev/null
+++ b/church.cabal
@@ -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