Control.Effect.Helpers.List

Documentation

data List (l :: [*]) where

Constructors

Nil :: List '[]

Cons :: x -> List xs -> List (x ': xs)

type family (s :: [*]) :++ (t :: [*]) :: [*] where ...

Equations

'[] :++ ys = ys

(x ': xs) :++ ys = x ': (xs :++ ys)

append :: List s -> List t -> List (s :++ t)

class Split (s :: [*]) (t :: [*]) where

Minimal complete definition

split

Methods

split :: List (s :++ t) -> (List s, List t)

Instances

Split ([] *) xs

Methods

split :: List ([*] :++ xs) -> (List [*], List xs)

Split xs ys => Split ((:) * x xs) ys

Methods

split :: List ((* ': x) xs :++ ys) -> (List ((* ': x) xs), List ys)

lengthL :: List xs -> Int

type family LookupT k xs where ...

Equations

LookupT k '[] = Maybe ()

LookupT k ((k, x) ': xs) = Maybe x

LookupT k ((j, x) ': xs) = LookupT k xs

class LookUpA k xs (LookupT k xs) => Lookup k xs where

Methods

lookup :: List xs -> Proxy k -> Maybe (LookupT k xs)

class LookUpA k xs x where

Minimal complete definition

lookupA

Methods

lookupA :: List xs -> Proxy k -> Maybe x

Instances

LookUpA k1 k2 xs y => LookUpA k1 k2 ((:) * (j, x) xs) y

Methods

lookupA :: List y -> Proxy k2 ((* ': (j, x)) xs) -> Maybe x

LookUpA * k ((:) * (k, x) xs) x

Methods

lookupA :: List x -> Proxy k ((* ': (k, x)) xs) -> Maybe x