yoko-0.1: generic programming with disbanded constructors

Portabilitysee LANGUAGE pragmas (... GHC)



The basic yoko reflection concepts.



type family Tag dc Source

The Tag of a constructor type is a type-level reflection of its constructor name.

type family Recurs t Source

The Recurs of a constructor type is the type-Type.Yoko.Sum of types that occur in this constructor. NB: Recurs t isSubsumedBy Siblings (Range dc).

class (DT (Range dc), dc ::: (DCU (Range dc)), Generic dc) => DC dc whereSource

The "Datatype Constructor" class.

Associated Types

type Range dc Source

The range of this constructor.


occName :: Proxy (KS dc) -> StringSource

The string name of this constructor.

tag :: DCU (Range dc) dcSource

The evidence that this constructor inhabits the datatype constructor universe of its range.

to :: Range dc -> Maybe (RMNI dc)Source

Project this constructor from its range.

fr :: RMNI dc -> Range dcSource

Embed this constructor in its range.

data DCOf t dc whereSource

Evidence that t is the range of the constructor type dc.


DCOf :: (DC dc, t ~ Range dc) => DCU t dc -> DCOf t dc 


(t ~ Range dc, DC dc) => dc ::: (DCOf t) 
Finite (DCU t) => Finite (DCOf t) 

class UniqueDC dc whereSource

UniqueDC is for newtypes and GADT constructors where the type dc determines the constructor.


uniqueTo :: Range dc -> RMNI dcSource

type AnRMN m u = NP u (RM m :. N)Source

type Disbanded m t = AnRMN m (DCOf t)Source

disbanded :: DC dc => RMN m dc -> Disbanded m (Range dc)Source

type family LeftmostRange dcs Source

class (Finite (DCU t), EqT (DCU t), (DCs t) ::: (All (DCOf t)), (Siblings t) ::: TSum) => DT t whereSource

The DataType class.

Associated Types

type Siblings t Source

A type-sum of the types in this type's binding group, including itself. Siblings t ought to be the same for every type t in the binding group. (It also ought to be equivalent to the transitive closure of Recurs . DCs, by definition.)

data DCU t :: * -> *Source

The data constructor universe.


packageName :: Proxy (KS t) -> StringSource

The string name of this datatype's original package.

moduleName :: Proxy (KS t) -> StringSource

The string name of this datatype's original module.

disband :: t -> Disbanded IdM tSource

Disband this type into one of its data constructors.