Type.Yoko.BTree

Operators for the type-sums from Type.Yoko.Sum.

Documentation

type Inu t = Exists (:=: t)

Inu t is a universe of type-sums containing t.

newtype Uni ts t

Uni ts is a universe containing the types in the type-sum ts.

Constructors

Uni (Inu t ts)

Instances

ts ::: (Inu t) => t ::: (Uni ts)

ts ::: TSum => EqT (Uni ts)

Finite (Uni ts) => Etinif (Uni ts)

ts ::: TSum => Finite (Uni ts)

type family PrimUni ts :: * -> *

A Uni ts t value can also be understood in terms of more primitive universes, VoidU, :=: and :|| for V, N, and :+, respectively.

primUni :: Uni ts t -> PrimUni ts t

primUni1 :: Uni (ts :+ us) t -> (Uni ts :|| Uni us) t

type family Inhabitants u

Finite universes can be represented as type-sums.

class (Inhabitants u) ::: TSum => Finite u where

Methods

toUni :: u t -> Uni (Inhabitants u) t

Instances

ts ::: TSum => Finite (Uni ts)

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

class Finite u => Etinif u where

fromUni sometimes requires a stronger context than does toUni, so we separate the two methods.

Methods

fromUni :: Uni (Inhabitants u) t -> u t

Instances

Finite (Uni ts) => Etinif (Uni ts)

eqTFin :: (Inhabitants u ~ Inhabitants v, Finite u, Finite v) => u a -> v b -> Maybe (a :=: b)

Any finite universe can be used to determine type equality.

type family Norm c

Norm uses NormW to remove duplicates from (i.e. normalize) a type-sum.

type family NormW c acc

NormW combines two type-sums into a right-associated type-sum containing no duplicates.

type Each ts = NT (Uni ts)

Each ts f provides a NT t f for each t in the type-sum ts.

none :: String -> Each V f

one_ :: Proxy (KTSS f) -> Unwrap f t -> Each (N t) f

one :: Unwrap f t -> Each (N t) f

oneF :: Wrapper f => f t -> Each (N t) f

both, (|||) :: Each ts f -> Each us f -> Each (ts :+ us) f

(.|.) :: Wrapper f => Unwrap f t -> Unwrap f s -> Each (N t :+ N s) f

(||.) :: Wrapper f => Each ts f -> Unwrap f t -> Each (ts :+ N t) f

(.||) :: Wrapper f => Unwrap f t -> Each ts f -> Each (N t :+ ts) f

each :: forall u ts f. ts ::: (All u) => Proxy (KTSS u) -> (forall a. u a -> Unwrap f a) -> Each ts f

each is the principal means of defining an Each value.

eachF :: forall u ts f. (Wrapper f, ts ::: (All u)) => Proxy (KTSS u) -> (forall a. u a -> f a) -> Each ts f

eachF_ :: forall f ts. (Wrapper f, ts ::: (All NoneD)) => (forall a. f a) -> Each ts f

prjEach :: Uni ts t -> Each ts f -> Unwrap f t

Just a specialization: prjEach x f = appNT f x.

prjEachF :: Wrapper f => Uni ts t -> Each ts f -> f t

eachOrNT :: forall u v f w. ((Inhabitants v) ::: (All (u :|| w)), Finite v) => NT u f -> NT w f -> NT v f

eachOrNT fs gs builds an NT that uses fs for as many types in the universe v as possible, and uses gs for the rest. It's an extension of orNT to Each.