Data.HList.TIP

The HList library

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

Type-indexed products.

The newtype for type-indexed products

newtype TIP l

Constructors

TIP

Fields

unTIP :: HList l

Instances

HOccursNot k [*] e l => HOccursNot k * e (TIP l)

(HOccurs e (TIP l1), SubType * * (TIP l1) (TIP l2)) => SubType * * (TIP l1) (TIP (: * e l2))

SubType * * (TIP l) (TIP ([] *))

Subtyping for TIPs

HOccurs e (HList (: * x (: * y l))) => HOccurs e (TIP (: * x (: * y l)))

~ * e' e => HOccurs e' (TIP (: * e ([] *)))

One occurrence and nothing is left

This variation provides an extra feature for singleton lists. That is, the result type is unified with the element in the list. Hence the explicit provision of a result type can be omitted.

(HOccursNot * [*] e l, HTypeIndexed l) => HExtend e (TIP l)

Show (HList l) => Show (TIP l)

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

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

emptyTIP :: TIP `[]`

Type-indexed type sequences

class HTypeIndexed l

Instances

HTypeIndexed ([] *)

(HOccursNot * [*] e l, HTypeIndexed l) => HTypeIndexed (: * e l)

Shielding type-indexed operations

The absence of signatures is deliberate! They all must be inferred.

onTIP :: HTypeIndexed l => (HList t -> HList l) -> TIP t -> TIP l

tipyDelete :: (HType2HNat k [*] e t n, HDeleteAtHNat n t, HTypeIndexed (HDeleteAtHNatR n t)) => Proxy k e -> TIP t -> TIP (HDeleteAtHNatR n t)

tipyUpdate :: (HType2HNat * [*] e t n, HUpdateAtHNat n e t, HTypeIndexed (HUpdateAtHNatR n e t)) => e -> TIP t -> TIP (HUpdateAtHNatR n e t)

tipyProject :: (Apply (FHUProj True ns) (HList t, Proxy HNat HZero), HTypes2HNats [*] [*] (HUnfoldR (FHUProj True ns) (ApplyR (FHUProj True ns) (HList t, Proxy HNat HZero))) t ns, HUnfold' (FHUProj True ns) (ApplyR (FHUProj True ns) (HList t, Proxy HNat HZero)), HTypeIndexed (HUnfoldR (FHUProj True ns) (ApplyR (FHUProj True ns) (HList t, Proxy HNat HZero)))) => Proxy [*] (HProjectByHNatsR ns t) -> TIP t -> TIP (HProjectByHNatsR ns t)

tipySplit :: (Apply (FHUProj True ns) (HList l, Proxy HNat HZero), Apply (FHUProj False ns) (HList l, Proxy HNat HZero), HTypes2HNats [*] [*] ps l ns, HUnfold' (FHUProj True ns) (ApplyR (FHUProj True ns) (HList l, Proxy HNat HZero)), HUnfold' (FHUProj False ns) (ApplyR (FHUProj False ns) (HList l, Proxy HNat HZero)), HTypeIndexed (HUnfoldR (FHUProj True ns) (ApplyR (FHUProj True ns) (HList l, Proxy HNat HZero))), HTypeIndexed (HUnfoldR (FHUProj False ns) (ApplyR (FHUProj False ns) (HList l, Proxy HNat HZero)))) => Proxy [*] ps -> TIP l -> (TIP (HProjectByHNatsR ns l), TIP (HProjectAwayByHNatsR ns l))

Split produces two TIPs

Sample code

Assume

>>> import Data.HList.FakePrelude

>>> :{
newtype Key    = Key Integer deriving (Show,Eq,Ord)
newtype Name   = Name String deriving (Show,Eq)
data Breed     = Cow | Sheep deriving (Show,Eq)
newtype Price  = Price Float deriving (Show,Eq,Ord)
data Disease   = BSE | FM deriving (Show,Eq)
type Animal =  '[Key,Name,Breed,Price]
:}

>>> :{
let myAnimal :: HList Animal
    myAnimal = hBuild (Key 42) (Name "Angus") Cow (Price 75.5)
    myTipyCow = TIP myAnimal
    animalKey :: (HOccurs Key l, SubType l (TIP Animal)) => l -> Key
    animalKey = hOccurs
:}

Session log

>>> :t myTipyCow
myTipyCow :: TIP Animal

>>> hOccurs myTipyCow :: Breed
Cow

>>> BSE .*. myTipyCow
TIPH[BSE, Key 42, Name "Angus", Cow, Price 75.5]

>>> Sheep .*. tipyDelete (proxy::Proxy Breed) myTipyCow
TIPH[Sheep, Key 42, Name "Angus", Price 75.5]

>>> tipyUpdate Sheep myTipyCow
TIPH[Key 42, Name "Angus", Sheep, Price 75.5]

Don't bother repeating the type error:

>>> let doctestEq x y = x == y || "No instance for" `Data.List.isInfixOf` x

>>> Sheep .*. myTipyCow
-- type error --