Data.Yoko.ReflectBase

The basic yoko reflection concepts.

Documentation

type family Tag dc

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

type family Recurs t

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 where

The "Datatype Constructor" class.

Associated Types

type Range dc

The range of this constructor.

Methods

occName :: Proxy (KS dc) -> String

The string name of this constructor.

tag :: DCOf (Range dc) dc

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

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

Project this constructor from its range.

fr :: RMNI dc -> Range dc

Embed this constructor in its range.

data DCOf t dc where

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

Constructors

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

Instances

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

EqT (DCU t) => EqT (DCOf t)

Finite (DCU t) => Finite (DCOf t)

data SiblingOf t s where

Constructors

SiblingOf :: (s ::: (Uni (Siblings t)), Siblings s ~ Siblings t, DT s) => Uni (Siblings t) s -> SiblingOf t s

Instances

(Siblings s ~ Siblings t, s ::: (Uni (Siblings t)), DT s) => s ::: (SiblingOf t)

EqT (SiblingOf t)

Finite (SiblingOf t)

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

The DataType class.

Associated Types

type Siblings t

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 :: * -> *

The data constructor universe. DCOf is to be preferred as much as possible.

Methods

packageName :: Proxy (KS t) -> String

The string name of this datatype's original package.

moduleName :: Proxy (KS t) -> String

The string name of this datatype's original module.

disband :: t -> Disbanded IdM t

Disband this type into one of its data constructors.