- Heterogeneous type sequences
- The set of all types of heterogeneous lists
- Public constructors
- Basic list functions
- A class for extension
- Appending HLists
- Reversing HLists
- A nicer notation for lists
- A heterogeneous apply operator
- A heterogeneous fold for all types
- Map
- Map a heterogeneous list to a homogeneous one
- A heterogenous version of mapM.
- A reconstruction of append
- A heterogeneous map for all types
- A function for showing
- Type-level equality for lists
- Staged equality for lists
- Ensure a list to contain HNats only
- Static set property based on HEq
- Find an element in a set based on HEq
- Membership test
- Intersection based on HTMember
- Turn a heterogeneous list into a homogeneous one
- With
HMaybe
- Annotated lists
- Splitting by HTrue and HFalse
The HList library
(C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
Basic declarations for typeful heterogeneous lists.
Excuse the unstructured haddocks: while there are many declarations here some are alternative implementations should be grouped, and the definitions here are analgous to many list functions in the Prelude.
- data HNil = HNil
- data HCons e l = HCons e l
- class HList l
- hNil :: HNil
- hCons :: HList l => e -> l -> HCons e l
- class HHead l h | l -> h where
- hHead :: l -> h
- class HTail l l' | l -> l' where
- hTail :: l -> l'
- class HExtend e l l' | e l -> l', l' -> e l where
- hExtend :: e -> l -> l'
- append :: [a] -> [a] -> [a]
- class HAppend l l' l'' | l l' -> l'' where
- hAppend :: l -> l' -> l''
- class HReverse l1 l2 | l1 -> l2, l2 -> l1 where
- hReverse :: l1 -> l2
- class HReverse' l1 l2 l3 | l1 l2 -> l3 where
- hReverse' :: l1 -> l2 -> l3
- class NaiveHReverse l l' | l -> l' where
- naiveHReverse :: l -> l'
- hEnd :: HCons t t1 -> HCons t t1
- hBuild :: HBuild' HNil a r => a -> r
- class HBuild' l a r | r -> a l where
- hBuild' :: l -> a -> r
- class Apply f a r | f a -> r where
- apply :: f -> a -> r
- data Id = Id
- class HList l => HFoldr f v l r | f v l -> r where
- hFoldr :: f -> v -> l -> r
- class HMap f l l' | f l -> l' where
- hMap :: f -> l -> l'
- class HMapOut f r e where
- hMapOut :: f -> r -> [e]
- hMapM :: (Monad m, HMapOut f l (m e)) => f -> l -> [m e]
- hMapM_ :: (Monad m, HMapOut f l (m ())) => f -> l -> m ()
- append' :: [a] -> [a] -> [a]
- hAppend' :: HFoldr ApplyHCons v l r => l -> v -> r
- data ApplyHCons = ApplyHCons
- data HMap' f = HMap' f
- hMap' :: HFoldr (HMap' f) HNil l r => f -> l -> r
- data HShow = HShow
- data HSeq x = HSeq x
- class HStagedEq' b e e' where
- hStagedEq' :: b -> e -> e' -> Bool
- class HList l => HNats l
- class HSet l
- class HNat n => HFind e l n | e l -> n where
- hFind :: e -> l -> n
- class HNat n => HFind' b e l n | b e l -> n where
- hFind' :: b -> e -> l -> n
- class HBool b => HMember e l b | e l -> b
- hMember :: HMember e l b => e -> l -> b
- class HMemberM e l r | e l -> r
- class HMemberM' b e l r | b e l -> r
- class HBool b => HTMember e l b | e l -> b
- hTMember :: HTMember e l b => e -> l -> b
- class HTIntersect l1 l2 l3 | l1 l2 -> l3 where
- hTIntersect :: l1 -> l2 -> l3
- class HBool b => HTIntersectBool b h t l1 l2 | b h t l1 -> l2 where
- hTIntersectBool :: b -> h -> t -> l1 -> l2
- class HList2List l e where
- hList2List :: l -> [e]
- class ToHJust l l' | l -> l' where
- toHJust :: l -> l'
- class FromHJust l l' | l -> l' where
- fromHJust :: l -> l'
- data HAddTag t = HAddTag t
- data HRmTag = HRmTag
- hAddTag :: HMap (HAddTag t) l l' => t -> l -> l'
- hRmTag :: HMap HRmTag l l' => l -> l'
- hFlag :: HMap (HAddTag HTrue) l l' => l -> l'
- class HSplit l l' l'' | l -> l' l'' where
- hSplit :: l -> (l', l'')
Heterogeneous type sequences
HCons e l |
The set of all types of heterogeneous lists
Public constructors
Basic list functions
A class for extension
class HExtend e l l' | e l -> l', l' -> e l whereSource
HExtend e HNil (HCons e HNil) | |
(HOccursNot e l, HTypeIndexed l) => HExtend e (TIP l) (TIP (HCons e l)) | |
HList l => HExtend e (HCons e' l) (HCons e (HCons e' l)) | |
HRLabelSet (HCons (LVPair l v) r) => HExtend (LVPair l v) (Record r) (Record (HCons (LVPair l v) r)) | |
(HLabelSet (HCons l ls), HSameLength ls vs) => HExtend (LVPair l v) (RecordP ls vs) (RecordP (HCons l ls) (HCons v vs)) |
Appending HLists
class HAppend l l' l'' | l l' -> l'' whereSource
The class HAppend
HList l => HAppend HNil l l | The instance following the normal append |
(HAppend l l' l'', HTypeIndexed l'') => HAppend (TIP l) (TIP l') (TIP l'') | |
(HRLabelSet r'', HAppend r r' r'') => HAppend (Record r) (Record r') (Record r'') | |
(HList l, HAppend l l' l'') => HAppend (HCons x l) l' (HCons x l'') | |
(HLabelSet ls'', HAppend ls ls' ls'', HAppend vs vs' vs'', HSameLength ls'' vs'') => HAppend (RecordP ls vs) (RecordP ls' vs') (RecordP ls'' vs'') |
Reversing HLists
Naive HReverse
class NaiveHReverse l l' | l -> l' whereSource
naiveHReverse :: l -> l'Source
NaiveHReverse HNil HNil | |
(NaiveHReverse l l', HAppend l' (HCons e HNil) l'') => NaiveHReverse (HCons e l) l'' |
A nicer notation for lists
hEnd :: HCons t t1 -> HCons t t1Source
List termination
Note:
x :: HCons a b
- means:
forall a b. x :: HCons a b
hEnd x
- means:
exists a b. x :: HCons a b
Building non-empty lists
HList> let x = hBuild True in hEnd x HCons True HNil
HList> let x = hBuild True 'a' in hEnd x HCons True (HCons 'a' HNil)
HList> let x = hBuild True 'a' "ok" in hEnd x HCons True (HCons 'a' (HCons "ok" HNil))
HList> hEnd (hBuild (Key 42) (Name "Angus") Cow (Price 75.5)) HCons (Key 42) (HCons (Name "Angus") (HCons Cow (HCons (Price 75.5) HNil)))
HList> hEnd (hBuild (Key 42) (Name "Angus") Cow (Price 75.5)) == angus True
A heterogeneous apply operator
class Apply f a r | f a -> r whereSource
Apply Id x x | |
Show x => Apply HShow x (IO ()) | |
Apply HRmTag (e, t) e | |
HList l => Apply ApplyHCons (e, l) (HCons e l) | |
Apply (HAddTag t) e (e, t) | |
(Monad m, Apply f x (m ())) => Apply (HSeq f) (x, m ()) (m ()) | |
Apply f e e' => Apply (HMap' f) (e, l) (HCons e' l) | |
Apply (x -> y) x y | Normal function application |
A heterogeneous fold for all types
Map
Map a heterogeneous list to a homogeneous one
A heterogenous version of mapM.
A reconstruction of append
hAppend' :: HFoldr ApplyHCons v l r => l -> v -> rSource
A heterogeneous map for all types
hMap' :: HFoldr (HMap' f) HNil l r => f -> l -> rSource
Same as hMap
only a different implementation.
A function for showing
Type-level equality for lists
Staged equality for lists
class HStagedEq' b e e' whereSource
hStagedEq' :: b -> e -> e' -> BoolSource
HStagedEq' HFalse e e' | |
Eq e => HStagedEq' HTrue e e |
Ensure a list to contain HNats only
Static set property based on HEq
Find an element in a set based on HEq
Membership test
Another type-level membership test
Membership test based on type equality
Intersection based on HTMember
class HTIntersect l1 l2 l3 | l1 l2 -> l3 whereSource
hTIntersect :: l1 -> l2 -> l3Source
Like Data.List.intersect
HTIntersect HNil l HNil | |
(HTMember h l1 b, HTIntersectBool b h t l1 l2) => HTIntersect (HCons h t) l1 l2 |
class HBool b => HTIntersectBool b h t l1 l2 | b h t l1 -> l2 whereSource
hTIntersectBool :: b -> h -> t -> l1 -> l2Source
HTIntersect t l1 l2 => HTIntersectBool HFalse h t l1 l2 | |
HTIntersect t l1 l2 => HTIntersectBool HTrue h t l1 (HCons h l2) |
Turn a heterogeneous list into a homogeneous one
class HList2List l e whereSource
Same as hMapOut Id
hList2List :: l -> [e]Source
HList2List HNil e | |
HList2List l e => HList2List (HCons e l) e |