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

Fail * (FieldNotFound * (Proxy HNat n, e1)) => HUpdateAtHNat n e1 ([] *)

HUpdateAtHNat HZero e1 ((:) * e l)

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

Projection

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

newtype FHLookupByHNat l

Constructors

FHLookupByHNat (HList l)

Instances

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

type ApplyR (FHLookupByHNat l) (Proxy HNat n) = HLookupByHNatR n l

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

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 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) = HJust (e, (HList l, Proxy HNat (HSucc n)))

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 ApplyR (FHUProj sel ns) (HList ([] *), n) = HNothing

type family KMember n ns :: Bool

Instances

type KMember n ([] HNat) = False

type KMember n ((:) HNat n1 l) = HOr (HNatEq n n1) (KMember n l)

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) (HList l, Proxy HZero))

Complement of Projection

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

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) (HList l, Proxy HZero))

Splitting

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

Splitting an array according to indices