Data.PolyKinded

Lists of types and application

data LoT k where

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

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

type LoT1 a = a :&&: LoT0

type LoT2 a b = a :&&: (b :&&: LoT0)

Splitting types

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

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

Simple natural numbers.

Constructors

Z

S Nat

data TyEnv where

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

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