Data.YokoRaw

This is the entire library, excluding the fancy builder of precise cases from Data.Yoko.SmartPreciseCase.

Representation

Sums

data Void p1 p0

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.

Instances

Invariant2 Void

data family N dc :: * -> * -> *

The singleton sum.

data (a :+: b) p1 p0

Sum union.

Constructors

L (a p1 p0)

R (b p1 p0)

Instances

(HCompos0 * * cnv a t, HCompos0 * * cnv b t) => HCompos0 * * cnv (:+: a b) t

(FoldPlusW' k t, AreDCsOf k t l, AreDCsOf k t r) => AreDCsOf k t (:+: l r)

(Invariant2 l, Invariant2 r) => Invariant2 (:+: l r)

(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

(Eq (a p1 p0), Eq (b p1 p0)) => Eq (:+: a b p1 p0)

(Ord (a p1 p0), Ord (b p1 p0)) => Ord (:+: a b p1 p0)

(Read (a p1 p0), Read (b p1 p0)) => Read (:+: a b p1 p0)

(Show (a p1 p0), Show (b p1 p0)) => Show (:+: a b p1 p0)

newtype C dc r p1 p0

Wrapper around productus

Constructors

C (r p1 p0)

Instances

MapRs0 k k1 * * cnv msg dc dc' a a' => MapRs0 k k1 * * cnv msg dc dc' (C k2 dcA a) (C k3 dcB a')

Invariant2 r => Invariant2 (C k dc r)

Products

data U p1 p0

The empty product.

Constructors

U

Instances

Invariant2 U

Applicative (Idiom cnv) => MapRs0 k k1 * * cnv msg dc dc' U U

data (a :*: b) p1 p0

Product union.

Constructors

(a p1 p0) :*: (b p1 p0)

Instances

(MapRs0 k k1 * * cnv msg dc dc' a a', MapRs0 k k1 * * cnv msg dc dc' b b') => MapRs0 k k1 * * cnv msg dc dc' (:*: a b) (:*: a' b')

(Invariant2 l, Invariant2 r) => Invariant2 (:*: l r)

Fields

newtype T0 v t p1 p0

Constructors

T0 t

Instances

Applicative (Idiom cnv) => MapRs0 k k1 * * cnv msg dc dc' (T0 Dep a) (T0 Dep a)

Convert0 cnv a b => MapRs0 k k1 * * cnv msg dc dc' (T0 (Rec lbl) a) (T0 (Rec lbl') b)

Invariant2 (T0 v t)

newtype T1 v t a p1 p0

Constructors

T1 (t (a p1 p0))

Instances

(Traversable f, MapRs0 k k1 * * cnv msg dc dc' a a') => MapRs0 k k1 * * cnv msg dc dc' (T1 Dep f a) (T1 Dep f a')

(Invariant t, Invariant2 r) => Invariant2 (T1 v t r)

newtype T2 v t b a p1 p0

Constructors

T2 (t (b p1 p0) (a p1 p0))

Instances

(Bitraversable f, MapRs0 k k1 * * cnv msg dc dc' a a', MapRs0 k k1 * * cnv msg dc dc' b b') => MapRs0 k k1 * * cnv msg dc dc' (T2 Dep f a b) (T2 Dep f a' b')

(Invariant2 t, Invariant2 r, Invariant2 s) => Invariant2 (T2 v t r s)

data Variety

Constructors

Rec Nat

Dep

newtype Par1 p1 p0

An occurrence of the 1st parameter.

Constructors

Par1 p1

Instances

Invariant2 Par1

newtype Par0 p1 p0

An occurrence of the zeroth parameter.

Constructors

Par0 p0

Instances

Invariant2 Par0

Conversions to and from fields-of-products structure

type family Rep t :: * -> * -> *

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

class Generic dc where

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

Methods

rep :: W dc (Rep dc) p1 p0

obj :: W' dc (Rep dc) p1 p0

Instances

Generic * True_

Generic * False_

Generic * ()_

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => Generic * (:%_ a0)

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => Generic * (Just_ a0)

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => Generic * (Nothing_ a0)

Generic * (Cons_ a)

Generic * (Nil_ a)

