Safe Haskell | None |
---|
Data.HList.TIP
Contents
Description
The HList library
(C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
Type-indexed products.
- newtype TIP l = TIP l
- mkTIP :: HTypeIndexed l => l -> TIP l
- unTIP :: TIP l -> l
- emptyTIP :: TIP HNil
- class HList l => HTypeIndexed l
- hExtend' :: (HOccursNot e l, HTypeIndexed l) => e -> TIP l -> TIP (HCons e l)
- onTIP :: HTypeIndexed l => (t -> l) -> TIP t -> TIP l
- tipyDelete :: (HDeleteAtHNat n t l, HType2HNat e t n, HTypeIndexed l) => Proxy e -> TIP t -> TIP l
- tipyUpdate :: (HUpdateAtHNat n e t l, HType2HNat e t n, HTypeIndexed l) => e -> TIP t -> TIP l
- tipyProject :: (HProjectByHNats ns t l, HTypes2HNats ps t ns, HTypeIndexed l) => ps -> TIP t -> TIP l
- tipySplit :: (HMap (HAddTag HTrue) t l', HSplitByHNats' ns l' l l1, HTypes2HNats ps t ns, HTypeIndexed l, HTypeIndexed l1) => ps -> TIP t -> (TIP l, TIP l1)
- tuple :: (HOccurs e1 (TIP l), HType2HNat e1 l n, HDeleteAtHNat n l l', HOccurs e2 (TIP l'), HOccurs e2 (TIP l), HType2HNat e2 l n', HDeleteAtHNat n' l l'', HOccurs e1 (TIP l'')) => TIP l -> (e1, e2)
- oneTrue :: TIP (HCons Int (HCons Bool HNil))
Documentation
newtype TIP l
The newtype for type-indexed products
Constructors
TIP l |
Instances
HOccursNot e l => HOccursNot e (TIP l) | |
HOccursOpt e l => HOccursOpt e (TIP l) | |
HOccurs e (HCons x (HCons y l)) => HOccurs e (TIP (HCons x (HCons y l))) | |
TypeCast e' e => HOccurs e (TIP (HCons e' HNil)) | |
HOccursFst e l => HOccursFst e (TIP l) | |
HOccursMany1 e l => HOccursMany1 e (TIP l) | |
HOccursMany e l => HOccursMany e (TIP l) | |
(HOccursNot e l, HTypeIndexed l) => HExtend e (TIP l) (TIP (HCons e l)) | |
Read l => Read (TIP l) | |
Show l => Show (TIP l) | |
(HOccurs e l, SubType (TIP l) (TIP l')) => SubType (TIP l) (TIP (HCons e l')) | |
SubType (TIP l) (TIP HNil) | |
(HAppend l l' l'', HTypeIndexed l'') => HAppend (TIP l) (TIP l') (TIP l'') |
mkTIP :: HTypeIndexed l => l -> TIP l
class HList l => HTypeIndexed l
Type-indexed type sequences
Instances
HTypeIndexed HNil | |
(HList (HCons e l), HOccursNot e l, HTypeIndexed l) => HTypeIndexed (HCons e l) |
hExtend' :: (HOccursNot e l, HTypeIndexed l) => e -> TIP l -> TIP (HCons e l)
Type-indexed extension
signature is inferred
hExtend' :: (HTypeIndexed t, HOccursNot e t) => e -> TIP t -> TIP (HCons e t)
Valid type I
hExtend' :: (HTypeIndexed l, HOccursNot e l) => e -> TIP l -> TIP (HCons e l)
Valid type II
- TIP> :t hExtend' hExtend' :: forall l e. (HTypeIndexed (HCons e l)) => e -> TIP l -> TIP (HCons e l)
onTIP :: HTypeIndexed l => (t -> l) -> TIP t -> TIP l
Shielding type-indexed operations The absence of signatures is deliberate! They all must be inferred.
tipyDelete :: (HDeleteAtHNat n t l, HType2HNat e t n, HTypeIndexed l) => Proxy e -> TIP t -> TIP l
tipyUpdate :: (HUpdateAtHNat n e t l, HType2HNat e t n, HTypeIndexed l) => e -> TIP t -> TIP l
tipyProject :: (HProjectByHNats ns t l, HTypes2HNats ps t ns, HTypeIndexed l) => ps -> TIP t -> TIP l
tipySplit :: (HMap (HAddTag HTrue) t l', HSplitByHNats' ns l' l l1, HTypes2HNats ps t ns, HTypeIndexed l, HTypeIndexed l1) => ps -> TIP t -> (TIP l, TIP l1)
Sample code
Assume
myTipyCow = TIP myAnimal
animalKey :: (HOccurs Key l, SubType l (TIP Animal)) => l -> Key animalKey = hOccurs
Session log
*TIP> :t myTipyCow myTipyCow :: TIP Animal
*TIP> hOccurs myTipyCow :: Breed Cow
*TIP> hExtend BSE myTipyCow TIP (HCons BSE (HCons (Key 42) (HCons (Name "Angus") (HCons Cow (HCons (Price 75.5) HNil)))))
*TIP> BSE .*. myTipyCow --- same as before ---
*TIP> Sheep .*. myTipyCow Type error ...
*TIP> Sheep .*. tipyDelete myTipyCow (HProxy::HProxy Breed) TIP (HCons Sheep (HCons (Key 42) (HCons (Name "Angus") (HCons (Price 75.5) HNil))))
*TIP> tipyUpdate myTipyCow Sheep TIP (HCons (Key 42) (HCons (Name "Angus") (HCons Sheep (HCons (Price 75.5) HNil))))
Sample 2
tuple :: (HOccurs e1 (TIP l), HType2HNat e1 l n, HDeleteAtHNat n l l', HOccurs e2 (TIP l'), HOccurs e2 (TIP l), HType2HNat e2 l n', HDeleteAtHNat n' l l'', HOccurs e1 (TIP l'')) => TIP l -> (e1, e2)
This example from the TIR paper challenges singleton lists. Thanks to the HW 2004 reviewer who pointed out the value of this example. We note that the explicit type below is richer than the inferred type. This richer type is needed for making this operation more polymorphic. That is, a) would not work without the explicit type, while it would:
a) ((+) (1::Int)) $ snd $ tuple oneTrue b) ((+) (1::Int)) $ fst $ tuple oneTrue