HList-0.2.3: Heterogeneous lists

Safe HaskellNone

Data.HList.FakePrelude

Contents

Description

The HList library

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

Some very basic technology for faking dependent types in Haskell.

Synopsis

Booleans

data HTrue

Instances

Show HTrue 
HBool HTrue 
TupleType () HTrue 
HBool HTrue => TypeEq x x HTrue 
HEq HZero HZero HTrue 
HEq HNil HNil HTrue 
HOr HFalse HTrue HTrue 
HOr HTrue HFalse HTrue 
HOr HTrue HTrue HTrue 
HAnd HFalse HTrue HFalse 
HAnd HTrue HFalse HFalse 
HAnd HTrue HTrue HTrue 
Eq e => HStagedEq' HTrue e e 
Fail (DuplicatedLabel x) => HLabelSet' x ls HTrue 
HBool HTrue => HCond HTrue x y x 
HNat HZero => HFind' HTrue e l HZero 
(HBool HTrue, HNat HZero, HOccursNot e l) => HType2HNatCase HTrue e l HZero 
HLeftUnionBool HTrue r f r 
HDeleteMany e l l' => HDeleteManyCase HTrue e e l l' 
Fail (DuplicatedLabel l1) => HRLabelSet' l1 v1 l2 v2 HTrue r 
(HBool HTrue, HTIntersect t l1 l2) => HTIntersectBool HTrue h t l1 (HCons h l2) 
(HList l, HOccursNot e l) => HOccursBool HTrue e (HCons e l) 
HasField' HTrue l (HCons (LVPair l v) r) v 
HasFieldP' HTrue l (RecordP (HCons l ls) (HCons v vs)) v 
(UnionSymRec r1 r2' (Record ru), HasField l2 ru v2, HUpdateAtHNat n (LVPair l2 v2) ru ru, RecordLabels ru ls, HFind l2 ls n) => UnionSymRec' HTrue r1 (LVPair l2 v2) r2' (Record ru)

Field f2 is already in r1, so it will be in the union of r1 with the rest of r2.

To inject (HCons f2 r2) in that union, we should replace the field f2

HMemberM' HTrue e (HCons e l) (HJust l) 
H2ProjectByLabels ls (RecordP ls' vs') (RecordP lin vin) rout => H2ProjectByLabels' HTrue ls (RecordP (HCons l' ls') (HCons v' vs')) (RecordP (HCons l' lin) (HCons v' vin)) rout 
HProjectByLabelP' HTrue l (HCons l ls) (HCons v vs) ls v vs 
(HBool HTrue, HNat n) => HLt HZero (HSucc n) HTrue 
HBool HTrue => TupleType (x, y) HTrue 
HSplit l l' l'' => HSplit (HCons (e, HTrue) l) (HCons e l') l'' 
HBool HTrue => TupleType (x, y, z) HTrue 

data HFalse

Instances

