yoko- Generic Programming with Disbanded Data Types

Portabilitysee LANGUAGE pragmas (... GHC)
Safe HaskellSafe-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 DCsOf t dcs are 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 Source

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.

newtype N a Source

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) 

data a :+: b Source

Sum union.


L a 
R b 


(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 

newtype DCsOf t sum Source

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 


Each_ cxt sum => Each_ cxt (DCsOf t sum) 
HCompos cnv sum t => HCompos cnv (DCsOf a sum) t 
Functor (DCsOf t) 


data U Source

The empty product.




Applicative (Idiom cnv) => HComposRs cnv U U 

data a :*: b Source

Product union.


a :*: b 


(HComposRs cnv a a', HComposRs cnv b b') => HComposRs cnv (:*: a b) (:*: a' b') 


newtype Rec a Source

A recursive occurrence.


Rec a 


HCompos cnv a b => HComposRs cnv (Rec a) (Rec b) 

newtype Dep a Source

A non-recursive occurrence.


Dep a 


Applicative (Idiom cnv) => HComposRs cnv (Dep a) (Dep a) 

newtype Par1 f a Source

Representation of unary type application. f is a genuine *->* type, not a representation. a is a representation.


Par1 (f a) 

newtype Par2 f a b Source

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

type family Rep a Source

A mapping to the structural representation of a fields type: just products of fields, no sums -- fields types have just one constructor.

class Generic a whereSource

Converts between a fields type and its product-of-fields structure.


rep :: a -> Rep aSource

obj :: Rep a -> aSource

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.


unDCsOf :: DCsOf t t1 -> t1Source

unN :: N t -> tSource

foldN :: (b -> c) -> N b -> cSource

mapN :: (b1 -> b) -> N b1 -> N bSource

foldPlus :: (t1 -> t) -> (t2 -> t) -> :+: t1 t2 -> tSource

mapPlus :: (t -> b) -> (t1 -> b1) -> :+: t t1 -> :+: b b1Source

foldTimes :: (t3 -> t4 -> t) -> (t1 -> t3) -> (t2 -> t4) -> :*: t1 t2 -> tSource

mapTimes :: (t -> a) -> (t1 -> b) -> :*: t t1 -> :*: a bSource

unRec :: Rec t -> tSource

mapRec :: (t -> a) -> Rec t -> Rec aSource

unDep :: Dep t -> tSource

unPar1 :: Par1 t t1 -> t t1Source

unPar2 :: Par2 t t1 t2 -> t t1 t2Source

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


Fields types

type family Tag dc Source

Tag returns a simulated type-level string that is the name of the constructor that the dc fields type represents.

type family Range dc Source

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.


rejoin :: dc -> Range dcSource

Disbanded data types

type family DCs t Source

The DCs of a data type is sum of all of its fields 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.


disband :: t -> Disbanded tSource

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

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

class (Range dc ~ t, DC dc) => ConDCOf t dc Source


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

type family sum :-: sum2 Source

class Embed sub sup Source


(~ * (Locate x sup) (Just path), InjectAt path x sup) => Embed (N x) sup 
(Embed l sup, Embed r sup) => Embed (:+: l r) sup 

class Partition sup subL subR Source


Partition_N (Elem x subL) x subL subR => Partition (N x) subL subR 
(Partition a subL subR, Partition b subL subR) => Partition (:+: a b) subL subR 

inject :: Embed (N dc) sum => dc -> sumSource

injects a fields type into a sum of fields types.

partition :: Partition sum sub (sum :-: sub) => DCsOf t sum -> Either (DCsOf t sub) (DCsOf t (sum :-: sub))Source

partitions 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

projects 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


type family EachRep sum Source

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 (Compare a b)Source

Convenient synonym. type Equal a b = IsEQ (Compare a b)

Bundled Template Haskell