Safe Haskell | None |
---|
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.
- data HTrue
- hTrue :: HTrue
- data HFalse
- hFalse :: HFalse
- class HBool x
- class (HBool t, HBool t', HBool t'') => HAnd t t' t'' | t t' -> t'' where
- hAnd :: t -> t' -> t''
- class (HBool t, HBool t', HBool t'') => HOr t t' t'' | t t' -> t'' where
- hOr :: t -> t' -> t''
- class HBool t => HCond t x y z | t x y -> z where
- hCond :: t -> x -> y -> z
- data HZero
- data HSucc n
- hZero :: HZero
- hSucc :: HNat n => n -> HSucc n
- hPred :: HNat n => HSucc n -> n
- class HNat n
- class HNat n => HNat2Integral n where
- hNat2Integral :: Integral i => n -> i
- data HNothing = HNothing
- data HJust x = HJust x
- class HBool b => HEq x y b | x y -> b
- hEq :: HEq x y b => x -> y -> b
- class HStagedEq x y where
- class HBool b => HLt x y b | x y -> b
- hLt :: HLt x y b => x -> y -> b
- class HBool b => TypeEq x y b | x y -> b
- typeEq :: TypeEq t t' b => t -> t' -> b
- proxyEq :: TypeEq t t' b => Proxy t -> Proxy t' -> b
- class TypeCast x y | x -> y, y -> x where
- typeCast :: x -> y
- data Proxy e
- proxy :: Proxy e
- toProxy :: e -> Proxy e
- unProxy :: Proxy e -> e
- class TypeEqTrue x y
- class TypeEqFalse x y
- typeEqTrue :: TypeEqTrue x y => x -> y -> ()
- typeEqFalse :: TypeEqFalse x y => x -> y -> ()
- class SubType l l'
- subType :: SubType l l' => l -> l' -> ()
- class Fail x
Booleans
data HTrue
Instances
data HFalse
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
Naturals
data HZero
Instances
Show HZero | |
HNat2Integral HZero | |
HNat HZero | |
HLength HNil HZero | |
HLt HZero HZero HFalse | |
HEq HZero HZero HTrue | |
HNat HZero => HFind' HTrue e l HZero | |
(HBool HTrue, HNat HZero, HOccursNot e l) => HType2HNatCase HTrue e l HZero | |
HNat HZero => HUpdateAtHNat HZero e' (HCons e l) (HCons e' l) | |
(HBool HTrue, HNat n) => HLt HZero (HSucc n) HTrue | |
(HBool HFalse, HNat n) => HEq HZero (HSucc n) HFalse | |
HNat HZero => HDeleteAtHNat HZero (HCons e l) l | |
HNat HZero => HLookupByHNat HZero (HCons e l) e | |
Show (HSucc HZero) | |
(HBool HFalse, HNat n) => HLt (HSucc n) HZero HFalse | |
(HBool HFalse, HNat n) => HEq (HSucc n) HZero HFalse | |
HBetween (HSucc HZero) (HCons HZero HNil) |
data HSucc n
Instances
class HNat n => HNat2Integral n where
Methods
hNat2Integral :: Integral i => n -> i
Instances
HNat2Integral HZero | |
(HNat (HSucc n), HNat2Integral n) => HNat2Integral (HSucc n) |
Maybies
data HNothing
Constructors
HNothing |
Instances
Show HNothing | |
HMemberM e HNil HNothing | |
NarrowM'' f HNothing HNothing | |
HMemberM' HNothing e l HNothing | |
NarrowM' HNil rout b HNothing | |
H2ProjectByLabels ls r' rin rout => H2ProjectByLabels' HNothing ls (HCons f' r') rin (HCons f' rout) | |
FromHJust l l' => FromHJust (HCons HNothing l) l' | |
RecordEquiv' (r1 -> HNothing) pj2 HNothing | |
RecordEquiv' (r1 -> HJust r2) (r2 -> HNothing) HNothing |
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) |
Staged equality
class HStagedEq x y where
- Establish type equality statically
- Establish remaining value-level equality dynamically
class HBool b => TypeEq x y b | x y -> b
A predicate for type equality
There are different implementations.
See imports in Main*.hs
Type-safe cast
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') |
Type equality and disequality
class TypeEqTrue x y
Instances
TypeEqTrue x x |
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') |
Error messages
class Fail x
A class without instances for explicit failure