Type.Yoko.Type

Some fundamental types central to yoko.

Documentation

qK :: QuasiQuoter

[qK|...|] is the a type that takes one parameter of the corresponding kind. (The name is an encoding of that parameter's kind based on prefix notation for application.)

data Proxy p

Constructors

Proxy

Instances

Monad Proxy

Functor Proxy

Typeable1 Proxy

Applicative Proxy

Foldable Proxy

Traversable Proxy

Bounded (Proxy s)

Enum (Proxy s)

Eq (Proxy p)

Data p => Data (Proxy p)

Ord (Proxy p)

Read (Proxy p)

Show (Proxy p)

Ix (Proxy s)

Monoid (Proxy s)

Default (Proxy s)

Semigroup (Proxy s)

type family Med m a

The Med type family encodes the behavior of recursion mediators.

data IdM

type instance Med IdM a = a.

Constructors

IdM

class Wrapper f where

The Wrapper class is used to make term-level programming newtypes a little more lightweight from the user perspective.

Methods

wrap :: Unwrap f a -> f a

unwrap :: f a -> Unwrap f a

Instances

Wrapper (AsComp fn)

Wrapper (Algebra m)

Wrapper (:. f g)

Wrapper (ArrowTSS f g)

Wrapper (FromAt m n)

Wrapper (RMNTo m b)

type family Unwrap f a

type family Pred p a

The Pred type family realizes type-level predicates (over types) that yield a type-level Boolean: either True or False. Predicates are often universes.

newtype (f :. g) a

Composition of * -> * types.

Constructors

Compose (f (g a))

Instances

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

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

Wrapper (:. f g)

composeWith :: Proxy (KTSS g) -> f (g a) -> (f :. g) a

Explicitly takes the inner type as a proxy.

module Type.Spine.Stage0

module Type.Booleans

type IsEQ t = OrdCase t False True False

type Compare l r = SpineCompare (KS l) (KS r)

class EqT f where

A type class for constructing equality proofs. This is as close as we can get to decidable equality on types. Note that f must be a GADT to be able to define eqT.

Methods

eqT :: f a -> f b -> Maybe (:=: a b)

Instances

EqT (:=: a)

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

data a :=: b where

Type equality. A value of a :=: b is a proof that types a and b are equal. By pattern matching on Refl this fact is introduced to the type checker.

Constructors

Refl :: :=: a a

Instances

Category :=:

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

EqT (:=: a)

Read (:=: a a)

We can only read values if the result is a :=: a, not a :=: b since that is not true, in general. We just parse the string Refl, optionally surrounded with parentheses, and return Refl.

Show (:=: a b)

Any value is just shown as Refl, but this cannot be derived for a GADT, so it is defined here manually.