The HList library
(C) 2004-2006, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
Extensible records
The are different models of labels that go with this module; see:
- newtype LVPair l v = LVPair {
- valueLVPair :: v
- labelLVPair :: LVPair l v -> l
- newLVPair :: l -> v -> LVPair l v
- newtype Record r = Record r
- mkRecord :: HRLabelSet r => r -> Record r
- emptyRecord :: Record HNil
- class RecordLabels r ls | r -> ls
- recordLabels :: RecordLabels r ls => Record r -> ls
- recordLabels' :: RecordLabels r ls => r -> ls
- class RecordValues r ls | r -> ls where
- recordValues' :: r -> ls
- recordValues :: RecordValues r vs => Record r -> vs
- class ShowComponents l where
- showComponents :: String -> l -> String
- class ShowLabel l where
- class HasField l r v | l r -> v where
- hLookupByLabel :: l -> r -> v
- class HasField' b l r v | b l r -> v where
- hLookupByLabel' :: b -> l -> r -> v
- hDeleteAtLabel :: H2ProjectByLabels (HCons e HNil) t t1 t2 => e -> Record t -> Record t2
- hUpdateAtLabel :: (HUpdateAtHNat n (LVPair l v) t l', HFind l ls n, RecordLabels t ls) => l -> v -> Record t -> Record l'
- hTPupdateAtLabel :: (HasField l t a, HUpdateAtHNat n (LVPair l a) t l', HFind l ls n, RecordLabels t ls) => l -> a -> Record t -> Record l'
- hRenameLabel :: (HRLabelSet (HCons (LVPair l v) t2), HasField e t1 v, H2ProjectByLabels (HCons e HNil) t1 t t2) => e -> l -> Record t1 -> Record (HCons (LVPair l v) t2)
- hProjectByLabels :: (HRLabelSet a, H2ProjectByLabels ls t a b) => ls -> Record t -> Record a
- hProjectByLabels2 :: (H2ProjectByLabels ls t t1 t2, HRLabelSet t1, HRLabelSet t2) => ls -> Record t -> (Record t1, Record t2)
- class HLeftUnion r r' r'' | r r' -> r'' where
- hLeftUnion :: r -> r' -> r''
- class HLeftUnionBool b r f r' | b r f -> r' where
- hLeftUnionBool :: b -> r -> f -> r'
- class UnionSymRec r1 r2 ru | r1 r2 -> ru where
- unionSR :: r1 -> r2 -> (ru, ru)
- hRearrange :: (HLabelSet ls, HRearrange ls r r') => ls -> Record r -> Record r'
- data DuplicatedLabel l = DuplicatedLabel l
- data ExtraField l = ExtraField
- data FieldNotFound l = FieldNotFound
- class H2ProjectByLabels ls r rin rout | ls r -> rin rout where
- h2projectByLabels :: ls -> r -> (rin, rout)
- class H2ProjectByLabels' b ls r rin rout | b ls r -> rin rout where
- h2projectByLabels' :: b -> ls -> r -> (rin, rout)
- class HLabelSet ls
- class HLabelSet' x ls xmem
- class HRLabelSet ps
- class HRLabelSet' l1 v1 l2 v2 leq r
- class HRearrange ls r r' | ls r -> r' where
- hRearrange2 :: ls -> r -> r'
- class HRearrange' l ls rin rout r' | l ls rin rout -> r' where
- hRearrange2' :: l -> ls -> rin -> rout -> r'
- class UnionSymRec' b r1 f2 r2' ru | b r1 f2 r2' -> ru where
- unionSR' :: b -> r1 -> f2 -> r2' -> (ru, ru)
Records
Labels
Record types as label-value pairs, where label is purely phantom. Thus the run-time representation of a field is the same as that of its value, and the record, at run-time, is indistinguishable from the HList of field values. At run-time, all information about the labels is erased.
Field of label l with value type v
LVPair | |
|
HasField' HTrue l (HCons (LVPair l v) r) v | |
(UnionSymRec r1 r2' (Record ru), HasField l2 ru v2, HUpdateAtHNat n (LVPair l2 v2) ru ru, RecordLabels ru ls, HFind l2 ls n) => UnionSymRec' HTrue r1 (LVPair l2 v2) r2' (Record ru) | Field f2 is already in r1, so it will be in the union of r1 with the rest of r2. To inject (HCons f2 r2) in that union, we should replace the field f2 |
HRearrange ls rout r' => HRearrange' l ls (HCons (LVPair l v) HNil) rout (HCons (LVPair l v) r') | |
(Narrow rout r', H2ProjectByLabels (HCons l HNil) r (HCons (LVPair l v) HNil) rout) => Narrow r (HCons (LVPair l v) r') | |
(HEq l l' b, HasField' b l (HCons (LVPair l' v') r) v) => HasField l (HCons (LVPair l' v') r) v | |
(H2ProjectByLabels (HCons l HNil) a rin rout, NarrowM' rin rout b res) => NarrowM a (HCons (LVPair l v) b) res | |
Fail (ExtraField l) => HRearrange HNil (HCons (LVPair l v) a) (ExtraField l) | For improved error messages |
(RecordLabels r1 ls, HMember l ls b, UnionSymRec' b (Record r1) (LVPair l v) (Record r2') ru) => UnionSymRec (Record r1) (Record (HCons (LVPair l v) r2')) ru | |
(RecordLabels r ls, HMember l ls b, HLeftUnionBool b r (LVPair l v) r''', HLeftUnion (Record r''') (Record r') r'') => HLeftUnion (Record r) (Record (HCons (LVPair l v) r')) r'' | |
Eq v => Eq (LVPair l v) | |
(Typeable x, Typeable y) => Typeable (LVPair x y) | |
(ShowLabel l, Show v, ShowComponents r) => ShowComponents (HCons (LVPair l v) r) | |
(HEq l1 l2 leq, HRLabelSet' l1 v1 l2 v2 leq r) => HRLabelSet (HCons (LVPair l1 v1) (HCons (LVPair l2 v2) r)) | |
Fail (ProxyFound x) => HasNoProxies (HCons (LVPair lab (Proxy x)) l) | |
HRLabelSet (HCons (LVPair l v) r) => HExtend (LVPair l v) (Record r) (Record (HCons (LVPair l v) r)) | |
RecordValues r' vs => RecordValues (HCons (LVPair l v) r') (HCons v vs) | |
RecordLabels r' ls => RecordLabels (HCons (LVPair l v) r') (HCons l ls) | |
HMaybied r r' => HMaybied (HCons (LVPair l (Proxy v)) r) (HCons (LVPair l (Maybe v)) r') | |
(HMemberM l' (HCons l ls) b, H2ProjectByLabels' b (HCons l ls) (HCons (LVPair l' v') r') rin rout) => H2ProjectByLabels (HCons l ls) (HCons (LVPair l' v') r') rin rout | |
(HLabelSet (HCons l ls), HSameLength ls vs) => HExtend (LVPair l v) (RecordP ls vs) (RecordP (HCons l ls) (HCons v vs)) | |
(RecordR2P r ls vs, HRLabelSet (HCons (LVPair l v) r), HLabelSet (HCons l ls), HSameLength ls vs) => RecordR2P (HCons (LVPair l v) r) (HCons l ls) (HCons v vs) |
labelLVPair :: LVPair l v -> lSource
Label accessor
Record
Record r |
(UnionSymRec r1 r2' (Record ru), HExtend f2 (Record ru) (Record (HCons f2 ru))) => UnionSymRec' HFalse r1 f2 r2' (Record (HCons f2 ru)) | |
NarrowM a HNil (HJust (Record HNil)) | |
(UnionSymRec r1 r2' (Record ru), HasField l2 ru v2, HUpdateAtHNat n (LVPair l2 v2) ru ru, RecordLabels ru ls, HFind l2 ls n) => UnionSymRec' HTrue r1 (LVPair l2 v2) r2' (Record ru) | Field f2 is already in r1, so it will be in the union of r1 with the rest of r2. To inject (HCons f2 r2) in that union, we should replace the field f2 |
UnionSymRec r1 (Record HNil) r1 | |
HLeftUnion r (Record HNil) r | |
HasField l r v => HasField l (Record r) v | |
NarrowM'' f (HJust (Record r)) (HJust (Record (HCons f r))) | |
Eq r => Eq (Record r) | |
ShowComponents r => Show (Record r) | |
Typeable x => Typeable (Record x) | |
(RecordLabels r' ls, H2ProjectByLabels ls r r' rout) => SubType (Record r) (Record r') | Subtyping for records |
(RecordLabels r1 ls, HMember l ls b, UnionSymRec' b (Record r1) (LVPair l v) (Record r2') ru) => UnionSymRec (Record r1) (Record (HCons (LVPair l v) r2')) ru | |
(RecordLabels r ls, HMember l ls b, HLeftUnionBool b r (LVPair l v) r''', HLeftUnion (Record r''') (Record r') r'') => HLeftUnion (Record r) (Record (HCons (LVPair l v) r')) r'' | |
(HRLabelSet r'', HAppend r r' r'') => HAppend (Record r) (Record r') (Record r'') | |
(RecordLabels a la, RecordLabels b lb, HTIntersect la lb lc, H2ProjectByLabels lc a c aout, H2ProjectByLabels lc b c bout, HRLabelSet c) => LubNarrow (Record a) (Record b) (Record c) | |
HRLabelSet (HCons (LVPair l v) r) => HExtend (LVPair l v) (Record r) (Record (HCons (LVPair l v) r)) |
mkRecord :: HRLabelSet r => r -> Record rSource
Build a record
emptyRecord :: Record HNilSource
Build an empty record
Getting Labels
class RecordLabels r ls | r -> lsSource
Construct the (phantom) list of labels of the record.
This is a purely type-level function.
RecordLabels HNil HNil | |
RecordLabels r' ls => RecordLabels (HCons (LVPair l v) r') (HCons l ls) |
recordLabels :: RecordLabels r ls => Record r -> lsSource
recordLabels' :: RecordLabels r ls => r -> lsSource
Getting Values
class RecordValues r ls | r -> ls whereSource
Construct the list of values of the record.
recordValues' :: r -> lsSource
RecordValues HNil HNil | |
RecordValues r' vs => RecordValues (HCons (LVPair l v) r') (HCons v vs) |
recordValues :: RecordValues r vs => Record r -> vsSource
Operations
Show
A corresponding Show
instance exists as
show x = "Record {" ++ showComponents "" x ++ "}"
class ShowComponents l whereSource
showComponents :: String -> l -> StringSource
ShowComponents HNil | |
(ShowLabel l, Show v, ShowComponents r) => ShowComponents (HCons (LVPair l v) r) |
Lookup
class HasField l r v | l r -> v whereSource
This is a baseline implementation. We use a helper class, HasField, to abstract from the implementation.
Because hLookupByLabel
is so frequent and important, we implement
it separately, more efficiently. The algorithm is familiar assq, only
the comparison operation is done at compile-time
hLookupByLabel :: l -> r -> vSource
class HasField' b l r v | b l r -> v whereSource
hLookupByLabel' :: b -> l -> r -> vSource
Delete
hDeleteAtLabel
label record
hDeleteAtLabel :: H2ProjectByLabels (HCons e HNil) t t1 t2 => e -> Record t -> Record t2Source
Update
hUpdateAtLabel
label value record
hUpdateAtLabel :: (HUpdateAtHNat n (LVPair l v) t l', HFind l ls n, RecordLabels t ls) => l -> v -> Record t -> Record l'Source
hTPupdateAtLabel :: (HasField l t a, HUpdateAtHNat n (LVPair l a) t l', HFind l ls n, RecordLabels t ls) => l -> a -> Record t -> Record l'Source
A variation on hUpdateAtLabel
: type-preserving update.
We could also say:
hTPupdateAtLabel l v r = hUpdateAtLabel l v r `asTypeOf` r
Then we were taking a dependency on Haskell's type equivalence. This would also constrain the actual implementation of hUpdateAtLabel.
Rename Label
hRenameLabel :: (HRLabelSet (HCons (LVPair l v) t2), HasField e t1 v, H2ProjectByLabels (HCons e HNil) t1 t t2) => e -> l -> Record t1 -> Record (HCons (LVPair l v) t2)Source
Rename the label of record
Projection
It is also an important operation: the basis of many deconstructors -- so we try to implement it efficiently.
hProjectByLabels :: (HRLabelSet a, H2ProjectByLabels ls t a b) => ls -> Record t -> Record aSource
hProjectByLabels ls r
returns r
with only the labels in ls
remaining
hProjectByLabels2 :: (H2ProjectByLabels ls t t1 t2, HRLabelSet t1, HRLabelSet t2) => ls -> Record t -> (Record t1, Record t2)Source
Unions
Left
class HLeftUnion r r' r'' | r r' -> r'' whereSource
hLeftUnion :: r -> r' -> r''Source
HLeftUnion r (Record HNil) r | |
(RecordLabels r ls, HMember l ls b, HLeftUnionBool b r (LVPair l v) r''', HLeftUnion (Record r''') (Record r') r'') => HLeftUnion (Record r) (Record (HCons (LVPair l v) r')) r'' |
class HLeftUnionBool b r f r' | b r f -> r' whereSource
hLeftUnionBool :: b -> r -> f -> r'Source
HLeftUnionBool HTrue r f r | |
HLeftUnionBool HFalse r f (HCons f r) |
Symmetric
Compute the symmetric union of two records r1 and r2 and return the pair of records injected into the union (ru1, ru2).
To be more precise, we compute the symmetric union type ru
of two record types r1
and r2
. The emphasis on types is important.
The two records (ru1,ru2) in the result of unionSR
have the same
type ru, but they are generally different values.
Here the simple example: suppose
r1 = (Label .=. True) .*. emptyRecord r2 = (Label .=. False) .*. emptyRecord
Then unionSR
r1 r2 will return (r1,r2). Both components of the result
are different records of the same type.
To project from the union ru, use hProjectByLabels
.
It is possible to project from the union obtaining a record
that was not used at all when creating the union.
We do assure however that if unionSR r1 r2
gave (r1u,r2u)
,
then projecting r1u onto the type of r1 gives the value identical
to r1. Ditto for r2.
class UnionSymRec r1 r2 ru | r1 r2 -> ru whereSource
UnionSymRec r1 (Record HNil) r1 | |
(RecordLabels r1 ls, HMember l ls b, UnionSymRec' b (Record r1) (LVPair l v) (Record r2') ru) => UnionSymRec (Record r1) (Record (HCons (LVPair l v) r2')) ru |
Reorder Labels
hRearrange :: (HLabelSet ls, HRearrange ls r r') => ls -> Record r -> Record r'Source
Rearranges a record by labels. Returns the record r, rearranged such that the labels are in the order given by ls. (recordLabels r) must be a permutation of ls.
Extension
Unclassified
Probably internals, that may not be useful
data DuplicatedLabel l Source
data ExtraField l Source
Fail (ExtraField l) => HRearrange HNil (HCons (LVPair l v) a) (ExtraField l) | For improved error messages |
data FieldNotFound l Source
Fail (FieldNotFound l) => HRearrange' l ls HNil rout (FieldNotFound l) | For improved error messages |
class H2ProjectByLabels ls r rin rout | ls r -> rin rout whereSource
Invariant:
r === rin `disjoint-union` rout labels rin === ls where (rin,rout) = hProjectByLabels ls r
h2projectByLabels :: ls -> r -> (rin, rout)Source
H2ProjectByLabels HNil r HNil r | |
(HMember l' ls b, H2ProjectByLabels' b ls (RecordP (HCons l' ls') vs') rin rout) => H2ProjectByLabels ls (RecordP (HCons l' ls') vs') rin rout | |
H2ProjectByLabels (HCons l ls) HNil HNil HNil | |
(HMemberM l' (HCons l ls) b, H2ProjectByLabels' b (HCons l ls) (HCons (LVPair l' v') r') rin rout) => H2ProjectByLabels (HCons l ls) (HCons (LVPair l' v') r') rin rout | |
H2ProjectByLabels (HCons l ls) (RecordP HNil HNil) (RecordP HNil HNil) (RecordP HNil HNil) |
class H2ProjectByLabels' b ls r rin rout | b ls r -> rin rout whereSource
h2projectByLabels' :: b -> ls -> r -> (rin, rout)Source
H2ProjectByLabels ls r' rin rout => H2ProjectByLabels' HNothing ls (HCons f' r') rin (HCons f' rout) | |
H2ProjectByLabels ls (RecordP ls' vs') rin (RecordP lo vo) => H2ProjectByLabels' HFalse ls (RecordP (HCons l' ls') (HCons v' vs')) rin (RecordP (HCons l' lo) (HCons v' vo)) | |
H2ProjectByLabels ls (RecordP ls' vs') (RecordP lin vin) rout => H2ProjectByLabels' HTrue ls (RecordP (HCons l' ls') (HCons v' vs')) (RecordP (HCons l' lin) (HCons v' vin)) rout | |
H2ProjectByLabels ls' r' rin rout => H2ProjectByLabels' (HJust ls') ls (HCons f' r') (HCons f' rin) rout |
class HLabelSet' x ls xmem Source
Fail (DuplicatedLabel x) => HLabelSet' x ls HTrue | |
HLabelSet ls => HLabelSet' x ls HFalse |
class HRLabelSet ps Source
Propery of a proper label set for a record: no duplication of labels
HRLabelSet HNil | |
HRLabelSet (HCons x HNil) | |
(HEq l1 l2 leq, HRLabelSet' l1 v1 l2 v2 leq r) => HRLabelSet (HCons (LVPair l1 v1) (HCons (LVPair l2 v2) r)) |
class HRLabelSet' l1 v1 l2 v2 leq r Source
Fail (DuplicatedLabel l1) => HRLabelSet' l1 v1 l2 v2 HTrue r | |
(HRLabelSet (HCons (LVPair l2 v2) r), HRLabelSet (HCons (LVPair l1 v1) r)) => HRLabelSet' l1 v1 l2 v2 HFalse r |
class HRearrange ls r r' | ls r -> r' whereSource
Helper class for hRearrange
hRearrange2 :: ls -> r -> r'Source
HRearrange HNil HNil HNil | |
Fail (ExtraField l) => HRearrange HNil (HCons (LVPair l v) a) (ExtraField l) | For improved error messages |
(H2ProjectByLabels (HCons l HNil) r rin rout, HRearrange' l ls rin rout r') => HRearrange (HCons l ls) r r' |
class HRearrange' l ls rin rout r' | l ls rin rout -> r' whereSource
Helper class 2 for hRearrange
hRearrange2' :: l -> ls -> rin -> rout -> r'Source
Fail (FieldNotFound l) => HRearrange' l ls HNil rout (FieldNotFound l) | For improved error messages |
HRearrange ls rout r' => HRearrange' l ls (HCons (LVPair l v) HNil) rout (HCons (LVPair l v) r') |
class UnionSymRec' b r1 f2 r2' ru | b r1 f2 r2' -> ru whereSource
(UnionSymRec r1 r2' (Record ru), HExtend f2 (Record ru) (Record (HCons f2 ru))) => UnionSymRec' HFalse r1 f2 r2' (Record (HCons f2 ru)) | |
(UnionSymRec r1 r2' (Record ru), HasField l2 ru v2, HUpdateAtHNat n (LVPair l2 v2) ru ru, RecordLabels ru ls, HFind l2 ls n) => UnionSymRec' HTrue r1 (LVPair l2 v2) r2' (Record ru) | Field f2 is already in r1, so it will be in the union of r1 with the rest of r2. To inject (HCons f2 r2) in that union, we should replace the field f2 |