Portability | see LANGUAGE pragmas (... GHC) |
---|---|
Stability | experimental |
Maintainer | nicolas.frisby@gmail.com |
The basic 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
Documentation
The Tag
of a constructor type is a type-level reflection of its
constructor name.
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.
occName :: Proxy (KS dc) -> StringSource
The string name of this constructor.
tag :: DCOf (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.
Evidence that t
is the range of the constructor type dc
.
type family LeftmostRange dcs Source
type DCs t = Inhabitants (DCOf t)Source
class (Finite (DCU t), EqT (DCU t), (DCs t) ::: (All (DCOf t)), (Siblings t) ::: (All (SiblingOf t))) => DT t whereSource
The DataType class.
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.)
The data constructor universe. DCOf
is to be preferred as much as
possible.