Portability | see LANGUAGE pragmas (... GHC) |
---|---|

Stability | experimental |

Maintainer | nicolas.frisby@gmail.com |

Safe Haskell | Safe-Infered |

This omnibus module is the only necessary import for using the `yoko`

generic
programming library.

However, some sophisticated functions' types might need to import the Data.Yoko.TypeBasics or Data.Yoko.Each modules.

The Data.Yoko.HCompos function defines the generic homomorphism; see the paper "A Pattern for Almost Homomorphic Functions" at http://www.ittc.ku.edu/~nfrisby/papers/yoko.pdf, submitted to ICFP 2012.

`dc`

type variables abstract over *fields types*.

`dcs`

and `sum`

type variables abstract over sums of *fields types*.

Types of the form

are `DCsOf`

t dcs*disbanded data types*; for each fields
type `dc`

in `dcs`

,

.
`Range`

dc ~ t

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

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

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

Sum union.

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

's first
parameter throughout the API (e.g. in `|||`

) supplants many ascriptions.

DCsOf sum |

## Products

Product union.

a :*: b |

## Fields

Representation of unary type application. `f`

is a genuine `*->*`

type,
not a representation. `a`

is a representation.

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

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

(|||) :: (DCsOf t sumL -> a) -> (DCsOf t sumR -> a) -> DCsOf t (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.

## Auxilliaries

type family DistMaybePlus a b 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

`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
type `dc`

represents.

class (Generic dc, DT (Range 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

type Disbanded t = DCsOf t (DCs t)Source

A disbanded data type is the data type's `DCs`

annotated with it.

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) -> DCsOf (Range dc) (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.

(||.) :: (DCsOf (Range dc) sumL -> a) -> (dc -> a) -> DCsOf (Range dc) (:+: sumL (N dc)) -> aSource

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

one g

(.||) :: (dc -> a) -> (DCsOf (Range dc) sumR -> a) -> DCsOf (Range dc) (:+: (N dc) sumR) -> aSource

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

g

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

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

one g

# Operations on disbanded data types

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

`disbanded`

injects a fields type into its disbanded range

band :: forall t. Each (ConDCOf t) (DCs t) => Disbanded 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.

exact_case :: (DT t, Partition (DCs t) dcs (DCs t :-: dcs)) => (DCsOf t (DCs t :-: dcs) -> a) -> t -> (DCsOf t dcs -> a) -> aSource

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

exact_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 :: Partition sum sub (sum :-: sub) => DCsOf t sum -> Either (DCsOf t sub) (DCsOf t (sum :-: sub))Source

`partition`

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

project :: Partition sum (N dc) (sum :-: N dc) => DCsOf (Range dc) sum -> Either dc (DCsOf (Range 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 => DCsOf t 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.

# Bundled Template Haskell

module Data.Yoko.TH