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
Instances
Instances
Conjunction
Disjunction
Conditional
Naturals
Instances
| Show HZero | |
| HNat2Integral HZero | |
| HNat HZero | |
| HLength HNil HZero | |
| HLt HZero HZero HFalse | |
| HEq HZero HZero HTrue | |
| HFind' HTrue e l HZero | |
| HOccursNot e l => HType2HNatCase HTrue e l HZero | |
| HUpdateAtHNat HZero e' (HCons e l) (HCons e' l) | |
| HNat n => HLt HZero (HSucc n) HTrue | |
| HNat n => HEq HZero (HSucc n) HFalse | |
| HDeleteAtHNat HZero (HCons e l) l | |
| HLookupByHNat HZero (HCons e l) e | |
| Show (HSucc HZero) | |
| HNat n => HLt (HSucc n) HZero HFalse | |
| HNat n => HEq (HSucc n) HZero HFalse | |
| HBetween (HSucc HZero) (HCons HZero HNil) |
Instances
| HFind e l n => HFind' HFalse e l (HSucc n) | |
| HType2HNat e l n => HType2HNatCase HFalse e l (HSucc n) | |
| HNat n => HLt HZero (HSucc n) HTrue | |
| HNat n => HEq HZero (HSucc n) HFalse | |
| (HNat n, Show (HSucc n)) => Show (HSucc (HSucc n)) | |
| Show (HSucc HZero) | |
| 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 | |
| HNat n => HLt (HSucc n) HZero HFalse | |
| HNat n => HEq (HSucc n) HZero HFalse | |
| (HUpdateAtHNat n e' l l', HNat n) => HUpdateAtHNat (HSucc n) e' (HCons e l) (HCons e l') | |
| (HNat n, HNat n', HLt n n' b) => HLt (HSucc n) (HSucc n') b | |
| (HNat n, HNat n', HEq n n' b) => HEq (HSucc n) (HSucc n') b | |
| HBetween (HSucc HZero) (HCons HZero HNil) | |
| (HLookupByHNat n l e', HNat n) => HLookupByHNat (HSucc n) (HCons e l) e' | |
| (HDeleteAtHNat n l l', HNat n) => HDeleteAtHNat (HSucc n) (HCons e l) (HCons e l') | |
| (HLength l n, HNat n, HList l) => HLength (HCons a l) (HSucc n) |
class HNat n => HNat2Integral n whereSource
Methods
hNat2Integral :: Integral i => n -> iSource
Instances
| HNat2Integral HZero | |
| HNat2Integral n => HNat2Integral (HSucc n) |
Maybies
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 |
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 -> bSource
Instances
| TypeEq x y b => HEq x y b | Equality on labels |
| HEq HZero HZero HTrue | |
| HEq HNil HNil HTrue | |
| HNat n => HEq HZero (HSucc n) HFalse | |
| HList l => HEq HNil (HCons e l) HFalse | |
| HNat n => HEq (HSucc n) HZero HFalse | |
| TypeEq x y b => HEq (Proxy x) (Proxy y) b | Equality on labels |
| (HNat n, HNat n', HEq n n' b) => HEq (HSucc n) (HSucc n') b | |
| HEq n n' b => HEq (Label n) (Label n') b | Equality on labels |
| HList l => HEq (HCons e l) HNil HFalse | |
| (HList l, HList l', HEq e e' b, HEq l l' b', HAnd b b' b'') => HEq (HCons e l) (HCons e' l') b'' | |
| HEq x x' b => HEq (Label x ns desc1) (Label x' ns desc2) b | Equality on labels (descriptions are ignored) |
| (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 whereSource
- Establish type equality statically
- Establish remaining value-level equality dynamically
class HBool b => TypeEq x y b | x y -> bSource
A predicate for type equality
There are different implementations.
See imports in Main*.hs
Type-safe cast
A phantom type for type proxies
Instances
| Show (Proxy e) | |
| Typeable x => Typeable (Proxy x) | |
| Typeable x => ShowLabel (Proxy x) | Show label |
| 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 Source
Instances
| TypeEqTrue x x |
class TypeEqFalse x y Source
Instances
| TypeEqFalse x y | |
| Fail () => TypeEqFalse x x |
typeEqTrue :: TypeEqTrue x y => x -> y -> ()Source
typeEqFalse :: TypeEqFalse x y => x -> y -> ()Source
Subtyping
Instances
| (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. |
| (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') |