The HList library
(C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
Extensible records -- operations that (may) require GHC
See Data.HList.Record for the base module.
- hUnproxyLabel :: (HUpdateAtHNat n (LVPair l a) t l', HFind l ls n, RecordLabels t ls, HasField l t (Proxy a)) => l -> a -> Record t -> Record l'
- hasNoProxies :: HasNoProxies r => Record r -> ()
- data ProxyFound x
- class HasNoProxies l
- class NarrowM a b res | a b -> res where
- class NarrowM' rin rout b res | rin rout b -> res where
- narrowM' :: rin -> rout -> b -> res
- class NarrowM'' f r r' | f r -> r' where
- narrowM'' :: f -> r -> r'
- class Narrow a b where
- class LubNarrow a b c | a b -> c where
- lubNarrow :: a -> b -> (c, c)
- data NilLub
- nilLub :: NilLub
- class ConsLub h t l | h t -> l where
- consLub :: h -> t -> l
- class HLub l e | l -> e where
- hLub :: l -> [e]
- class RecordEquiv r1 r2 res | r1 r2 -> res where
- class RecordEquiv' pj1 pj2 res | pj1 pj2 -> res where
- equivR' :: pj1 -> pj2 -> res
- hNilTcName :: TyCon
- hConsTcName :: TyCon
- recordTcName :: TyCon
- hFieldTcName :: TyCon
- proxyTcName :: TyCon
Documentation
hUnproxyLabel :: (HUpdateAtHNat n (LVPair l a) t l', HFind l ls n, RecordLabels t ls, HasField l t (Proxy a)) => l -> a -> Record t -> Record l'Source
A variation on update.
Replace a proxy by a value of the proxied type. The signature is inferred
hasNoProxies :: HasNoProxies r => Record r -> ()Source
Test for values; refuse proxies
data ProxyFound x Source
class HasNoProxies l Source
HasNoProxies HNil | |
HasNoProxies l => HasNoProxies (HCons e l) | |
Fail (ProxyFound x) => HasNoProxies (HCons (Proxy x) l) | |
Fail (ProxyFound x) => HasNoProxies (HCons (LVPair lab (Proxy x)) l) |
class NarrowM a b res | a b -> res whereSource
Narrow a record to a different record type
First is the monadic
version, which returns the `failure indictator'
(HNothing) if the narrowing fails because the source does not have
all the fields for the target.
class LubNarrow a b c | a b -> c whereSource
Narrow two records to their least-upper bound
(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) |
class RecordEquiv r1 r2 res | r1 r2 -> res whereSource
Record equivalence modulo field order
Decide if two records r1 and r2 are identical or differ only in the order of their fields.
If the two record types are indeed equivalent, return the witness of their equivalence, (HJust (r1->r2,r2->r1)). If they are not equivalent, return HNothing
The function equivR does not examine the values of its arguments: it needs only their types.
The algorithm is simple: two records are equivalent if one can be narrowed to the other, and vice versa. The narrowing coercions are the desired witnesses.
The obvious optimization is to check first if two records are of the same type. That requires TypeEq however. Perhaps we shouldn't use it here. Use of the record narrowing tacitly assumes that the label of a record field uniquely determines the type of the field value. Therefore, we should not use equivR on two records with inconsistent labeling...
(NarrowM r1 r2 r12, NarrowM r2 r1 r21, RecordEquiv' (Record r1 -> r12) (Record r2 -> r21) res) => RecordEquiv r1 r2 res |
class RecordEquiv' pj1 pj2 res | pj1 pj2 -> res whereSource
RecordEquiv' (r1 -> HNothing) pj2 HNothing | |
RecordEquiv' (r1 -> HJust r2) (r2 -> HNothing) HNothing | |
RecordEquiv' (r1 -> HJust r2) (r2 -> HJust r1) (HJust (r1 -> r2, r2 -> r1)) |