Data.HList.TIP

The HList library

(C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke

Type-indexed products.

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)

Shielding type-indexed operations The absence of signatures is deliberate! They all must be inferred.

(HAppend l l' l'', HTypeIndexed l'') => HAppend (TIP l) (TIP l') (TIP l'')

mkTIP :: HTypeIndexed l => l -> TIP l

unTIP :: TIP l -> l

emptyTIP :: TIP HNil

class HList l => HTypeIndexed l

Type-indexed type sequences

Instances

HTypeIndexed HNil

(HOccursNot e l, HTypeIndexed l) => HTypeIndexed (HCons e l)

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)

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

oneTrue :: TIP (HCons Int (HCons Bool HNil))

A specific tuple