Type.Yoko.Sum

Finite sums of types.

Documentation

data t :+ s

Type-sum union. We re-use N as type-sum singleton and V as the empty type-sum.

Instances

(Med m (LeftmostRange ts) ~ Med m (LeftmostRange us), Reduce m ts, Reduce m us) => Reduce m (:+ ts us)

(c ::: (All u), d ::: (All u)) => (:+ c d) ::: (All u)

d ::: (:? (Exists p) path) => (:+ c d) ::: (:? (Exists p) (OnRight path))

c ::: (:? (Exists p) path) => (:+ c d) ::: (:? (Exists p) (OnLeft path))

data All u c where

The higher-order universe All. c inhabits All u if c is a type-sum and all types in it inhabit u.

Constructors

SumV :: All u V

SumN :: t ::: u => u t -> All u (N t)

SumS :: All u c -> All u d -> All u (c :+ d)

Instances

V ::: (All u)

t ::: u => (N t) ::: (All u)

(c ::: (All u), d ::: (All u)) => (:+ c d) ::: (All u)

type TSum = All NoneD

All NoneD is satisfied by any type-sum.

data Exists p c where

The higher-order universe Exists. c inhabits Exists p if there exists a type t in the type-sum c for which True ~ Pred p t. NB that c is not necessarily a type-sum; i.e. there is no well-typed total function from Exists p c to TSum c.

Constructors

Here :: p t -> Exists p (N t)

OnLeft :: Exists p c -> Exists p (c :+ d)

OnRight :: Exists p d -> Exists p (c :+ d)

Instances

(Just path ~ Find p c, c ::: (:? (Exists p) path)) => c ::: (Exists p)

t ::: p => (N t) ::: (:? (Exists p) Here)

d ::: (:? (Exists p) path) => (:+ c d) ::: (:? (Exists p) (OnRight path))

c ::: (:? (Exists p) path) => (:+ c d) ::: (:? (Exists p) (OnLeft path))

type Elem t ts = IsJust (Find (:=: t) ts)

Elem t ts is True if t occurs in the type sum ts.