|Portability||see LANGUAGE pragmas (... GHC)|
yoko reflection concepts.
- type family Tag dc
- type family Recurs t
- class (DT (Range dc), dc ::: (DCU (Range dc)), Generic dc) => DC dc where
- data DCOf t dc where
- data SiblingOf t s where
- type AnRMN m u = NP u (RM m :. N)
- type Disbanded m t = AnRMN m (DCOf t)
- disbanded :: DC dc => RMN m dc -> Disbanded m (Range dc)
- band :: Disbanded IdM t -> t
- type family LeftmostRange dcs
- type DCs t = Inhabitants (DCOf t)
- class (Finite (DCU t), EqT (DCU t), (DCs t) ::: (All (DCOf t)), (Siblings t) ::: (All (SiblingOf t))) => DT t where
Tag of a constructor type is a type-level reflection of its
Recurs of a constructor type is the type-Type.Yoko.Sum of types
that occur in this constructor. NB:
Recurs t .
isSubsumedBy Siblings (Range
The "Datatype Constructor" class.
The string name of this constructor.
The evidence that this constructor inhabits the datatype constructor universe of its range.
Project this constructor from its range.
Embed this constructor in its range.
t is the range of the constructor type
|SiblingOf :: (s ::: (Uni (Siblings t)), Siblings s ~ Siblings t, DT s) => Uni (Siblings t) s -> SiblingOf t s|
The DataType class.
A type-sum of the types in this type's binding group, including
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
Recurs . DCs, by definition.)
The data constructor universe.
DCOf is to be preferred as much as