Data.HList.HArray

The HList library

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

Array-like access to HLists.

Lookup

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

Minimal complete definition

hLookupByHNat

Associated Types

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

Methods

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

Instances

HLookupByHNat HZero ((:) * e l)

Associated Types

type HLookupByHNatR (HZero :: HNat) ((* ': e) l :: [*]) :: *

Methods

hLookupByHNat :: Proxy HNat HZero -> HList ((* ': e) l) -> HLookupByHNatR HZero ((* ': e) l)

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

Associated Types

type HLookupByHNatR (HSucc n :: HNat) ((* ': e) l :: [*]) :: *

Methods

hLookupByHNat :: Proxy HNat (HSucc n) -> HList ((* ': e) l) -> HLookupByHNatR (HSucc n) ((* ': e) l)

Delete

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

Minimal complete definition

hDeleteAtHNat

Associated Types

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

Methods

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

Instances

HDeleteAtHNat HZero ((:) * e l)

Associated Types

type HDeleteAtHNatR (HZero :: HNat) ((* ': e) l :: [*]) :: [*]

Methods

hDeleteAtHNat :: Proxy HNat HZero -> HList ((* ': e) l) -> HList (HDeleteAtHNatR HZero ((* ': e) l))

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

Associated Types

type HDeleteAtHNatR (HSucc n :: HNat) ((* ': e) l :: [*]) :: [*]

Methods

hDeleteAtHNat :: Proxy HNat (HSucc n) -> HList ((* ': e) l) -> HList (HDeleteAtHNatR (HSucc n) ((* ': e) l))

Update

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

Minimal complete definition

hUpdateAtHNat

Methods

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

Instances

HUpdateAtHNat' n e l l => HUpdateAtHNat n e l

Methods

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

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

Minimal complete definition

hUpdateAtHNat'

Associated Types

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

Methods

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

Instances

Fail ErrorMessage (HNatIndexTooLarge * n HList l0) => HUpdateAtHNat' n e1 ([] *) l0

Associated Types

type HUpdateAtHNatR (n :: HNat) e1 ([*] :: [*]) :: [*]

Methods

hUpdateAtHNat' :: Proxy [*] l0 -> Proxy HNat n -> e1 -> HList [*] -> HList (HUpdateAtHNatR n e1 [*])

HUpdateAtHNat' HZero e1 ((:) * e l) l0

Associated Types

type HUpdateAtHNatR (HZero :: HNat) e1 ((* ': e) l :: [*]) :: [*]

Methods

hUpdateAtHNat' :: Proxy [*] l0 -> Proxy HNat HZero -> e1 -> HList ((* ': e) l) -> HList (HUpdateAtHNatR HZero e1 ((* ': e) l))

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

Associated Types

type HUpdateAtHNatR (HSucc n :: HNat) e1 ((* ': e) l :: [*]) :: [*]

Methods

hUpdateAtHNat' :: Proxy [*] l0 -> Proxy HNat (HSucc n) -> e1 -> HList ((* ': e) l) -> HList (HUpdateAtHNatR (HSucc n) e1 ((* ': e) l))

Projection

hProjectByHNats' :: (SameLength' * * a b, SameLength' * * b a, HMapAux r (FHLookupByHNat l) 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)

Associated Types

type ApplyR (FHLookupByHNat l) (Proxy HNat n) :: *

Methods

apply :: FHLookupByHNat l -> Proxy HNat n -> ApplyR (FHLookupByHNat l) (Proxy HNat n)

type ApplyR (FHLookupByHNat l) (Proxy HNat n)

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

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

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)

Associated Types

type ApplyR (Proxy Bool False, FHUProj sel ns) (HList ((* ': e) l), Proxy HNat n) :: *

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)

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

Associated Types

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

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)

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

Associated Types

type ApplyR (FHUProj sel ns) (HList ((* ': e) l), Proxy HNat n) :: *

Methods

apply :: FHUProj sel ns -> (HList ((* ': e) l), Proxy HNat n) -> ApplyR (FHUProj sel ns) (HList ((* ': e) l), Proxy HNat n)

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

Associated Types

type ApplyR (FHUProj sel ns) (HList [*], n) :: *

Methods

apply :: FHUProj sel ns -> (HList [*], n) -> ApplyR (FHUProj sel ns) (HList [*], n)

type ApplyR (Proxy Bool False, FHUProj sel ns) (HList ((:) * e l), Proxy HNat 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)

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)

type ApplyR (FHUProj sel ns) (HList ([] *), n) = HNothing

type ApplyR (FHUProj sel ns) (HList ((:) * e l), Proxy HNat 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 family KMember (n :: HNat) (ns :: [HNat]) :: Bool

Instances

type KMember n ([] HNat)

type KMember n ([] HNat) = False

type KMember n ((:) HNat n1 l)

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)

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) (a, Proxy HNat HZero)) z, Apply (FHUProj False ns) (a, Proxy HNat HZero)) => Proxy [HNat] ns -> a -> HList z

type HProjectAwayByHNatsR (ns :: [HNat]) (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 :: (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)

Splitting an array according to indices