Type.Yoko.Universe

Type universes.

Documentation

class a ::: u where

A universe determines a set of types; open or closed. (:::) is comparable to the Sat class (e.g. from SYB3).

Methods

inhabits :: u a

Instances

a ::: NoneD

DC dc => dc ::: IsDC

a ~ b => b ::: (:=: a)

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

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

(Dom fn t ~ ex0 (ex1 ex2), Rng fn t ~ ex3 (ex4 ex5), t ::: (Domain fn)) => t ::: (Domain (AsComp fn))

(f t) ::: (Domain fn) => t ::: (Domain (:. fn f))

(Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t, t ::: (Domain fn)) => t ::: (YieldsArrowTSSD fn)

a ::: (Domain (FromAt m n))

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

(t ~ LeftmostRange (DCs t), Reduce m (DCs t)) => t ::: (ReduceD m)

U ::: (Domain (RMMap u fn m))

U ::: (Domain (CMap fn m))

Applicative (Idiom (fn m)) => U ::: (DomainA (CMap fn m))

V ::: (All u)

V ::: (Domain (CMap fn m))

Applicative (Idiom (fn m)) => V ::: (DomainA (CMap fn m))

(f t) ::: u => t ::: (:. u f)

(False ~ Pred u a, a ::: v) => a ::: (:? (:|| u v) False)

(True ~ Pred u a, a ::: u) => a ::: (:? (:|| u v) True)

(anno ~ Pred u a, a ::: (:? (:|| u v) anno)) => a ::: (:|| u v)

(a ::: u, a ::: v) => a ::: (:&& u v)

(Tag dc ~ tag, c ~ Rep dc) => dc ::: (TagRepIs tag c)

(Generic dc, (Rep dc) ::: (DomainA (CMap fn IdM)), t ::: (HasTagRepDCImageD (fn IdM) dc)) => dc ::: (ImageInDTDA t fn)

(Generic dc, (Rep dc) ::: (Domain (CMap fn IdM)), t ::: (HasTagRepDCImageD (fn IdM) dc)) => dc ::: (ImageInDTD t fn)

(DT t, (DCs t) ::: (Exists (:&& (DCOf t) (TagRepIs tag c)))) => t ::: (HasTagRepDCD tag c)

(ts ~ Siblings t, DT t, t ::: (Uni ts), (DCs t) ::: (All (YieldsArrowTSSD (AsComp (:. (RMMap (SiblingsU t) (FromAt m) IdM) N)))), ts ::: (All (CataD ts m))) => t ::: (CataD ts m)

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

((Rep t) ::: (Domain (RMMap u fn m)), Generic t) => (N t) ::: (Domain (RMMap u fn m))

(Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med (MApp fn m) t, t ::: u, t ::: (Domain (fn m)), Wrapper (fn m)) => (R t) ::: (Domain (RMMap u fn m))

(Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med m (TApp (fn m) t), t ::: (DomainA (fn m)), Functor (Idiom (fn m)), Wrapper (fn m)) => (R t) ::: (DomainA (CMap fn m))

(Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med m (TApp (fn m) t), t ::: (Domain (fn m)), Wrapper (fn m)) => (R t) ::: (Domain (CMap fn m))

(D a) ::: (Domain (RMMap u fn m))

Applicative (Idiom (fn m)) => (D a) ::: (DomainA (CMap fn m))

(D a) ::: (Domain (CMap fn m))

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

c ::: (Domain (RMMap u fn m)) => (M i c) ::: (Domain (RMMap u fn m))

(c ::: (DomainA (CMap fn m)), Functor (Idiom (fn m))) => (M i c) ::: (DomainA (CMap fn m))

c ::: (Domain (CMap fn m)) => (M i c) ::: (Domain (CMap fn m))

(Functor f, c ::: (Domain (RMMap u fn m))) => (F f c) ::: (Domain (RMMap u fn m))

(c ::: (DomainA (CMap fn m)), Applicative (Idiom (fn m)), Traversable f) => (F f c) ::: (DomainA (CMap fn m))

(c ::: (Domain (CMap fn m)), Traversable f) => (F f c) ::: (Domain (CMap fn m))

(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))

(c ::: (Domain (RMMap u fn m)), d ::: (Domain (RMMap u fn m)), FunctorTSTSS ff) => (FF ff c d) ::: (Domain (RMMap u fn m))

(c ::: (DomainA (CMap fn m)), d ::: (DomainA (CMap fn m)), Applicative (Idiom (fn m)), TraversableTSTSS ff) => (FF ff c d) ::: (DomainA (CMap fn m))

(c ::: (Domain (CMap fn m)), d ::: (Domain (CMap fn m)), FunctorTSTSS ff) => (FF ff c d) ::: (Domain (CMap fn m))

data (u :? anno) a

(:?) helps us write guarded (:::) instances (see http://hackage.haskell.org/trac/ghc/ticket/5590)

Constructors

Anno (u a)

Instances

(False ~ Pred u a, a ::: v) => a ::: (:? (:|| u v) False)

(True ~ Pred u a, a ::: u) => a ::: (:? (:|| u v) True)

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))

inhabits_ :: forall a u anno. a ::: (u :? anno) => Proxy (KS anno) -> u a

For use with (:::) instances that use (:?).

inhabitsFor :: t ::: u => Proxy (KS t) -> u t

Sometimes it's helpful to specify which t must be in the universe.

data NoneD a

The universe of all types; it has no contraints.

Constructors

NoneD

Instances

a ::: NoneD

type Both = :&&

data (u :&& v) a where

Universe product.

Constructors

:&& :: (a ::: u, a ::: v) => u a -> v a -> (u :&& v) a

Fields

fstD :: u a

sndD :: v a

Instances

(a ::: u, a ::: v) => a ::: (:&& u v)

data (u :|| v) a where

Universe sum.

Constructors

LeftD :: u a -> (u :|| v) a

RightD :: v a -> (u :|| v) a

Instances

(False ~ Pred u a, a ::: v) => a ::: (:? (:|| u v) False)

(True ~ Pred u a, a ::: u) => a ::: (:? (:|| u v) True)

(anno ~ Pred u a, a ::: (:? (:|| u v) anno)) => a ::: (:|| u v)

data VoidU t

The empty universe.

Constructors

VoidU