-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | An implementation of extensible products and sums
--   
--   An implementation of extensible products and sums.
@package summer
@version 0.3.2.0


module Data.Prodder

-- | An extensible product type
data Prod (xs :: [*])

-- | Extract a value at a particular index
extract :: forall x xs. x `HasIndexIn` xs => Prod xs -> x

-- | Computes the index of the given type in the given type level list.
index :: forall x xs. x `HasIndexIn` xs => Word

-- | Takes the tail of a product after the nth element.
tailN :: forall n xs. (KnownNat n, n <= Length xs) => Prod xs -> Prod (Tail n xs)

-- | Takes the initial length n segment of a product.
initN :: forall n xs. (KnownNat n, n <= Length xs) => Prod xs -> Prod (Init n xs)

-- | Drop the first element of a product. Sometimes needed for better type
--   inference and less piping around of constraints.
dropFirst :: forall x xs. Prod (x : xs) -> Prod xs

-- | A typeclass that is useful to define the scott encoding/decoding for
--   extensible products.
class Consume xs
consume :: forall r. Consume xs => Prod xs -> Consumer xs r -> r
produceB :: Consume xs => (forall r. Consumer xs r -> r) -> ProdBuilder xs
extend1 :: Consume xs => x -> Consumer xs (ProdBuilder (x : xs))
cmap :: Consume xs => (r -> r') -> Consumer xs r -> Consumer xs r'
produce :: (KnownNat (Length xs), Consume xs) => (forall r. Consumer xs r -> r) -> Prod xs
empty :: Prod '[]

-- | A class for folding over a <a>Prod</a> using a function which only
--   requires that every element of the product satisfy a certain
--   constraint.
class ForAll c xs => FoldProd c xs
foldProd :: (FoldProd c xs, Monoid m) => (forall a. c a => a -> m) -> Prod xs -> m
toList :: forall c xs a. FoldProd c xs => (forall x. c x => x -> a) -> Prod xs -> [a]
type family ForAll c xs :: Constraint

-- | Lens to modify one element of a product.
atType :: forall a b xs f. (a `HasIndexIn` xs, Functor f) => (a -> f b) -> Prod xs -> f (Prod (Replace a b xs))

-- | Execute a <a>ProdBuilder</a>, pulling out a <a>Prod</a>.
buildProd :: forall xs. KnownNat (Length xs) => ProdBuilder xs -> Prod xs

-- | A type for constructing products with linear memory use.
data ProdBuilder (xs :: [*])

-- | Cons an element onto the head of a <a>ProdBuilder</a>.
consB :: x -> ProdBuilder xs -> ProdBuilder (x : xs)

-- | Empty <a>ProdBuilder</a>.
emptyB :: ProdBuilder '[]

-- | Appends two <a>ProdBuilder</a>s.
appendB :: ProdBuilder xs -> ProdBuilder ys -> ProdBuilder (xs <> ys)

-- | A type family for indexing into lists of types.
type family Index (n :: Nat) (xs :: [k])

-- | A type family for computing the index of a type in a list of types.
type family IndexIn (x :: k) (xs :: [k])

-- | A class that is used for convenience in order to make certain type
--   signatures read more clearly.
class KnownNat (x `IndexIn` xs) => x `HasIndexIn` xs

-- | This is a reified pattern match on an extensible product
type family Consumer xs r
type family (<>) (xs :: [k]) (ys :: [k]) :: [k]

-- | A type family for computing the length of a type level list
type family Length (xs :: [k])

-- | A type family for computing the tail of a type level list
type family Tail n xs

-- | A type family for computing the initial segment of a type level list
type family Init n xs

-- | Type family for replacing one type in a type level list with another
type family Replace x y xs

-- | A typeclass to rearrange and possibly remove things from a product.
class Strengthen xs ys
strengthenP :: Strengthen xs ys => Prod xs -> ProdBuilder ys
strengthen :: (KnownNat (Length ys), Strengthen xs ys) => Prod xs -> Prod ys

-- | Replaces one type with another via a function
remap :: forall x y xs. x `HasIndexIn` xs => (x -> y) -> Prod xs -> Prod (Replace x y xs)

-- | A class for constructing the select function inductively.
class Selection def selector a
select :: Selection def selector a => Prod def -> selector -> a

-- | Extracts the fields intended from the given selector type.
type family FieldsFromSelector def selector

-- | A typeclass for creating a selection function which is valid on the
--   given definition.
type family Selector def fields a
instance Data.Prodder.FoldProd c '[]
instance (c x, Data.Prodder.FoldProd c xs) => Data.Prodder.FoldProd c (x : xs)
instance Data.Prodder.Selection def a a
instance (Data.Prodder.HasIndexIn x def, Data.Prodder.Selection def xs a) => Data.Prodder.Selection def (x -> xs) a
instance (Data.Prodder.Strengthen xs ys, Data.Prodder.HasIndexIn y xs) => Data.Prodder.Strengthen xs (y : ys)
instance Data.Prodder.Strengthen xs '[]
instance Data.Prodder.Consume '[]
instance Data.Prodder.Consume xs => Data.Prodder.Consume (x : xs)
instance forall k (x :: k) (xs :: [k]). GHC.TypeNats.KnownNat (Data.Prodder.IndexIn x xs) => Data.Prodder.HasIndexIn x xs
instance GHC.Classes.Eq (Data.Prodder.Prod '[])
instance (GHC.Classes.Eq x, GHC.Classes.Eq (Data.Prodder.Prod xs)) => GHC.Classes.Eq (Data.Prodder.Prod (x : xs))


module Data.Summer

-- | The extensible sum type, allowing inhabitants to be of any of the
--   types in the given type list.
data Sum (xs :: [*])

-- | A pattern to match on for convenience. Without this, the user facing
--   interface is rather baroque.
pattern Inj :: forall x xs. x `HasTagIn` xs => x -> Sum xs

-- | Computes the tag of the given type in the given type level list.
tag :: forall x xs. x `HasTagIn` xs => Word

-- | Injects a type into the extensible sum.
inject :: forall x xs. x `HasTagIn` xs => x -> Sum xs

-- | Inspects an extensible sum for a particular type.
inspect :: forall x xs. x `HasTagIn` xs => Sum xs -> Maybe x

-- | Consider a certain type, discarding it as an option if it is not the
--   correct one.
consider :: forall x xs. x `HasTagIn` xs => Sum xs -> Either (Sum (Delete x xs)) x

-- | Consider the first type in the list of possibilities, a useful
--   specialization for type inference.
considerFirst :: forall x xs. Sum (x : xs) -> Either (Sum xs) x

-- | A typeclass for scott encoding extensible sums
class Match xs
match :: forall r. Match xs => Sum xs -> Matcher xs r
unmatch :: Match xs => (forall r. Matcher xs r) -> Sum xs
override :: forall r. Match xs => r -> Matcher xs r -> Matcher xs r

-- | A utility typeclass which makes the implementation of <a>Match</a>
--   cleaner.
class Unmatch xs ys

-- | A type family for computing the tag of a given type in an extensible
--   sum. In practice, this means computing the first index of the given
--   type in the list.
type family TagIn (x :: k) (xs :: [k])

-- | A class that is used for convenience in order to make certain type
--   signatures read more clearly.
class KnownNat (x `TagIn` xs) => x `HasTagIn` xs

-- | A type family for deleting the given type from a list
type family Delete (x :: k) (xs :: [k]) :: [k]

-- | A class which checks that every type has the same tag in the first
--   list as the second. In other words, checks if the first list is a
--   prefix of the other.
class HaveSameTagsIn xs ys

-- | The scott encoding of an extensible sum
type family Matcher xs r :: Type

-- | Transforming one sum into a sum which contains all of the same types
class Weaken xs ys
weaken :: Weaken xs ys => Sum xs -> Sum ys

-- | A free version of weakening, where all you're doing is adding more
--   possibilities at exclusively higher tags.
noOpWeaken :: forall xs ys. xs `HaveSameTagsIn` ys => Sum xs -> Sum ys

-- | Transforms one type in the sum into another.
inmap :: forall x y xs. (x `HasTagIn` xs, y `HasTagIn` xs) => (x -> y) -> Sum xs -> Sum xs

-- | Transform one type in one sum into another type in another sum.
smap :: forall x y xs ys. (Weaken (Delete x xs) ys, x `HasTagIn` xs, y `HasTagIn` ys) => (x -> y) -> Sum xs -> Sum ys

-- | Using functions which only require constraints which are satisfied by
--   all members of the sum.
class ForAll c xs => ApplyFunction c xs
apply :: ApplyFunction c xs => (forall a. c a => a -> y) -> Sum xs -> y
type family ForAll c xs :: Constraint
instance Data.Summer.ApplyFunction c '[]
instance (c x, Data.Summer.ApplyFunction c xs) => Data.Summer.ApplyFunction c (x : xs)
instance (Data.Summer.Unmatch xs (x : xs), Data.Summer.Match xs) => Data.Summer.Match (x : xs)
instance Data.Summer.Unmatch '[] ys
instance (Data.Summer.Unmatch xs ys, Data.Summer.HasTagIn x ys) => Data.Summer.Unmatch (x : xs) ys
instance Data.Summer.Match '[]
instance (Data.Summer.Weaken xs ys, Data.Summer.HasTagIn x ys) => Data.Summer.Weaken (x : xs) ys
instance Data.Summer.Weaken '[] ys
instance forall k1 k2 (ys :: k1). Data.Summer.HaveSameTagsIn '[] ys
instance forall a (xs :: [a]) (ys :: [a]) (x :: a). Data.Summer.HaveSameTagsIn xs ys => Data.Summer.HaveSameTagsIn (x : xs) (x : ys)
instance forall k (x :: k) (xs :: [k]). GHC.TypeNats.KnownNat (Data.Summer.TagIn x xs) => Data.Summer.HasTagIn x xs
instance Generics.SOP.Universe.Generic (Data.Summer.Sum '[])
instance Generics.SOP.Universe.Generic (Data.Summer.Sum xs) => Generics.SOP.Universe.Generic (Data.Summer.Sum (x : xs))
instance (GHC.Classes.Eq (Data.Summer.Sum xs), GHC.Classes.Eq x) => GHC.Classes.Eq (Data.Summer.Sum (x : xs))
instance GHC.Classes.Eq (Data.Summer.Sum '[])