(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => Generic * ((,)_ a0 b0)

(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => Generic * (Right_ a0 b0)

(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => Generic * (Left_ a0 b0)

(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0)), ~ Ordering EQ (Compare * (Spine * c0) (Spine * c0))) => Generic * ((,,)_ a0 b0 c0)

Generic (* -> * -> *) (,)_

Generic (* -> * -> *) Right_

Generic (* -> * -> *) Left_

Generic (* -> *) :%_

Generic (* -> *) Just_

Generic (* -> *) Nothing_

Generic (* -> *) Cons_

Generic (* -> *) Nil_

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => Generic (* -> * -> *) ((,,)_ a0)

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => Generic (* -> *) ((,)_ a0)

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => Generic (* -> *) (Right_ a0)

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => Generic (* -> *) (Left_ a0)

(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => Generic (* -> *) ((,,)_ a0 b0)

Auxilliaries

unC :: C k t t1 t2 t3 -> t1 t2 t3

foldC :: (t1 t2 t3 -> c) -> C k t t1 t2 t3 -> c

mapC :: (t1 t2 t3 -> r p1 p0) -> C k t t1 t2 t3 -> C k1 dc r p1 p0

class ComposeW dc => WN dc where

Methods

nN :: W dc (N dc) p1 p0

unN :: W' dc (N dc) p1 p0

Instances

WN * dc

WN (* -> * -> *) dc

WN (* -> *) dc

unN0 :: N * dc p1 p0 -> dc

foldN0 :: (b -> c) -> N * b p1 p0 -> c

mapN0 :: (b1 -> b) -> N * b1 p2 p3 -> N * b p1 p0

unN1 :: N (* -> *) dc p1 p0 -> dc p0

foldN1 :: (dc p0 -> c) -> N (* -> *) dc p1 p0 -> c

mapN1 :: (dc1 p3 -> dc p0) -> N (* -> *) dc1 p2 p3 -> N (* -> *) dc p1 p0

unN2 :: N (* -> * -> *) dc p1 p0 -> dc p1 p0

foldN2 :: (dc p1 p0 -> c) -> N (* -> * -> *) dc p1 p0 -> c

mapN2 :: (dc1 p2 p3 -> dc p1 p0) -> N (* -> * -> *) dc1 p2 p3 -> N (* -> * -> *) dc p1 p0

foldPlus :: (t1 t3 t4 -> t) -> (t2 t3 t4 -> t) -> :+: t1 t2 t3 t4 -> t

class FoldPlusW' s where

Methods

foldPlusW' :: W' s l p1 p0 -> W' s r p1 p0 -> W' s (l :+: r) p1 p0

Instances

FoldPlusW' * s

FoldPlusW' (* -> * -> *) s

FoldPlusW' (* -> *) s

mapPlus :: (t t2 t3 -> a p1 p0) -> (t1 t2 t3 -> b p1 p0) -> :+: t t1 t2 t3 -> :+: a b p1 p0

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

mapTimes :: (t t2 t3 -> a p1 p0) -> (t1 t2 t3 -> b p1 p0) -> :*: t t1 t2 t3 -> :*: a b p1 p0

unT0 :: T0 t t1 t2 t3 -> t1

mapT0 :: (t1 -> t4) -> T0 t t1 t2 t3 -> T0 v t4 p1 p0

unT1 :: T1 t t1 t2 t3 t4 -> t1 (t2 t3 t4)

mapT1 :: (t1 (t2 t3 t4) -> t5 (a p1 p0)) -> T1 t t1 t2 t3 t4 -> T1 v t5 a p1 p0

unT2 :: T2 t t1 t2 t3 t4 t5 -> t1 (t2 t4 t5) (t3 t4 t5)

mapT2 :: (t1 (t2 t4 t5) (t3 t4 t5) -> t6 (b p1 p0) (a p1 p0)) -> T2 t t1 t2 t3 t4 t5 -> T2 v t6 b a p1 p0

unPar0 :: Par0 t t1 -> t1

mapPar0 :: (t1 -> p0) -> Par0 t t1 -> Par0 p1 p0

unPar1 :: Par1 t t1 -> t

mapPar1 :: (t -> p1) -> Par1 t t1 -> Par1 p1 p0

type family DistMaybePlus a b :: Maybe (* -> * -> *)

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

type family Tag dc :: Digit

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

type family Codomain dc :: k

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.

type family Codomain0 dcs :: *

type family Codomain1 dcs :: * -> *

type family Codomain2 dcs :: * -> * -> *

data DTPos k

Constructors

NonRecDT

RecDT [k] [k]

type family DTs t :: DTPos k

Maps a type to its mutually recursive siblings.

type NumDTs t = NumDTs' (DTs t)

type family NumDTs' t :: Nat

type SiblingDTs t = SiblingDTs' t (DTs t)

type family SiblingDTs' t dpos :: [k]

class (Generic dc, DT (Codomain 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 :: Sym dc (Codomain dc) p1 p0

Instances

DC * True_

DC * False_

DC * ()_

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DC * (:%_ a0)

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DC * (Just_ a0)

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DC * (Nothing_ a0)

(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => DC * ((,)_ a0 b0)

(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => DC * (Right_ a0 b0)

(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => DC * (Left_ a0 b0)

(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0)), ~ Ordering EQ (Compare * (Spine * c0) (Spine * c0))) => DC * ((,,)_ a0 b0 c0)

DC (* -> * -> *) (,)_

DC (* -> * -> *) Right_

DC (* -> * -> *) Left_

DC (* -> *) :%_

DC (* -> *) Just_

DC (* -> *) Nothing_

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DC (* -> * -> *) ((,,)_ a0)

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DC (* -> *) ((,)_ a0)

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DC (* -> *) (Right_ a0)

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DC (* -> *) (Left_ a0)

(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => DC (* -> *) ((,,)_ a0 b0)

type family DCs t :: * -> * -> *

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

class DT t where

Methods

disband :: W t (DCs t) p1 p0

Instances

DT * Bool

DT * ()

~ Ordering EQ (SpineCompare * * a a) => DT * [a]

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DT * (Ratio a0)

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DT * (Maybe a0)

(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => DT * (Either a0 b0)

(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => DT * (a0, b0)

(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0)), ~ Ordering EQ (Compare * (Spine * c0) (Spine * c0))) => DT * (a0, b0, c0)

DT (* -> * -> *) Either

DT (* -> * -> *) (,)

DT (* -> *) []

DT (* -> *) Ratio

DT (* -> *) Maybe

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DT (* -> * -> *) ((,,) a0)

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DT (* -> *) (Either a0)

~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)) => DT (* -> *) ((,) a0)

(~ Ordering EQ (Compare * (Spine * a0) (Spine * a0)), ~ Ordering EQ (Compare * (Spine * b0) (Spine * b0))) => DT (* -> *) ((,,) a0 b0)

type family Eval r :: *

data SubstSpec star

Constructors

Sub0 star

Sub1 star

Sub10 star star

type family Subst spec r :: * -> * -> *

type Subst0 t p0 = Subst (Sub0 p0) (Rep t)

type Subst1 t p1 = Subst (Sub1 p1) (Rep t)

type Subst10 t p1 p0 = Subst (Sub10 p1 p0) (Rep t)

module Data.Yoko.TypeBasics

module Data.Yoko.W

Building fields type consumers

one :: (dc -> a) -> N dc p1 p0 -> a

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

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

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

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

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

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

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

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

Operations on disbanded data types

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

disbanded injects a fields type into its disbanded range

class AreDCsOf t dcs

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

Since DCs is a type family, it's the range of band that determines the t type variable.

Instances

(FoldPlusW' k t, AreDCsOf k t l, AreDCsOf k t r) => AreDCsOf k t (:+: l r)

(WN k dc, ~ k (Codomain k dc) t, DC k dc) => AreDCsOf k t (N k dc)

band :: AreDCsOf (t :: k) (DCs t) => W' t (DCs t) p1 p0

precise_case0 :: (Codomain0 dcs ~ t, Codomain0 (DCs t) ~ t, DT t, Partition (DCs t) dcs (DCs t :-: dcs)) => ((DCs t :-: dcs) p1 p0 -> a) -> t -> (dcs p1 p0 -> a) -> a

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

type family sum :-: sum2 :: * -> * -> *

class Embed sub sup

Instances

(Embed l sup, Embed r sup) => Embed (:+: l r) sup

(~ (Maybe (Path k)) (Locate k x sup) (Just (Path k) path), InjectAt (Path k) path (N k x) sup) => Embed (N k x) sup

class Partition sup subL subR

Instances

(Partition a subL subR, Partition b subL subR) => Partition (:+: a b) subL subR

Partition_N (Elem k x subL) (N k x) subL subR => Partition (N k x) subL subR

embed :: (Codomain0 sub ~ Codomain0 sup, Embed sub sup) => sub p1 p0 -> sup p1 p0

inject :: Embed (N dc) sum => dc -> sum p1 p0

injects a fields type into a sum of fields types.

partition :: (Codomain0 sum ~ Codomain0 sub, Partition sum sub (sum :-: sub)) => sum p1 p0 -> Either (sub p1 p0) ((sum :-: sub) p1 p0)

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

project :: (Codomain0 sum ~ Codomain dc, Partition sum (N dc) (sum :-: N dc)) => sum p1 p0 -> Either dc ((sum :-: N dc) p1 p0)

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

Forgetting yoko's extra structure

reps :: EachGeneric sum => sum p1 p0 -> EachRep sum p1 p0

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

class EachGeneric sum

Instances

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

(WN k dc, Generic k dc) => EachGeneric (N k dc)

type family EachRep sum :: * -> * -> *

ig_from :: (ComposeW t, DT t, EachGeneric (DCs t)) => W t (EachRep (DCs t)) p1 p0

ig_from x = 'reps $ disband' x is a convenience. It approximates the instant-generics view, less the CEq annotations.