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
A variation on update.
Replace a proxy by a value of the proxied type. The signature is inferred
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.
Narrow two records to their least-upper bound
Extension of lubNarrow to a heterogeneous list
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...