Data.HList.HArray

The HList library

(C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke

Array-like access to HLists.

Lookup

class HLookupByHNat n l where

Associated Types

type HLookupByHNatR n l :: *

Methods

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

Instances

HLookupByHNat HZero (: * e l)

HLookupByHNat n l => HLookupByHNat (HSucc n) (: * e l)

Delete

class HDeleteAtHNat n l where

Associated Types

type HDeleteAtHNatR n l :: [*]

Methods

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

Instances

HDeleteAtHNat HZero (: * e l)

HDeleteAtHNat n l => HDeleteAtHNat (HSucc n) (: * e l)

Update

class HUpdateAtHNat n e l where

Associated Types

type HUpdateAtHNatR n e l :: [*]

Methods

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

Instances

HUpdateAtHNat HZero e1 (: * e l)

HUpdateAtHNat n e1 l => HUpdateAtHNat (HSucc n) e1 (: * e l)

Projection

hProjectByHNats' :: (HMapAux (FHLookupByHNat l) as' bs', SameLength [*] [*] bs' as', SameLength [*] [*] as' bs') => HList as' -> HList l -> HList bs'

newtype FHLookupByHNat l

Constructors

FHLookupByHNat (HList l)

Instances

HLookupByHNat n l => Apply (FHLookupByHNat l) (Proxy HNat n)

hProjectByHNats :: (Apply (FHUProj True ns) (t, Proxy HNat HZero), HUnfold' (FHUProj True ns) (ApplyR (FHUProj True ns) (t, Proxy HNat HZero))) => Proxy [HNat] ns -> t -> HList (HUnfold (FHUProj True ns) (t, Proxy HNat HZero))

data FHUProj sel ns

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)

Apply (Proxy Bool True, FHUProj sel ns) (HList (: * e l), Proxy HNat n)

(~ * 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)

Apply (FHUProj sel ns) (HList ([] *), n)

type family KMember n ns :: Bool

type HProjectByHNatsR ns l = HUnfold (FHUProj True ns) (HList l, Proxy HZero)

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

Complement of Projection

hProjectAwayByHNats :: (Apply (FHUProj False ns) (t, Proxy HNat HZero), HUnfold' (FHUProj False ns) (ApplyR (FHUProj False ns) (t, Proxy HNat HZero))) => Proxy [HNat] ns -> t -> HList (HUnfold (FHUProj False ns) (t, Proxy HNat HZero))

type HProjectAwayByHNatsR ns l = HUnfold (FHUProj False ns) (HList l, Proxy HZero)

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

Splitting

hSplitByHNats :: (Apply (FHUProj True ns) (t, Proxy HNat HZero), Apply (FHUProj False ns) (t, Proxy HNat HZero), HUnfold' (FHUProj True ns) (ApplyR (FHUProj True ns) (t, Proxy HNat HZero)), HUnfold' (FHUProj False ns) (ApplyR (FHUProj False ns) (t, Proxy HNat HZero))) => Proxy [HNat] ns -> t -> (HList (HUnfold (FHUProj True ns) (t, Proxy HNat HZero)), HList (HUnfold (FHUProj False ns) (t, Proxy HNat HZero)))

Splitting an array according to indices