kind-apply-0.1.0.0: Utilities to work with lists of types

Data.PolyKinded

Synopsis

# Lists of types and application

data LoT k where Source #

LoT k represents a list of types which can be applied to a data type of kind k.

Constructors

 LoT0 :: LoT * Empty list of types. (:&&:) :: k -> LoT ks -> LoT (k -> ks) infixr 5 Cons a type with a list of types.

type family (f :: k) :@@: (tys :: LoT k) :: * where ... Source #

Apply a list of types to a type constructor.

>>> :kind! Either :@@: (Int :&&: Bool :&&: LoT0)
Either Int Bool :: *


Equations

 f :@@: LoT0 = f f :@@: (a :&&: as) = f a :@@: as

# Splitting types

type SplitF (t :: d) (f :: k) = SplitF' t f LoT0 Source #

Split a type t until the constructor f is found.

>>> :kind! SplitF (Either Int Bool) Either
Int :&&: Bool :&&: LoT0 :: LoT (* -> * -> *)
>>> :kind! SplitF (Either Int Bool) (Either Int)
Bool :&&: LoT0 :: LoT (* -> *)


data Nat Source #

Simple natural numbers.

Constructors

 Z S Nat

data TyEnv where Source #

A type constructor and a list of types that can be applied to it.

Constructors

 TyEnv :: forall k. k -> LoT k -> TyEnv

type family SplitN (n :: Nat) t :: TyEnv where ... Source #

Split a type t until its list of types has length n.

>>> :kind! SplitN (Either Int Bool) (S (S Z))
TyEnv Either (Int :&&: Bool :&&: LoT0) :: TyEnv
>>> :kind! SplitF (Either Int Bool) (S Z)
TyEnv (Either Int) (Bool :&&: LoT0) :: TyEnv


Equations

 SplitN n t = SplitN' n t LoT0

class (x ~ SplitF t f, t ~ (f :@@: x)) => Split t (f :: k) (x :: LoT k) | t -> k f x Source #

Split t f x declares that the default way to split the type t is into a type constructor f and a list of types x.

instance Split (Either a b) Either (a :&&: b :&&: LoT0)