Portability | see LANGUAGE pragmas (... GHC) |
---|---|
Stability | experimental |
Maintainer | nicolas.frisby@gmail.com |
Safe Haskell | None |
This is the entire library, excluding the fancy builder of precise cases from Data.Yoko.SmartPreciseCase.
- data Void p1 p0
- data family N dc :: * -> * -> *
- data (a :+: b) p1 p0
- newtype C dc r p1 p0 = C (r p1 p0)
- data U p1 p0 = U
- data (a :*: b) p1 p0 = (a p1 p0) :*: (b p1 p0)
- newtype T0 v t p1 p0 = T0 t
- newtype T1 v t a p1 p0 = T1 (t (a p1 p0))
- newtype T2 v t b a p1 p0 = T2 (t (b p1 p0) (a p1 p0))
- data Variety
- newtype Par1 p1 p0 = Par1 p1
- newtype Par0 p1 p0 = Par0 p0
- type family Rep t :: * -> * -> *
- class Generic dc where
- unC :: C k t t1 t2 t3 -> t1 t2 t3
- foldC :: (t1 t2 t3 -> c) -> C k t t1 t2 t3 -> c
- mapC :: (t1 t2 t3 -> r p1 p0) -> C k t t1 t2 t3 -> C k1 dc r p1 p0
- class ComposeW dc => WN dc where
- unN0 :: N * dc p1 p0 -> dc
- foldN0 :: (b -> c) -> N * b p1 p0 -> c
- mapN0 :: (b1 -> b) -> N * b1 p2 p3 -> N * b p1 p0
- unN1 :: N (* -> *) dc p1 p0 -> dc p0
- foldN1 :: (dc p0 -> c) -> N (* -> *) dc p1 p0 -> c
- mapN1 :: (dc1 p3 -> dc p0) -> N (* -> *) dc1 p2 p3 -> N (* -> *) dc p1 p0
- unN2 :: N (* -> * -> *) dc p1 p0 -> dc p1 p0
- foldN2 :: (dc p1 p0 -> c) -> N (* -> * -> *) dc p1 p0 -> c
- mapN2 :: (dc1 p2 p3 -> dc p1 p0) -> N (* -> * -> *) dc1 p2 p3 -> N (* -> * -> *) dc p1 p0
- foldPlus :: (t1 t3 t4 -> t) -> (t2 t3 t4 -> t) -> :+: t1 t2 t3 t4 -> t
- class FoldPlusW' s where
- foldPlusW' :: W' s l p1 p0 -> W' s r p1 p0 -> W' s (l :+: r) p1 p0
- mapPlus :: (t t2 t3 -> a p1 p0) -> (t1 t2 t3 -> b p1 p0) -> :+: t t1 t2 t3 -> :+: a b p1 p0
- foldTimes :: (t5 -> t6 -> t) -> (t1 t3 t4 -> t5) -> (t2 t3 t4 -> t6) -> :*: t1 t2 t3 t4 -> t
- mapTimes :: (t t2 t3 -> a p1 p0) -> (t1 t2 t3 -> b p1 p0) -> :*: t t1 t2 t3 -> :*: a b p1 p0
- unT0 :: T0 t t1 t2 t3 -> t1
- mapT0 :: (t1 -> t4) -> T0 t t1 t2 t3 -> T0 v t4 p1 p0
- unT1 :: T1 t t1 t2 t3 t4 -> t1 (t2 t3 t4)
- mapT1 :: (t1 (t2 t3 t4) -> t5 (a p1 p0)) -> T1 t t1 t2 t3 t4 -> T1 v t5 a p1 p0
- unT2 :: T2 t t1 t2 t3 t4 t5 -> t1 (t2 t4 t5) (t3 t4 t5)
- mapT2 :: (t1 (t2 t4 t5) (t3 t4 t5) -> t6 (b p1 p0) (a p1 p0)) -> T2 t t1 t2 t3 t4 t5 -> T2 v t6 b a p1 p0
- unPar0 :: Par0 t t1 -> t1
- mapPar0 :: (t1 -> p0) -> Par0 t t1 -> Par0 p1 p0
- unPar1 :: Par1 t t1 -> t
- mapPar1 :: (t -> p1) -> Par1 t t1 -> Par1 p1 p0
- type family DistMaybePlus a b :: Maybe (* -> * -> *)
- type family Tag dc :: Digit
- type family Codomain dc :: k
- type family Codomain0 dcs :: *
- type family Codomain1 dcs :: * -> *
- type family Codomain2 dcs :: * -> * -> *
- data DTPos k
- type family DTs t :: DTPos k
- type NumDTs t = NumDTs' (DTs t)
- type family NumDTs' t :: Nat
- type SiblingDTs t = SiblingDTs' t (DTs t)
- type family SiblingDTs' t dpos :: [k]
- class (Generic dc, DT (Codomain dc)) => DC dc where
- type family DCs t :: * -> * -> *
- class DT t where
- type family Eval r :: *
- data SubstSpec star
- type family Subst spec r :: * -> * -> *
- type Subst0 t p0 = Subst (Sub0 p0) (Rep t)
- type Subst1 t p1 = Subst (Sub1 p1) (Rep t)
- type Subst10 t p1 p0 = Subst (Sub10 p1 p0) (Rep t)
- module Data.Yoko.TypeBasics
- module Data.Yoko.W
- one :: (dc -> a) -> N dc p1 p0 -> a
- (|||) :: Codomain0 sumL ~ Codomain0 sumR => (sumL p1 p0 -> a) -> (sumR p1 p0 -> a) -> (sumL :+: sumR) p1 p0 -> a
- (||.) :: ~ * (Codomain0 sumL) (Codomain * dc) => (sumL p1 p0 -> a) -> (dc -> a) -> :+: sumL (N * dc) p1 p0 -> a
- (.||) :: ~ * (Codomain0 sumR) (Codomain * dc) => (dc -> a) -> (sumR p1 p0 -> a) -> :+: (N * dc) sumR p1 p0 -> a
- (.|.) :: ~ * (Codomain * dc) (Codomain * dc1) => (dc -> a) -> (dc1 -> a) -> :+: (N * dc) (N * dc1) p1 p0 -> a
- disbanded :: Embed (N dc) (DCs (Codomain dc)) => dc -> DCs (Codomain dc) p1 p0
- class AreDCsOf t dcs
- band :: AreDCsOf (t :: k) (DCs t) => W' t (DCs t) p1 p0
- precise_case0 :: (Codomain0 dcs ~ t, Codomain0 (DCs t) ~ t, DT t, Partition (DCs t) dcs (DCs t :-: dcs)) => ((DCs t :-: dcs) p1 p0 -> a) -> t -> (dcs p1 p0 -> a) -> a
- type family sum :-: sum2 :: * -> * -> *
- class Embed sub sup
- class Partition sup subL subR
- embed :: (Codomain0 sub ~ Codomain0 sup, Embed sub sup) => sub p1 p0 -> sup p1 p0
- inject :: Embed (N dc) sum => dc -> sum p1 p0
- partition :: (Codomain0 sum ~ Codomain0 sub, Partition sum sub (sum :-: sub)) => sum p1 p0 -> Either (sub p1 p0) ((sum :-: sub) p1 p0)
- project :: (Codomain0 sum ~ Codomain dc, Partition sum (N dc) (sum :-: N dc)) => sum p1 p0 -> Either dc ((sum :-: N dc) p1 p0)
- reps :: EachGeneric sum => sum p1 p0 -> EachRep sum p1 p0
- class EachGeneric sum
- type family EachRep sum :: * -> * -> *
- ig_from :: (ComposeW t, DT t, EachGeneric (DCs t)) => W t (EachRep (DCs t)) p1 p0
Representation
Sums
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.
Sum union.
(HCompos0 * * cnv a t, HCompos0 * * cnv b t) => HCompos0 * * cnv (:+: a b) t | |
(FoldPlusW' k t, AreDCsOf k t l, AreDCsOf k t r) => AreDCsOf k t (:+: l r) | |
(Invariant2 l, Invariant2 r) => Invariant2 (:+: l r) | |
(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 | |
(Eq (a p1 p0), Eq (b p1 p0)) => Eq (:+: a b p1 p0) | |
(Ord (a p1 p0), Ord (b p1 p0)) => Ord (:+: a b p1 p0) | |
(Read (a p1 p0), Read (b p1 p0)) => Read (:+: a b p1 p0) | |
(Show (a p1 p0), Show (b p1 p0)) => Show (:+: a b p1 p0) |
Wrapper around productus
C (r p1 p0) |
MapRs0 k k1 * * cnv msg dc dc' a a' => MapRs0 k k1 * * cnv msg dc dc' (C k2 dcA a) (C k3 dcB a') | |
Invariant2 r => Invariant2 (C k dc r) |
Products
The empty product.
Invariant2 U | |
Applicative (Idiom cnv) => MapRs0 k k1 * * cnv msg dc dc' U U |
Product union.
(a p1 p0) :*: (b p1 p0) |
(MapRs0 k k1 * * cnv msg dc dc' a a', MapRs0 k k1 * * cnv msg dc dc' b b') => MapRs0 k k1 * * cnv msg dc dc' (:*: a b) (:*: a' b') | |
(Invariant2 l, Invariant2 r) => Invariant2 (:*: l r) |
Fields
T0 t |
T1 (t (a p1 p0)) |
(Traversable f, MapRs0 k k1 * * cnv msg dc dc' a a') => MapRs0 k k1 * * cnv msg dc dc' (T1 Dep f a) (T1 Dep f a') | |
(Invariant t, Invariant2 r) => Invariant2 (T1 v t r) |
newtype T2 v t b a p1 p0 Source
T2 (t (b p1 p0) (a p1 p0)) |
(Bitraversable f, MapRs0 k k1 * * cnv msg dc dc' a a', MapRs0 k k1 * * cnv msg dc dc' b b') => MapRs0 k k1 * * cnv msg dc dc' (T2 Dep f a b) (T2 Dep f a' b') | |
(Invariant2 t, Invariant2 r, Invariant2 s) => Invariant2 (T2 v t r s) |
Conversions to and from fields-of-products structure
type family Rep t :: * -> * -> *Source
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.
Generic * True_ | |
Generic * False_ | |
Generic * ()_ | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => Generic * (:%_ a0) | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => Generic * (Just_ a0) | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => Generic * (Nothing_ a0) | |
Generic * (Cons_ a) | |
Generic * (Nil_ a) | |
(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => Generic * ((,)_ a0 b0) | |
(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => Generic * (Right_ a0 b0) | |
(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => Generic * (Left_ a0 b0) | |
(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0)), ~ Ordering EQ (Compare * (Spine * c0) (Spine * c0))) => Generic * ((,,)_ a0 b0 c0) | |
Generic (* -> * -> *) (,)_ | |
Generic (* -> * -> *) Right_ | |
Generic (* -> * -> *) Left_ | |
Generic (* -> *) :%_ | |
Generic (* -> *) Just_ | |
Generic (* -> *) Nothing_ | |
Generic (* -> *) Cons_ | |
Generic (* -> *) Nil_ | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => Generic (* -> * -> *) ((,,)_ a0) | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => Generic (* -> *) ((,)_ a0) | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => Generic (* -> *) (Right_ a0) | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => Generic (* -> *) (Left_ a0) | |
(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => Generic (* -> *) ((,,)_ a0 b0) |
Auxilliaries
class FoldPlusW' s whereSource
FoldPlusW' * s | |
FoldPlusW' (* -> * -> *) s | |
FoldPlusW' (* -> *) s |
mapT2 :: (t1 (t2 t4 t5) (t3 t4 t5) -> t6 (b p1 p0) (a p1 p0)) -> T2 t t1 t2 t3 t4 t5 -> T2 v t6 b a p1 p0Source
type family DistMaybePlus a b :: Maybe (* -> * -> *)Source
We avoid empty sums with a type-level Maybe
. DistMaybePlus
performs
sum union on lifted sums, only introducing :+:
when both arguments are
Just
s.
type family Tag dc :: DigitSource
Tag
returns a simulated type-level string that is the name of the
constructor that the dc
fields type represents.
type family Codomain dc :: kSource
Codomain
is the data type that contains the constructor that the fields
type dc
represents. It can also be applied to sums of fields types, in
which case it just uses the left-most.
type SiblingDTs t = SiblingDTs' t (DTs t)Source
type family SiblingDTs' t dpos :: [k]Source
class (Generic dc, DT (Codomain dc)) => DC dc whereSource
Any fields type can be further represented as a product-of-fields and can be injected back into the original data type.
DC * True_ | |
DC * False_ | |
DC * ()_ | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DC * (:%_ a0) | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DC * (Just_ a0) | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DC * (Nothing_ a0) | |
(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => DC * ((,)_ a0 b0) | |
(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => DC * (Right_ a0 b0) | |
(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => DC * (Left_ a0 b0) | |
(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0)), ~ Ordering EQ (Compare * (Spine * c0) (Spine * c0))) => DC * ((,,)_ a0 b0 c0) | |
DC (* -> * -> *) (,)_ | |
DC (* -> * -> *) Right_ | |
DC (* -> * -> *) Left_ | |
DC (* -> *) :%_ | |
DC (* -> *) Just_ | |
DC (* -> *) Nothing_ | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DC (* -> * -> *) ((,,)_ a0) | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DC (* -> *) ((,)_ a0) | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DC (* -> *) (Right_ a0) | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DC (* -> *) (Left_ a0) | |
(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => DC (* -> *) ((,,)_ a0 b0) |
DT * Bool | |
DT * () | |
~ Ordering EQ (SpineCompare * * a a) => DT * [a] | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DT * (Ratio a0) | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DT * (Maybe a0) | |
(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => DT * (Either a0 b0) | |
(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => DT * (a0, b0) | |
(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0)), ~ Ordering EQ (Compare * (Spine * c0) (Spine * c0))) => DT * (a0, b0, c0) | |
DT (* -> * -> *) Either | |
DT (* -> * -> *) (,) | |
DT (* -> *) [] | |
DT (* -> *) Ratio | |
DT (* -> *) Maybe | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DT (* -> * -> *) ((,,) a0) | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DT (* -> *) (Either a0) | |
~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DT (* -> *) ((,) a0) | |
(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => DT (* -> *) ((,,) a0 b0) |
module Data.Yoko.TypeBasics
module Data.Yoko.W
Building fields type consumers
one :: (dc -> a) -> N dc p1 p0 -> aSource
one
extends a function that consumes a fields type to a function that
consumes a disbanded data type containing just that fields type.
(|||) :: Codomain0 sumL ~ Codomain0 sumR => (sumL p1 p0 -> a) -> (sumR p1 p0 -> a) -> (sumL :+: sumR) p1 p0 -> aSource
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.
(||.) :: ~ * (Codomain0 sumL) (Codomain * dc) => (sumL p1 p0 -> a) -> (dc -> a) -> :+: sumL (N * dc) p1 p0 -> aSource
f ||. g = f |||
one g
(.||) :: ~ * (Codomain0 sumR) (Codomain * dc) => (dc -> a) -> (sumR p1 p0 -> a) -> :+: (N * dc) sumR p1 p0 -> aSource
f .|| g = one f |||
g
(.|.) :: ~ * (Codomain * dc) (Codomain * dc1) => (dc -> a) -> (dc1 -> a) -> :+: (N * dc) (N * dc1) p1 p0 -> aSource
f .|. g = one f |||
one g
Operations on disbanded data types
disbanded :: Embed (N dc) (DCs (Codomain dc)) => dc -> DCs (Codomain dc) p1 p0Source
disbanded
injects a fields type into its disbanded range
band
s a disbanded data type back into its normal data type.
Since DCs
is a type family, it's the range of band
that determines the
t
type variable.
precise_case0 :: (Codomain0 dcs ~ t, Codomain0 (DCs t) ~ t, DT t, Partition (DCs t) dcs (DCs t :-: dcs)) => ((DCs t :-: dcs) p1 p0 -> a) -> t -> (dcs p1 p0 -> a) -> aSource
precise_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.
precise_case default x $ ((C0_ ...) -> ...).||
((C1_ ...) -> ...).|.
((C2_ ...) -> ...)
In this example, C0_
, C1_
, and C2_
are fields types. The other fields
types for the same data type are handled with the default
function.
Operations on sums of fields types
inject :: Embed (N dc) sum => dc -> sum p1 p0Source
inject
s a fields type into a sum of fields types.
partition :: (Codomain0 sum ~ Codomain0 sub, Partition sum sub (sum :-: sub)) => sum p1 p0 -> Either (sub p1 p0) ((sum :-: sub) p1 p0)Source
partition
s a sum of fields type into a specified sum of fields types and
the remaining sum.
project :: (Codomain0 sum ~ Codomain dc, Partition sum (N dc) (sum :-: N dc)) => sum p1 p0 -> Either dc ((sum :-: N dc) p1 p0)Source
project
s a single fields type out of a disbanded data type.
Forgetting yoko
's extra structure
reps :: EachGeneric sum => sum p1 p0 -> EachRep sum p1 p0Source
reps
maps a disbanded data type to its sum-of-products representation.
class EachGeneric sum Source
(EachGeneric a, EachGeneric b) => EachGeneric (:+: a b) | |
(WN k dc, Generic k dc) => EachGeneric (N k dc) |