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.