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
- newtype N a = N a
- data a :+: b
- 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
- 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 :: Maybe *
- type family Tag dc :: Digit
- type family Codomain dc
- class (Generic dc, DT (Codomain dc)) => DC dc where
- type family DCs t
- class Each IsDCOf (DCs t) => DT t where
- one :: (dc -> a) -> N dc -> a
- (|||) :: Codomain sumL ~ Codomain sumR => (sumL -> a) -> (sumR -> a) -> (sumL :+: sumR) -> a
- (||.) :: ~ * (Codomain sumL) (Codomain dc) => (sumL -> a) -> (dc -> a) -> :+: sumL (N dc) -> a
- (.||) :: ~ * (Codomain sumR) (Codomain dc) => (dc -> a) -> (sumR -> a) -> :+: (N dc) sumR -> a
- (.|.) :: ~ * (Codomain dc) (Codomain dc1) => (dc -> a) -> (dc1 -> a) -> :+: (N dc) (N dc1) -> a
- disbanded :: Embed (N dc) (DCs (Codomain dc)) => dc -> DCs (Codomain dc)
- band :: forall t. Each (ConDCOf t) (DCs t) => DCs t -> t
- class (Codomain dc ~ t, DC dc) => ConDCOf t dc
- precise_case :: (Codomain dcs ~ t, Codomain (DCs t) ~ t, DT t, Partition (DCs t) dcs (DCs t :-: dcs)) => ((DCs t :-: dcs) -> a) -> t -> (dcs -> a) -> a
- type family sum :-: sum2
- class Embed sub sup
- class Partition sup subL subR
- embed :: (Codomain sub ~ Codomain sup, Embed sub sup) => sub -> sup
- inject :: Embed (N dc) sum => dc -> sum
- partition :: (Codomain sum ~ Codomain sub, Partition sum sub (sum :-: sub)) => sum -> Either sub (sum :-: sub)
- project :: (Codomain sum ~ Codomain dc, Partition sum (N dc) (sum :-: N dc)) => sum -> Either dc (sum :-: N dc)
- reps :: EachGeneric sum => 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 (SpineCompare a b)
- module Data.Yoko.TH

# 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.

The singleton sum.

N a |

cxt a => Each_ cxt (N a) | |

(Applicative (Idiom cnv), Generic dcA, ~ (FoundDC *) (Match * dcB) (WithMessage dcA b (FindDCs (Tag dcA) (DCs b))), MapRs cnv (ResultsInIncompatibleFields dcA dcB) dcA dcB (Rep dcA) (Rep dcB), DC dcB, ~ * (Codomain dcB) b, DT b) => HCompos cnv (N dcA) b | |

Generic a => EachGeneric (N a) | |

(~ (Maybe *) (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) |

Sum union.

(Each_ cxt a, Each_ cxt b) => Each_ cxt (:+: a b) | |

(Applicative (Idiom cnv), 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) | |

(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 |

## Products

Product union.

a :*: b |

## Fields

A recursive occurrence.

Rec a |

Representation of unary type application. `f`

is a genuine `*->*`

type,
not a representation. `a`

is a representation.

Par1 (f a) |

(Applicative (Idiom cnv), Traversable f, MapRs cnv msg dc dc' a a') => MapRs cnv msg dc dc' (Par1 f a) (Par1 f a') |

Representation of binary type application. `f`

is a genuine `*->*->*`

type, not a representation. `a`

and `b`

are representations.

Par2 (f a b) |

(Applicative (Idiom cnv), Bitraversable f, MapRs cnv msg dc dc' a a', MapRs cnv msg dc dc' b b') => MapRs cnv msg dc dc' (Par2 f a b) (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.

## Auxilliaries

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.

# Reflection

## Fields types

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 Source

`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.

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.

## Disbanded data types

class Each IsDCOf (DCs t) => DT t whereSource

`DT`

disbands a data type if all of its fields types have `DC`

instances.

# Building fields type consumers

one :: (dc -> a) -> N dc -> aSource

`one`

extends a function that consumes a fields type to a function that
consumes a disbanded data type containing just that fields type.

(|||) :: Codomain sumL ~ Codomain sumR => (sumL -> a) -> (sumR -> a) -> (sumL :+: sumR) -> 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.

(||.) :: ~ * (Codomain sumL) (Codomain dc) => (sumL -> a) -> (dc -> a) -> :+: sumL (N dc) -> aSource

`f ||. g = f ``|||`

one g

(.||) :: ~ * (Codomain sumR) (Codomain dc) => (dc -> a) -> (sumR -> a) -> :+: (N dc) sumR -> aSource

`f .|| g = one f ``|||`

g

(.|.) :: ~ * (Codomain dc) (Codomain dc1) => (dc -> a) -> (dc1 -> a) -> :+: (N dc) (N dc1) -> aSource

`f .|. g = one f ``|||`

one g

# Operations on disbanded data types

disbanded :: Embed (N dc) (DCs (Codomain dc)) => dc -> DCs (Codomain dc)Source

`disbanded`

injects a fields type into its disbanded range

band :: forall t. Each (ConDCOf t) (DCs t) => DCs t -> tSource

`band`

s a disbanded data type back into its normal data type.

Since `Disbanded`

is a type family, the range of `band`

determines the `t`

type variable.

precise_case :: (Codomain dcs ~ t, Codomain (DCs t) ~ t, DT t, Partition (DCs t) dcs (DCs t :-: dcs)) => ((DCs t :-: dcs) -> a) -> t -> (dcs -> 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

partition :: (Codomain sum ~ Codomain sub, Partition sum sub (sum :-: sub)) => sum -> Either sub (sum :-: sub)Source

`partition`

s a sum of fields type into a specified sum of fields types and
the remaining sum.

project :: (Codomain sum ~ Codomain dc, Partition sum (N dc) (sum :-: N dc)) => sum -> Either dc (sum :-: N dc)Source

`project`

s a single fields type out of a disbanded data type.

# Forgetting `yoko`

's extra structure

reps :: EachGeneric sum => sum -> EachRep sumSource

`reps`

maps a disbanded data type to its sum-of-products representation.

class EachGeneric sum Source

Generic a => EachGeneric (N a) | |

(EachGeneric a, EachGeneric b) => EachGeneric (:+: a b) |

ig_from :: (DT t, EachGeneric (DCs t)) => t -> EachRep (DCs t)Source

`ig_from x =`

'reps $ disband' `x`

is a convenience. It approximates the
`instant-generics`

view, less the `CEq`

annotations.

type Equal a b = IsEQ (SpineCompare a b)Source

Convenient synonym. `type Equal a b = `

`IsEQ`

(`SpineCompare`

a b)

# Bundled Template Haskell

module Data.Yoko.TH