yoko-0.2: generic programming with disbanded constructors

Portabilitysee LANGUAGE pragmas (... GHC)



Some fundamental types central to yoko.



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

type family Med m a Source

The Med type family encodes the behavior of recursion mediators.

data IdM Source

type instance Med IdM a = a.



class Wrapper f whereSource

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


wrap :: Unwrap f a -> f aSource

unwrap :: f a -> Unwrap f aSource


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 Source

type family Pred p a Source

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 Source

Composition of * -> * types.


Compose (f (g a)) 


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

Explicitly takes the inner type as a proxy.

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.


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


EqT (:=: a) 
EqT (Uni ts) 
EqT (SiblingOf t) 
EqT (DCU t) => EqT (DCOf t) 

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.


Refl :: :=: a a 


Category :=: 
a ~ b => b ::: (:=: a) 
EqT (:=: a) 
Etinif (:=: t) 
Finite (:=: t) 
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.