Show HFalse 
HBool HFalse 
HLt HZero HZero HFalse 
HOr HFalse HFalse HFalse 
HOr HFalse HTrue HTrue 
HOr HTrue HFalse HTrue 
HAnd HFalse HFalse HFalse 
HAnd HFalse HTrue HFalse 
HAnd HTrue HFalse HFalse 
HBool HFalse => HTMember e HNil HFalse 
HBool HFalse => HMember e HNil HFalse 
HStagedEq' HFalse e e' 
HOrdMember e HNil HFalse 
HLabelSet ls => HLabelSet' x ls HFalse 
HBool HFalse => HCond HFalse x y y 
TypeEq'' () x y HFalse 
(HBool HFalse, HTIntersect t l1 l2) => HTIntersectBool HFalse h t l1 l2 
(HRLabelSet (HCons (LVPair l2 v2) r), HRLabelSet (HCons (LVPair l1 v1) r)) => HRLabelSet' l1 v1 l2 v2 HFalse r 
(UnionSymRec r1 r2' (Record ru), HExtend f2 (Record ru) (Record (HCons f2 ru))) => UnionSymRec' HFalse r1 f2 r2' (Record (HCons f2 ru)) 
HDeleteMany e l l' => HDeleteManyCase HFalse e e' l (HCons e' l') 
(HNat (HSucc n), HFind e l n) => HFind' HFalse e l (HSucc n) 
(HBool HFalse, HNat (HSucc n), HType2HNat e l n) => HType2HNatCase HFalse e l (HSucc n) 
HLeftUnionBool HFalse r f (HCons f r) 
(HOccurs' e l, HList l) => HOccursBool HFalse e (HCons e' l) 
(HMemberM e l r, HMemberM' r e (HCons e' l) res) => HMemberM' HFalse e (HCons e' l) res 
HasField l r v => HasField' HFalse l (HCons fld r) v 
HasField l (RecordP ls vs) v => HasFieldP' HFalse l (RecordP (HCons l' ls) (HCons v' vs)) v 
H2ProjectByLabels ls (RecordP ls' vs') rin (RecordP lo vo) => H2ProjectByLabels' HFalse ls (RecordP (HCons l' ls') (HCons v' vs')) rin (RecordP (HCons l' lo) (HCons v' vo)) 
HProjectByLabelP l ls vs lso' v vso' => HProjectByLabelP' HFalse l (HCons l' ls) (HCons v' vs) (HCons l' lso') v (HCons v' vso') 
(HBool HFalse, HNat n) => HEq HZero (HSucc n) HFalse 
(HBool HFalse, HList l) => HEq HNil (HCons e l) HFalse 
(HBool HFalse, HNat n) => HLt (HSucc n) HZero HFalse 
(HBool HFalse, HNat n) => HEq (HSucc n) HZero HFalse 
(HBool HFalse, HList l) => HEq (HCons e l) HNil HFalse 
HSplit l l' l'' => HSplit (HCons (e, HFalse) l) l' (HCons e l'') 

class HBool x

Instances

Conjunction

class (HBool t, HBool t', HBool t'') => HAnd t t' t'' | t t' -> t'' where

Methods

hAnd :: t -> t' -> t''

Disjunction

class (HBool t, HBool t', HBool t'') => HOr t t' t'' | t t' -> t'' where

Methods

hOr :: t -> t' -> t''

Conditional

class HBool t => HCond t x y z | t x y -> z where

Methods

hCond :: t -> x -> y -> z

Instances

HBool HFalse => HCond HFalse x y y 
HBool HTrue => HCond HTrue x y x 

Naturals

data HSucc n

Instances

(HNat (HSucc n), HFind e l n) => HFind' HFalse e l (HSucc n) 
(HBool HFalse, HNat (HSucc n), HType2HNat e l n) => HType2HNatCase HFalse e l (HSucc n) 
(HBool HTrue, HNat n) => HLt HZero (HSucc n) HTrue 
(HBool HFalse, HNat n) => HEq HZero (HSucc n) HFalse 
(HNat n, Show (HSucc n)) => Show (HSucc (HSucc n)) 
Show (HSucc HZero) 
(HNat (HSucc n), HNat2Integral n) => HNat2Integral (HSucc n) 
HNat n => HNat (HSucc n) 
(HNat x, HBetween (HSucc x) y, HAppend y (HCons (HSucc x) HNil) z, HList y) => HBetween (HSucc (HSucc x)) z 
(HBool HFalse, HNat n) => HLt (HSucc n) HZero HFalse 
(HBool HFalse, HNat n) => HEq (HSucc n) HZero HFalse 
(HNat (HSucc n), HUpdateAtHNat n e' l l', HNat n) => HUpdateAtHNat (HSucc n) e' (HCons e l) (HCons e l') 
(HBool b, HNat n, HNat n', HLt n n' b) => HLt (HSucc n) (HSucc n') b 
(HBool b, HNat n, HNat n', HEq n n' b) => HEq (HSucc n) (HSucc n') b 
HBetween (HSucc HZero) (HCons HZero HNil) 
(HNat (HSucc n), HLookupByHNat n l e', HNat n) => HLookupByHNat (HSucc n) (HCons e l) e' 
(HNat (HSucc n), HDeleteAtHNat n l l', HNat n) => HDeleteAtHNat (HSucc n) (HCons e l) (HCons e l') 
(HList (HCons a l), HNat (HSucc n), HLength l n, HNat n, HList l) => HLength (HCons a l) (HSucc n) 

hSucc :: HNat n => n -> HSucc n

hPred :: HNat n => HSucc n -> n

class HNat n

Instances

HNat HZero 
HNat n => HNat (HSucc n) 

class HNat n => HNat2Integral n where

Methods

hNat2Integral :: Integral i => n -> i

Maybies

data HJust x

Constructors

HJust x 

Instances

NarrowM a HNil (HJust (Record HNil)) 
HMemberM' HTrue e (HCons e l) (HJust l) 
NarrowM'' f (HJust (Record r)) (HJust (Record (HCons f r))) 
Show x => Show (HJust x) 
HMemberM' (HJust l') e (HCons e' l) (HJust (HCons e' l')) 
H2ProjectByLabels ls' r' rin rout => H2ProjectByLabels' (HJust ls') ls (HCons f' r') (HCons f' rin) rout 
FromHJust l l' => FromHJust (HCons (HJust e) l) (HCons e l') 
ToHJust l l' => ToHJust (HCons e l) (HCons (HJust e) l') 
RecordEquiv' (r1 -> HJust r2) (r2 -> HNothing) HNothing 
RecordEquiv' (r1 -> HJust r2) (r2 -> HJust r1) (HJust (r1 -> r2, r2 -> r1)) 

Equality for types

class HBool b => HEq x y b | x y -> b

Instances

(HBool b, TypeEq x y b) => HEq x y b

Equality on labels

HEq HZero HZero HTrue 
HEq HNil HNil HTrue 
(HBool HFalse, HNat n) => HEq HZero (HSucc n) HFalse 
(HBool HFalse, HList l) => HEq HNil (HCons e l) HFalse 
(HBool HFalse, HNat n) => HEq (HSucc n) HZero HFalse 
(HBool b, TypeEq x y b) => HEq (Proxy x) (Proxy y) b

Equality on labels

(HBool b, HNat n, HNat n', HEq n n' b) => HEq (HSucc n) (HSucc n') b 
(HBool b, HEq n n' b) => HEq (Label n) (Label n') b

Equality on labels

(HBool HFalse, HList l) => HEq (HCons e l) HNil HFalse 
(HBool b'', HList l, HList l', HEq e e' b, HEq l l' b', HAnd b b' b'') => HEq (HCons e l) (HCons e' l') b'' 
(HBool b, HEq x x' b) => HEq (Label x ns desc1) (Label x' ns desc2) b

Equality on labels (descriptions are ignored)

(HBool b'', HEq x x' b, TypeEq ns ns' b', HAnd b b' b'') => HEq (Label x ns desc) (Label x' ns' desc') b''

Equality on labels (descriptions are ignored)

hEq :: HEq x y b => x -> y -> b

Staged equality

class HStagedEq x y where

  • Establish type equality statically
  • Establish remaining value-level equality dynamically

Methods

hStagedEq :: x -> y -> Bool

Instances

HStagedEq HNil HNil 
HStagedEq HNil (HCons e l) 
HStagedEq (HCons e l) HNil 
(TypeEq e e' b, HStagedEq l l', HStagedEq' b e e') => HStagedEq (HCons e l) (HCons e' l') 

class HBool b => HLt x y b | x y -> b

Less than

Instances

HLt HZero HZero HFalse 
(HBool HTrue, HNat n) => HLt HZero (HSucc n) HTrue 
(HBool HFalse, HNat n) => HLt (HSucc n) HZero HFalse 
(HBool b, HNat n, HNat n', HLt n n' b) => HLt (HSucc n) (HSucc n') b 

hLt :: HLt x y b => x -> y -> b

class HBool b => TypeEq x y b | x y -> b

A predicate for type equality

There are different implementations.

See imports in Main*.hs

Instances

(HBool b, TypeCast HFalse b) => TypeEq x y b 
HBool HTrue => TypeEq x x HTrue 

typeEq :: TypeEq t t' b => t -> t' -> b

proxyEq :: TypeEq t t' b => Proxy t -> Proxy t' -> b

Type-safe cast

class TypeCast x y | x -> y, y -> x where

Methods

typeCast :: x -> y

Instances

TypeCast x x 

A phantom type for type proxies

data Proxy e

Instances

Show (Proxy e) 
Typeable x => Typeable (Proxy x) 
Typeable x => ShowLabel (Proxy x)

Show label

(HBool b, TypeEq x y b) => HEq (Proxy x) (Proxy y) b

Equality on labels

HTypeProxied l => HTypeProxied (HCons (Proxy e) l) 
Fail (ProxyFound x) => HasNoProxies (HCons (Proxy x) l) 
Fail (ProxyFound x) => HasNoProxies (HCons (LVPair lab (Proxy x)) l) 
(HType2HNat e l n, HTypes2HNats ps l ns) => HTypes2HNats (HCons (Proxy e) ps) l (HCons n ns) 
HMaybied r r' => HMaybied (HCons (LVPair l (Proxy v)) r) (HCons (LVPair l (Maybe v)) r') 

toProxy :: e -> Proxy e

unProxy :: Proxy e -> e

Type equality and disequality

class TypeEqTrue x y

Instances

class TypeEqFalse x y

Instances

TypeEqFalse x y 
Fail () => TypeEqFalse x x 

typeEqTrue :: TypeEqTrue x y => x -> y -> ()

typeEqFalse :: TypeEqFalse x y => x -> y -> ()

Subtyping

class SubType l l'

Instances

(HOccurs e l, SubType (TIP l) (TIP l')) => SubType (TIP l) (TIP (HCons e l')) 
SubType (TIP l) (TIP HNil) 
(RecordLabels r' ls, H2ProjectByLabels ls r r' rout) => SubType (Record r) (Record r')

Subtyping for records

H2ProjectByLabels ls' (RecordP ls vs) (RecordP ls' vs') rout => SubType (RecordP ls vs) (RecordP ls' vs') 

subType :: SubType l l' => l -> l' -> ()

Error messages

class Fail x

A class without instances for explicit failure