Data.Yoko

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.

Representation

Sums

data Void

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

The singleton sum.

Constructors

N a

Instances

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

Sum union.

Constructors

L a

R b

Instances

(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

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.

Constructors

DCsOf sum

Instances

Each_ cxt sum => Each_ cxt (DCsOf t sum)

HCompos cnv sum t => HCompos cnv (DCsOf a sum) t

Functor (DCsOf t)

Products

data U

The empty product.

Constructors

U

Instances

Applicative (Idiom cnv) => HComposRs cnv U U

data a :*: b

Product union.

Constructors

a :*: b

Instances

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

Fields

newtype Rec a

A recursive occurrence.

Constructors

Rec a

Instances

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

newtype Dep a

A non-recursive occurrence.

Constructors

Dep a

Instances

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

newtype Par1 f a

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

Constructors

Par1 (f a)

newtype Par2 f a b

Representation of binary type application. f is a genuine *->*->* type, not a representation. a and b are representations.

Constructors

Par2 (f a b)

Conversions to and from fields-of-products structure

type family Rep a

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 where

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

Methods

rep :: a -> Rep a

obj :: Rep a -> a

Building disbanded data type consumers

(|||) :: (DCsOf t sumL -> a) -> (DCsOf t sumR -> a) -> DCsOf t (sumL :+: sumR) -> a

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

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

We avoid empty sums with a type-level Maybe. DistMaybePlus performs sum union on lifted sums, only introducing :+: when both arguments are Justs.

Reflection

Fields types

type family Tag dc

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

type family Range dc

Range is the data type that contains the constructor that the fields type dc represents.

class (Generic dc, DT (Range dc)) => DC dc where

Any fields type can be further represented as a product-of-fields and can be injected back into the original data type.

Methods

rejoin :: dc -> Range dc

Disbanded data types

type family DCs t

The DCs of a data type is sum of all of its fields types.

type Disbanded t = DCsOf t (DCs t)

A disbanded data type is the data type's DCs annotated with it.

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

DT disbands a data type if all of its fields types have DC instances.

Methods

disband :: t -> Disbanded t

Building fields type consumers

one :: (dc -> a) -> DCsOf (Range dc) (N dc) -> a

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

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

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

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

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

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

Operations on disbanded data types

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

disbanded injects a fields type into its disbanded range

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

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

Instances

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

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

class Embed sub sup

Instances

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

Instances

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

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

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

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

Forgetting yoko's extra structure

reps :: EachGeneric sum => DCsOf t sum -> EachRep sum

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

class EachGeneric sum

Instances

Generic a => EachGeneric (N a)

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

type family EachRep sum

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

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)

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

Bundled Template Haskell

module Data.Yoko.TH