Portability | see LANGUAGE pragmas (... GHC) |
---|---|
Stability | experimental |
Maintainer | nicolas.frisby@gmail.com |
Type universes.
Documentation
A universe determines a set of types; open or closed. (:::)
is
comparable to the Sat
class (e.g. from SYB3
).
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)) |
(:?)
helps us write guarded (:::)
instances (see
http://hackage.haskell.org/trac/ghc/ticket/5590)
Anno (u a) |
(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.
Universe product.
Universe sum.