Yggdrasil.HList

Provides heterogeneous lists through HList, as well as some type and value level operations on them.

Documentation

data HList :: [*] -> * where

A heterogeneous list.

Constructors

Nil :: HList '[]

(:::) :: a -> HList as -> HList (a ': as) infixr 5

type family (as :: [k]) +|+ (bs :: [k]) :: [k] where ...

Type-level appending of lists.

Equations

'[] +|+ bs = bs

(a ': as) +|+ bs = a ': (as +|+ bs)

class HAppend as bs where

Value-level appending of HLists.

Minimal complete definition

(+++)

Methods

(+++) :: HList as -> HList bs -> HList (as +|+ bs)

Instances

HAppend ([] :: [*]) bs

Defined in Yggdrasil.HList

Methods

(+++) :: HList [] -> HList bs -> HList ([] +|+ bs)

HAppend as bs => HAppend (a ': as) bs

Defined in Yggdrasil.HList

Methods

(+++) :: HList (a ': as) -> HList bs -> HList ((a ': as) +|+ bs)

class HSplit hs as bs where

Split a HList at the value level given the type-level components.

Minimal complete definition

hsplit

Methods

hsplit :: HList hs -> (HList as, HList bs)

Instances

HSplit bs ([] :: [*]) bs

Defined in Yggdrasil.HList

Methods

hsplit :: HList bs -> (HList [], HList bs)

HSplit hs as bs => HSplit (a ': hs) (a ': as) bs

Defined in Yggdrasil.HList

Methods

hsplit :: HList (a ': hs) -> (HList (a ': as), HList bs)