|Portability||see LANGUAGE pragmas (... GHC)|
- Building fields type consumers
- Operations on disbanded data types
- Operations on sums of fields types
yoko's extra structure
- Bundled Template Haskell
This omnibus module is the only necessary import for using the
dc type variables abstract over fields types.
sum type variables abstract over sums of fields types.
A Template Haskell deriver is provided in the Data.Yoko.TH module.
- data Void
- newtype N a = N a
- data a :+: b
- newtype DCsOf t sum = DCsOf sum
- data U = U
- data a :*: b = a :*: b
- newtype Rec a = Rec a
- newtype Dep a = Dep a
- newtype Par1 f a = Par1 (f a)
- newtype Par2 f a b = Par2 (f a b)
- type family Rep a
- class Generic a where
- (|||) :: (DCsOf t sumL -> a) -> (DCsOf t sumR -> a) -> DCsOf t (sumL :+: sumR) -> a
- unDCsOf :: DCsOf t t1 -> t1
- unN :: N t -> t
- foldN :: (b -> c) -> N b -> c
- mapN :: (b1 -> b) -> N b1 -> N b
- foldPlus :: (t1 -> t) -> (t2 -> t) -> :+: t1 t2 -> t
- mapPlus :: (t -> b) -> (t1 -> b1) -> :+: t t1 -> :+: b b1
- foldTimes :: (t3 -> t4 -> t) -> (t1 -> t3) -> (t2 -> t4) -> :*: t1 t2 -> t
- mapTimes :: (t -> a) -> (t1 -> b) -> :*: t t1 -> :*: a b
- unRec :: Rec t -> t
- mapRec :: (t -> a) -> Rec t -> Rec a
- unDep :: Dep t -> t
- unPar1 :: Par1 t t1 -> t t1
- unPar2 :: Par2 t t1 t2 -> t t1 t2
- type family DistMaybePlus a b
- type family Tag dc
- type family Range dc
- class (Generic dc, DT (Range dc)) => DC dc where
- type family DCs t
- type Disbanded t = DCsOf t (DCs t)
- class Each IsDCOf (DCs t) => DT t where
- one :: (dc -> a) -> DCsOf (Range dc) (N dc) -> a
- (||.) :: (DCsOf (Range dc) sumL -> a) -> (dc -> a) -> DCsOf (Range dc) (:+: sumL (N dc)) -> a
- (.||) :: (dc -> a) -> (DCsOf (Range dc) sumR -> a) -> DCsOf (Range dc) (:+: (N dc) sumR) -> a
- (.|.) :: ~ * (Range dc) (Range dc1) => (dc -> a) -> (dc1 -> a) -> DCsOf (Range dc1) (:+: (N dc) (N dc1)) -> a
- disbanded :: Embed (N dc) (DCs (Range dc)) => dc -> Disbanded (Range dc)
- band :: forall t. Each (ConDCOf t) (DCs t) => Disbanded t -> t
- class (Range dc ~ t, DC dc) => ConDCOf t dc
- exact_case :: (DT t, Partition (DCs t) dcs (DCs t :-: dcs)) => (DCsOf t (DCs t :-: dcs) -> a) -> t -> (DCsOf t dcs -> a) -> a
- type family sum :-: sum2
- class Embed sub sup
- class Partition sup subL subR
- inject :: Embed (N dc) sum => dc -> sum
- partition :: Partition sum sub (sum :-: sub) => DCsOf t sum -> Either (DCsOf t sub) (DCsOf t (sum :-: sub))
- project :: Partition sum (N dc) (sum :-: N dc) => DCsOf (Range dc) sum -> Either dc (DCsOf (Range dc) (sum :-: N dc))
- reps :: EachGeneric sum => DCsOf t sum -> EachRep sum
- class EachGeneric sum
- type family EachRep sum
- ig_from :: (DT t, EachGeneric (DCs t)) => t -> EachRep (DCs t)
- type Equal a b = IsEQ (Compare a b)
- module Data.Yoko.TH
The empty sum. Used as an error type instead of a represention type, since data types with no constructors are uninteresting from a generic programming perspective -- there's just not much to be done generically.
The singleton sum.
|cxt a => Each_ cxt (N a)|
|(Generic dc, ~ * (Just (N dc')) (FindDCs (Tag dc) (DCs t)), HComposRs cnv (Rep dc) (Rep dc'), DC dc', ~ * (Range dc') t, DT t) => HCompos cnv (N dc) t|
|Generic a => EachGeneric (N a)|
|(~ * (Locate x sup) (Just path), InjectAt path x sup) => Embed (N x) sup|
|Partition_N (Elem x subL) x subL subR => Partition (N x) subL subR|
|InjectAt (Here a) a (N a)|
|(Each_ cxt a, Each_ cxt b) => Each_ cxt (:+: a b)|
|(HCompos cnv a t, HCompos cnv b t) => HCompos cnv (:+: a b) t|
|InjectAt path a r => InjectAt (TurnRight path) a (:+: l r)|
|InjectAt path a l => InjectAt (TurnLeft path) a (:+: l r)|
|(Eq a, Eq b) => Eq (:+: a b)|
|(Ord a, Ord b) => Ord (:+: a b)|
|(Read a, Read b) => Read (:+: a b)|
|(Show a, Show b) => Show (:+: a b)|
|(EachGeneric a, EachGeneric b) => EachGeneric (:+: a b)|
|(Embed l sup, Embed r sup) => Embed (:+: l r) sup|
|(Partition a subL subR, Partition b subL subR) => Partition (:+: a b) subL subR|
A disbanded data type is an application of
DCsOf t to a sum of fields
types all of which have
t as their range. The use of
parameter throughout the API (e.g. in
|||) supplants many ascriptions.
|a :*: b|
A non-recursive occurrence.
Representation of unary type application.
f is a genuine
not a representation.
a is a representation.
|Par1 (f a)|
Representation of binary type application.
f is a genuine
type, not a representation.
b are representations.
|Par2 (f a b)|
Conversions to and from fields-of-products structure
A mapping to the structural representation of a fields type: just products of fields, no sums -- fields types have just one constructor.
Converts between a fields type and its product-of-fields structure.
Building disbanded data type consumers
Combines two functions that consume disbanded data types into a function that consumes their union. All fields types must be from the same data type.
We avoid empty sums with a type-level
sum union on lifted sums, only introducing
:+: when both arguments are
Tag returns a simulated type-level string that is the name of the
constructor that the
dc fields type represents.
Range is the data type that contains the constructor that the fields
Any fields type can be further represented as a product-of-fields and can be injected back into the original data type.
Disbanded data types
A disbanded data type is the data type's
DCs annotated with it.
DT disbands a data type if all of its fields types have
Building fields type consumers
one extends a function that consumes a fields type to a function that
consumes a disbanded data type containing just that fields type.
f ||. g = f
f .|| g = one f
f .|. g = one f
Operations on disbanded data types
disbanded injects a fields type into its disbanded range
bands a disbanded data type back into its normal data type.
Disbanded is a type family, the range of
band determines the
exact_case is an exactly-typed case: the second argument is the
discriminant, the first argument is the default case, and the third argument
approximates a list of alternatives.
In this example,
C2_ are fields types. The other fields
types for the same data type are handled with the
Operations on sums of fields types
partitions a sum of fields type into a specified sum of fields types and
the remaining sum.
projects a single fields type out of a disbanded data type.
yoko's extra structure
reps maps a disbanded data type to its sum-of-products representation.
ig_from x = 'reps $ disband'
x is a convenience. It approximates the
instant-generics view, less the
Bundled Template Haskell