Safe Haskell	Safe
Language	Haskell2010

Data.PolyKinded

Contents

Lists of types and application
Splitting types

Synopsis

data LoT k where
- LoT0 :: LoT *
- (:&&:) :: k -> LoT ks -> LoT (k -> ks)
type family (f :: k) :@@: (tys :: LoT k) :: * where ...
type LoT1 a = a :&&: LoT0
type LoT2 a b = a :&&: (b :&&: LoT0)
type SplitF (t :: d) (f :: k) = SplitF' t f LoT0
data Nat
- = Z
- | S Nat
data TyEnv where
- TyEnv :: forall k. k -> LoT k -> TyEnv
type family SplitN (n :: Nat) t :: TyEnv where ...

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

type LoT1 a = a :&&: LoT0 Source #

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

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