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 disbanded data types; for each fields
type DCsOf
t dcsdc
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