Safe Haskell	None

Data.HList.TIP

Contents

The newtype for type-indexed products
Type-indexed type sequences
Shielding type-indexed operations
Sample code

Description

The HList library

Type-indexed products.

Synopsis

The newtype for type-indexed products

newtype TIP l Source

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 lSource

emptyTIP :: TIP `[]`Source

Type-indexed type sequences

class HTypeIndexed l Source

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 lSource

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

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

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)Source

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))Source

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 --