yoko-0.1: generic programming with disbanded constructors

Portabilitysee LANGUAGE pragmas (... GHC)



Operators for the type-sums from Type.Yoko.Sum.



type Inu t = Exists (:=: t)Source

Inu t is a universe of type-sums containing t.

newtype Uni ts t Source

Uni ts is a universe containing the types in the type-sum ts.


Uni (Inu t ts) 


ts ::: (Inu t) => t ::: (Uni ts) 
ts ::: TSum => EqT (Uni ts) 
Finite (Uni ts) => Etinif (Uni ts) 
ts ::: TSum => Finite (Uni ts) 

type family PrimUni ts :: * -> *Source

A Uni ts t value can also be understood in terms of more primitive universes, VoidU, :=: and :|| for V, N, and :+, respectively.

primUni :: Uni ts t -> PrimUni ts tSource

primUni1 :: Uni (ts :+ us) t -> (Uni ts :|| Uni us) tSource

type family Inhabitants u Source

Finite universes can be represented as type-sums.

class (Inhabitants u) ::: TSum => Finite u whereSource


toUni :: u t -> Uni (Inhabitants u) tSource


ts ::: TSum => Finite (Uni ts) 
Finite (DCU t) => Finite (DCOf t) 

class Finite u => Etinif u whereSource

fromUni sometimes requires a stronger context than does toUni, so we separate the two methods.


fromUni :: Uni (Inhabitants u) t -> u tSource


Finite (Uni ts) => Etinif (Uni ts) 

eqTFin :: (Inhabitants u ~ Inhabitants v, Finite u, Finite v) => u a -> v b -> Maybe (a :=: b)Source

Any finite universe can be used to determine type equality.

type family Norm c Source

Norm uses NormW to remove duplicates from (i.e. normalize) a type-sum.

type family NormW c acc Source

NormW combines two type-sums into a right-associated type-sum containing no duplicates.

type Each ts = NT (Uni ts)Source

Each ts f provides a NT t f for each t in the type-sum ts.

one_ :: Proxy (KTSS f) -> Unwrap f t -> Each (N t) fSource

one :: Unwrap f t -> Each (N t) fSource

oneF :: Wrapper f => f t -> Each (N t) fSource

both, (|||) :: Each ts f -> Each us f -> Each (ts :+ us) fSource

(.|.) :: Wrapper f => Unwrap f t -> Unwrap f s -> Each (N t :+ N s) fSource

(||.) :: Wrapper f => Each ts f -> Unwrap f t -> Each (ts :+ N t) fSource

(.||) :: Wrapper f => Unwrap f t -> Each ts f -> Each (N t :+ ts) fSource

each :: forall u ts f. ts ::: (All u) => Proxy (KTSS u) -> (forall a. u a -> Unwrap f a) -> Each ts fSource

each is the principal means of defining an Each value.

eachF :: forall u ts f. (Wrapper f, ts ::: (All u)) => Proxy (KTSS u) -> (forall a. u a -> f a) -> Each ts fSource

eachF_ :: forall f ts. (Wrapper f, ts ::: (All NoneD)) => (forall a. f a) -> Each ts fSource

prjEach :: Uni ts t -> Each ts f -> Unwrap f tSource

Just a specialization: prjEach x f = appNT f x.

prjEachF :: Wrapper f => Uni ts t -> Each ts f -> f tSource

eachOrNT :: forall u v f w. ((Inhabitants v) ::: (All (u :|| w)), Finite v) => NT u f -> NT w f -> NT v fSource

eachOrNT fs gs builds an NT that uses fs for as many types in the universe v as possible, and uses gs for the rest. It's an extension of orNT to Each.