Safe Haskell	None
Language	Haskell2010

Data.HList.HArray

Contents

Lookup
Delete
Update
Projection
Complement of Projection
Splitting

Description

The HList library

Array-like access to HLists.

Synopsis

Lookup

class HLookupByHNat (n :: HNat) (l :: [*]) where Source #

Minimal complete definition

hLookupByHNat

Associated Types

type HLookupByHNatR (n :: HNat) (l :: [*]) :: * Source #

Methods

hLookupByHNat :: Proxy n -> HList l -> HLookupByHNatR n l Source #

Instances

HLookupByHNat HZero ((:) * e l) Source #
Associated Types type HLookupByHNatR (HZero :: HNat) ((* ': e) l :: []) :: Source # Methods hLookupByHNat :: Proxy HNat HZero -> HList ((* ': e) l) -> HLookupByHNatR HZero ((* ': e) l) Source #
HLookupByHNat n l => HLookupByHNat (HSucc n) ((:) * e l) Source #
Associated Types type HLookupByHNatR (HSucc n :: HNat) ((* ': e) l :: []) :: Source # Methods hLookupByHNat :: Proxy HNat (HSucc n) -> HList ((* ': e) l) -> HLookupByHNatR (HSucc n) ((* ': e) l) Source #

Delete

class HDeleteAtHNat (n :: HNat) (l :: [*]) where Source #

Minimal complete definition

hDeleteAtHNat

Associated Types

type HDeleteAtHNatR (n :: HNat) (l :: [*]) :: [*] Source #

Methods

hDeleteAtHNat :: Proxy n -> HList l -> HList (HDeleteAtHNatR n l) Source #

Instances

HDeleteAtHNat HZero ((:) * e l) Source #
Associated Types type HDeleteAtHNatR (HZero :: HNat) ((* ': e) l :: []) :: [] Source # Methods hDeleteAtHNat :: Proxy HNat HZero -> HList ((* ': e) l) -> HList (HDeleteAtHNatR HZero ((* ': e) l)) Source #
HDeleteAtHNat n l => HDeleteAtHNat (HSucc n) ((:) * e l) Source #
Associated Types type HDeleteAtHNatR (HSucc n :: HNat) ((* ': e) l :: []) :: [] Source # Methods hDeleteAtHNat :: Proxy HNat (HSucc n) -> HList ((* ': e) l) -> HList (HDeleteAtHNatR (HSucc n) ((* ': e) l)) Source #

Update

class HUpdateAtHNat' n e l l => HUpdateAtHNat n e l where Source #

Minimal complete definition

hUpdateAtHNat

Methods

hUpdateAtHNat :: Proxy n -> e -> HList l -> HList (HUpdateAtHNatR n e l) Source #

Instances

HUpdateAtHNat' n e l l => HUpdateAtHNat n e l Source #
Methods hUpdateAtHNat :: Proxy HNat n -> e -> HList l -> HList (HUpdateAtHNatR n e l) Source #

class HUpdateAtHNat' (n :: HNat) e (l :: [*]) (l0 :: [*]) where Source #

Minimal complete definition

hUpdateAtHNat'

Associated Types

type HUpdateAtHNatR (n :: HNat) e (l :: [*]) :: [*] Source #

Methods

hUpdateAtHNat' :: Proxy l0 -> Proxy n -> e -> HList l -> HList (HUpdateAtHNatR n e l) Source #

Instances

Fail ErrorMessage (HNatIndexTooLarge * n HList l0) => HUpdateAtHNat' n e1 ([] *) l0 Source #
Associated Types type HUpdateAtHNatR (n :: HNat) e1 ([] :: []) :: [] Source # Methods hUpdateAtHNat' :: Proxy [] l0 -> Proxy HNat n -> e1 -> HList [] -> HList (HUpdateAtHNatR n e1 []) Source #
HUpdateAtHNat' HZero e1 ((:) * e l) l0 Source #
Associated Types type HUpdateAtHNatR (HZero :: HNat) e1 ((* ': e) l :: []) :: [] Source # Methods hUpdateAtHNat' :: Proxy [] l0 -> Proxy HNat HZero -> e1 -> HList (( ': e) l) -> HList (HUpdateAtHNatR HZero e1 ((* ': e) l)) Source #
HUpdateAtHNat' n e1 l l0 => HUpdateAtHNat' (HSucc n) e1 ((:) * e l) l0 Source #
Associated Types type HUpdateAtHNatR (HSucc n :: HNat) e1 ((* ': e) l :: []) :: [] Source # Methods hUpdateAtHNat' :: Proxy [] l0 -> Proxy HNat (HSucc n) -> e1 -> HList (( ': e) l) -> HList (HUpdateAtHNatR (HSucc n) e1 ((* ': e) l)) Source #

Projection

hProjectByHNats' :: (SameLength' * * a b, SameLength' * * b a, HMapAux r (FHLookupByHNat l) a b) => r a -> HList l -> r b Source #

newtype FHLookupByHNat (l :: [*]) Source #

Constructors

FHLookupByHNat (HList l)

Instances

HLookupByHNat n l => Apply (FHLookupByHNat l) (Proxy HNat n) Source #
Associated Types type ApplyR (FHLookupByHNat l) (Proxy HNat n) :: * Source # Methods apply :: FHLookupByHNat l -> Proxy HNat n -> ApplyR (FHLookupByHNat l) (Proxy HNat n) Source #
type ApplyR (FHLookupByHNat l) (Proxy HNat n) Source #
type ApplyR (FHLookupByHNat l) (Proxy HNat n) = HLookupByHNatR n l

hProjectByHNats :: (HUnfoldFD (FHUProj True ns) (ApplyR (FHUProj True ns) (a, Proxy HNat HZero)) z, Apply (FHUProj True ns) (a, Proxy HNat HZero)) => Proxy [HNat] ns -> a -> HList z Source #

data FHUProj (sel :: Bool) (ns :: [HNat]) Source #

Constructors

FHUProj

Instances

Apply (FHUProj sel ns) (HList l, Proxy HNat (HSucc n)) => Apply (Proxy Bool False, FHUProj sel ns) (HList ((:) * e l), Proxy HNat n) Source #
Associated Types type ApplyR (Proxy Bool False, FHUProj sel ns) (HList ((* ': e) l), Proxy HNat n) :: * Source # Methods apply :: (Proxy Bool False, FHUProj sel ns) -> (HList ((* ': e) l), Proxy HNat n) -> ApplyR (Proxy Bool False, FHUProj sel ns) (HList ((* ': e) l), Proxy HNat n) Source #
Apply (Proxy Bool True, FHUProj sel ns) (HList ((:) * e l), Proxy HNat n) Source #
Associated Types type ApplyR (Proxy Bool True, FHUProj sel ns) (HList ((* ': e) l), Proxy HNat n) :: * Source # Methods apply :: (Proxy Bool True, FHUProj sel ns) -> (HList ((* ': e) l), Proxy HNat n) -> ApplyR (Proxy Bool True, FHUProj sel ns) (HList ((* ': e) l), Proxy HNat n) Source #
((~) * ch (Proxy Bool (HBoolEQ sel (KMember n ns))), Apply (ch, FHUProj sel ns) (HList ((:) * e l), Proxy HNat n)) => Apply (FHUProj sel ns) (HList ((:) * e l), Proxy HNat n) Source #
Associated Types type ApplyR (FHUProj sel ns) (HList ((* ': e) l), Proxy HNat n) :: * Source # Methods apply :: FHUProj sel ns -> (HList ((* ': e) l), Proxy HNat n) -> ApplyR (FHUProj sel ns) (HList ((* ': e) l), Proxy HNat n) Source #
Apply (FHUProj sel ns) (HList ([] *), n) Source #
Associated Types type ApplyR (FHUProj sel ns) (HList [], n) :: Source # Methods apply :: FHUProj sel ns -> (HList [], n) -> ApplyR (FHUProj sel ns) (HList [], n) Source #
type ApplyR (Proxy Bool False, FHUProj sel ns) (HList ((:) * e l), Proxy HNat n) Source #
type ApplyR (Proxy Bool False, FHUProj sel ns) (HList ((:) * e l), Proxy HNat n) = ApplyR (FHUProj sel ns) (HList l, Proxy HNat (HSucc n))
type ApplyR (Proxy Bool True, FHUProj sel ns) (HList ((:) * e l), Proxy HNat n) Source #
type ApplyR (Proxy Bool True, FHUProj sel ns) (HList ((:) * e l), Proxy HNat n) = HJust (e, (HList l, Proxy HNat (HSucc n)))
type ApplyR (FHUProj sel ns) (HList ([] *), n) Source #
type ApplyR (FHUProj sel ns) (HList ([] *), n) = HNothing
type ApplyR (FHUProj sel ns) (HList ((:) * e l), Proxy HNat n) Source #
type ApplyR (FHUProj sel ns) (HList ((:) * e l), Proxy HNat n) = ApplyR (Proxy Bool (HBoolEQ sel (KMember n ns)), FHUProj sel ns) (HList ((:) * e l), Proxy HNat n)

type family KMember (n :: HNat) (ns :: [HNat]) :: Bool Source #

Instances

type KMember n ([] HNat) Source #
type KMember n ([] HNat) = False
type KMember n ((:) HNat n1 l) Source #
type KMember n ((:) HNat n1 l) = HOr (HNatEq n n1) (KMember n l)

type HProjectByHNatsR (ns :: [HNat]) (l :: [*]) = HUnfold (FHUProj True ns) (HList l, Proxy HZero) Source #

type HProjectByHNatsCtx ns l = (Apply (FHUProj True ns) (HList l, Proxy HZero), HUnfold' (FHUProj True ns) (HList l, Proxy HZero)) Source #

Complement of Projection

hProjectAwayByHNats :: (HUnfoldFD (FHUProj False ns) (ApplyR (FHUProj False ns) (a, Proxy HNat HZero)) z, Apply (FHUProj False ns) (a, Proxy HNat HZero)) => Proxy [HNat] ns -> a -> HList z Source #

type HProjectAwayByHNatsR (ns :: [HNat]) (l :: [*]) = HUnfold (FHUProj False ns) (HList l, Proxy HZero) Source #

type HProjectAwayByHNatsCtx ns l = (Apply (FHUProj False ns) (HList l, Proxy HZero), HUnfold' (FHUProj False ns) (HList l, Proxy HZero)) Source #

Splitting

hSplitByHNats :: (Apply (FHUProj False ns) (a, Proxy HNat HZero), Apply (FHUProj True ns) (a, Proxy HNat HZero), HUnfoldFD (FHUProj False ns) (ApplyR (FHUProj False ns) (a, Proxy HNat HZero)) z2, HUnfoldFD (FHUProj True ns) (ApplyR (FHUProj True ns) (a, Proxy HNat HZero)) z1) => Proxy [HNat] ns -> a -> (HList z1, HList z2) Source #

Splitting an array according to indices