yoko-0.2: generic programming with disbanded constructors

Portabilitysee LANGUAGE pragmas (... GHC)
Stabilityexperimental
Maintainernicolas.frisby@gmail.com

Type.Yoko.Universe

Description

Type universes.

Synopsis

Documentation

class a ::: u whereSource

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

Methods

inhabits :: u aSource

Instances

a ::: NoneU 
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 ::: (YieldsArrowTSSU fn) 
a ::: (Domain (FromAt m n)) 
(Siblings s ~ Siblings t, s ::: (Uni (Siblings t)), DT s) => s ::: (SiblingOf t) 
(t ~ Range dc, DC dc) => dc ::: (DCOf t) 
(DT t, AlgebraDT m t) => t ::: (AlgebraU 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 ::: (HasTagRepImageU (fn IdM) dc)) => dc ::: (ImageInDTDA t fn) 
(Generic dc, (Rep dc) ::: (Domain (CMap fn IdM)), t ::: (HasTagRepImageU (fn IdM) dc)) => dc ::: (ImageInDTU t fn) 
(DT t, (DCs t) ::: (Exists (:&& (DCOf t) (TagRepIs tag c)))) => t ::: (HasTagRepU tag c) 
(ts ~ Siblings t, DT t, ts ::: (Exists (:=: t)), (DCs t) ::: (All (YieldsArrowTSSU (AsComp (:. (RMMap (SiblingsU t) (FromAt m) IdM) N)))), ts ::: (All (CataU ts m))) => t ::: (CataU 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 Source

(:?) 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 aSource

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

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

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

data NoneU a Source

The universe of all types; it has no contraints.

Constructors

NoneU 

Instances

data (u :&& v) a whereSource

Universe product.

Constructors

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

Fields

fstU :: u a
 
sndU :: v a
 

Instances

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

data (u :|| v) a whereSource

Universe sum.

Constructors

LeftU :: u a -> (u :|| v) a 
RightU :: 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) 
(Etinif u, Etinif v) => Etinif (:|| u v) 
(Finite u, Finite v) => Finite (:|| u v) 

data VoidU t Source

The empty universe.