Data.HList.FakePrelude

The HList library

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

Some very basic technology for faking dependent types in Haskell.

A heterogeneous apply operator

class Apply f a where

simpler/weaker version where type information only propagates forward with this one. app defined below, is more complicated / verbose to define, but it offers better type inference. Most uses have been converted to app, so there is not much that can be done with Apply.

Associated Types

type ApplyR f a :: *

Methods

apply :: f -> a -> ApplyR f a

Instances

HLookupByHNat n l => Apply (FHLookupByHNat l) (Proxy HNat n)

Apply (FHUProj sel ns) (HList l, Proxy HNat (HSucc n)) => Apply (Proxy Bool False, FHUProj sel ns) (HList (: * e l), Proxy HNat n)

Apply (Proxy Bool True, FHUProj sel ns) (HList (: * e l), Proxy HNat n)

(~ * ch (Proxy Bool (HBoolEQ sel (KMember n ns))), Apply (ch, FHUProj sel ns) (HList (: * e l), Proxy HNat n)) => Apply (FHUProj sel ns) (HList (: * e l), Proxy HNat n)

Apply (FHUProj sel ns) (HList ([] *), n)

Polymorphic functions are not first-class in haskell. One solution is to write an instance of ApplyAB for a data type that takes the place of the original function. In other words,

 data Fn = Fn
 instance ApplyAB Fn a b where applyAB Fn a = actual_fn a

Normally you would have been able to pass around the definition actual_fn.

Type inference / Local functional dependencies

Note that class ApplyAB has three parameters and no functional dependencies. Instances should be written in the style:

 instance (int ~ Int, double ~ Double) => ApplyAB Fn int double
  where applyAB _ = fromIntegral

rather than the more natural

 instance ApplyAB Fn Int Double

The first instance allows types to be inferred as if we had class ApplyAB a b c | a -> b c, while the second instance only matches if ghc already knows that it needs ApplyAB Fn Int Double. Additional explanation can be found in local functional dependencies

class ApplyAB f a b where

No constraints on result and argument types

Methods

applyAB :: f -> a -> b

Instances

(~ * f1 (a -> b -> c), ~ * f2 (b -> a -> c)) => ApplyAB HFlip f1 f2

(~ * y y', ~ * fg (x -> y, y' -> z), ~ * r (x -> z)) => ApplyAB Comp fg r

(~ * String string, Show a) => ApplyAB HShow a string

(~ * String string, Read a) => ApplyAB HRead string a

(~ * io (IO ()), Show x) => ApplyAB HPrint x io

~ * hJustA (HJust a) => ApplyAB HFromJust hJustA a

(~ * x (e, HList l), ~ * y (HList (: * e l))) => ApplyAB FHCons x y

(HZip3 a b c, ~ * x (HList a, HList b), ~ * y (HList c)) => ApplyAB HZipF x y

(~ * (Tagged k l (Proxy * t)) a, ~ * b (Tagged k l (Maybe t))) => ApplyAB HMaybeF a b

~ * e' e => ApplyAB HRmTag (e, t) e'

~ * hJustA (HJust a) => ApplyAB (HJust t) a hJustA

HJust () is a placeholder for a function that applies the HJust constructor

(Monad m, ApplyAB f x fx, ~ * fx (m ()), ~ * pair (x, m ()), ApplyAB f x (m ())) => ApplyAB (HSeq f) pair fx

~ * et (e, t) => ApplyAB (HAddTag t) e et

(~ * l [e'], ApplyAB f e e', ~ * el (e, l)) => ApplyAB (Mapcar f) el l

(ApplyAB f (x, y) z, ~ * mz (m z), ~ * mxy (m x, m y), Applicative m) => ApplyAB (LiftA2 f) mxy mz

HMapCxt f as bs as' bs' => ApplyAB (HMap f) as bs

(Data b, ~ * x (t, c (b -> r)), ~ * y (c r)) => ApplyAB (GunfoldK c) x y

(Data d, ~ * (c (d -> b), d) x, ~ * (c b) y) => ApplyAB (GfoldlK c) x y

ApplyAB f e e' => ApplyAB (MapCar f) (e, HList l) (HList (: * e' l))

(~ * x' x, ~ * y' y) => ApplyAB (x' -> y') x y

note this function will only be available at a single type (that is, hMap succ will only work on HList that contain only one type)

(ApplyAB f a b, ApplyAB g b c) => ApplyAB (HComp g f) a c

(FunCxt k cxt b, ~ * (FunApp k1 geta b) a) => ApplyAB (Fun' k k1 cxt geta) a b

(FunCxt k cxt a, ~ * (FunApp k1 getb a) b) => ApplyAB (Fun k k1 cxt getb) a b

Fun can be used instead of writing a new instance of ApplyAB. Refer to the definition/source for the the most concise explanation. A more wordy explanation is given below:

A type signature needs to be provided on Fun to make it work. Depending on the kind of the parameters to Fun, a number of different results happen.

ex1

A list of kind [* -> Constraint] produces those constraints on the argument type:

>>> :set -XDataKinds
>>> let plus1 = Fun (\x -> if x < 5 then x+1 else 5) :: Fun '[Num, Ord] '()
>>> :t applyAB plus1
applyAB plus1 :: (Num a, Ord a) => a -> a

Also note the use of '() to signal that the result type is the same as the argument type.

A single constraint can also be supplied:

>>> let succ1 = Fun succ :: Fun Enum '()
>>> :t applyAB succ1
applyAB succ1 :: Enum a => a -> a

>>> let just = Fun Just :: Fun '[] Maybe
>>> :t applyAB just
applyAB just :: a -> Maybe a

data Fun cxt getb

Constructors

Fun (forall a. FunCxt cxt a => a -> FunApp getb a)

Instances

(FunCxt k cxt a, ~ * (FunApp k1 getb a) b) => ApplyAB (Fun k k1 cxt getb) a b

data Fun' cxt geta

see Fun. The only difference here is that the argument type is calculated from the result type.

>>> let rd = Fun' read :: Fun' Read String
>>> :t applyAB rd
applyAB rd :: Read b => [Char] -> b

>>> let fromJust' = Fun' (\(Just a) -> a) :: Fun' '[] Maybe
>>> :t applyAB fromJust'
applyAB fromJust' :: Maybe b -> b

Note this use of Fun' means we don't have to get the b out of Maybe b,

Constructors

Fun' (forall b. FunCxt cxt b => FunApp geta b -> b)

Instances

(FunCxt k cxt b, ~ * (FunApp k1 geta b) a) => ApplyAB (Fun' k k1 cxt geta) a b

type family FunApp fns a

type family FunCxt cxts a :: Constraint

Simple useful instances of Apply

data HPrint

print. An alternative implementation could be:

>>> let hPrint = Fun print :: Fun Show (IO ())

This produces:

>>> :t applyAB hPrint
applyAB hPrint :: Show a => a -> IO ()

Constructors

HPrint

Instances

(~ * io (IO ()), Show x) => ApplyAB HPrint x io

data HRead

read

>>> applyAB HRead "5.0" :: Double
5.0

Constructors

HRead

Instances

(~ * String string, Read a) => ApplyAB HRead string a

data HShow

show

Constructors

HShow

Instances

(~ * String string, Show a) => ApplyAB HShow a string

data HComp g f

Compose two instances of ApplyAB

>>> applyAB (HComp HRead HShow) (5::Double) :: Double
5.0

Constructors

HComp g f

g . f

Instances

(ApplyAB f a b, ApplyAB g b c) => ApplyAB (HComp g f) a c

data Comp

app Comp (f,g) = g . f. Works like:

>>> applyAB Comp (succ, pred) 'a'
'a'

>>> applyAB Comp (toEnum :: Int -> Char, fromEnum) 10
10

Note that defaulting will sometimes give you the wrong thing

 used to work (with associated types calculating result/argument types)
 >>> applyAB Comp (fromEnum, toEnum) 'a'
 *** Exception: Prelude.Enum.().toEnum: bad argument

Constructors

Comp

Instances

(~ * y y', ~ * fg (x -> y, y' -> z), ~ * r (x -> z)) => ApplyAB Comp fg r

newtype HSeq x

((a,b) -> f a >> b)

Constructors

HSeq x

Instances

(Monad m, ApplyAB f x fx, ~ * fx (m ()), ~ * pair (x, m ()), ApplyAB f x (m ())) => ApplyAB (HSeq f) pair fx

data HFlip

flip

Constructors

HFlip

Instances

(~ * f1 (a -> b -> c), ~ * f2 (b -> a -> c)) => ApplyAB HFlip f1 f2

Proxy

see Data.HList.Proxy

data Label l

A special Proxy for record labels, polykinded

Constructors

Label

Instances

~ k x x' => ToSym * k (Label k x) x'

for Data.HList.Label6 labels

IsKeyFN * (Label Symbol s -> a -> b) True

labels that impose no restriction on the type of the (single) argument which follows

>>> let testF (_ :: Label "a") (a :: Int) () = a+1
>>> kw (hBuild testF) (Label :: Label "a") 5 ()
6

Show desc => Show (Label * (Lbl k * x ns desc))

labelToProxy :: Label l -> Proxy l

class ShowLabel l where

Methods

showLabel :: Label l -> String

Instances

SingI Symbol x => ShowLabel Symbol x

Show desc => ShowLabel * (Lbl k * x ns desc)

Equality on labels (descriptions are ignored) Use generic instance

Show label

Booleans

GHC already lifts booleans, defined as

 data Bool = True | False

to types: Bool becomes kind and True and False (also denoted by 'True and 'False) become nullary type constructors.

The above line is equivalent to

 data HTrue
 data HFalse

 class HBool x
 instance HBool HTrue
 instance HBool HFalse

Value-level proxies

hTrue :: Proxy True

hFalse :: Proxy False

Conjunction

type family HAnd t1 t2 :: Bool

hAnd :: Proxy t1 -> Proxy t2 -> Proxy (HAnd t1 t2)

demote to values

Disjunction

type family HOr t1 t2 :: Bool

hOr :: Proxy t1 -> Proxy t2 -> Proxy (HOr t1 t2)

demote to values

Compare with the original code based on functional dependencies:

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

 instance HOr HFalse HFalse HFalse
  where
   hOr _ _ = hFalse

 instance HOr HTrue HFalse HTrue
  where
   hOr _ _ = hTrue

 instance HOr HFalse HTrue HTrue
  where
   hOr _ _ = hTrue

 instance HOr HTrue HTrue HTrue
  where
   hOr _ _ = hTrue

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

Methods

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

Instances

HCond False x y y

HCond True x y x

Boolean equivalence

type family HBoolEQ t1 t2 :: Bool

Naturals

data HNat

The data type to be lifted to the type level

Constructors

HZero

HSucc HNat

Instances

HEq HNat HZero HZero True

HEq HNat HZero (HSucc n) False

HEq HNat (HSucc n) HZero False

HEq HNat n n' b => HEq HNat (HSucc n) (HSucc n') b

HTypes2HNats [*] [*] ([] *) l ([] HNat)

And lift to the list of types

(HType2HNat k [*] e l n, HTypes2HNats [k] [*] es l ns) => HTypes2HNats [k] [*] (: k e es) l (: HNat n ns)

HLookupByHNat n l => Apply (FHLookupByHNat l) (Proxy HNat n)

HNat2Integral n => Show (Proxy HNat n)

Apply (FHUProj sel ns) (HList l, Proxy HNat (HSucc n)) => Apply (Proxy Bool False, FHUProj sel ns) (HList (: * e l), Proxy HNat n)

Apply (Proxy Bool True, FHUProj sel ns) (HList (: * e l), Proxy HNat n)

(~ * ch (Proxy Bool (HBoolEQ sel (KMember n ns))), Apply (ch, FHUProj sel ns) (HList (: * e l), Proxy HNat n)) => Apply (FHUProj sel ns) (HList (: * e l), Proxy HNat n)

hZero :: Proxy HZero

hSucc :: Proxy (n :: HNat) -> Proxy (HSucc n)

hPred :: Proxy (HSucc n) -> Proxy n

class HNat2Integral n where

Methods

hNat2Integral :: Integral i => Proxy n -> i

Instances

HNat2Integral HZero

HNat2Integral n => HNat2Integral (HSucc n)

type family HNatEq t1 t2 :: Bool

Equality on natural numbers (eventually to be subsumed by the universal polykinded HEq)

type family HLt x y :: Bool

Less than

hLt :: Proxy x -> Proxy y -> Proxy (HLt x y)

Maybies

We cannot use lifted Maybe since the latter are not populated

data HNothing

Constructors

HNothing

Instances

Show HNothing

HUnfold' p HNothing

FromHJust l => FromHJust (: * HNothing l)

newtype HJust x

Constructors

HJust x

Instances

(Apply p s, HUnfold' p (ApplyR p s)) => HUnfold' p (HJust (e, s))

Show x => Show (HJust x)

~ * hJustA (HJust a) => ApplyAB (HJust t) a hJustA

HJust () is a placeholder for a function that applies the HJust constructor

FromHJust l => FromHJust (: * (HJust e) l)

ToHJust l l' => ToHJust (: * e l) (: * (HJust e) l')

Polykinded Equality for types

class HEq x y b | x y -> b

We have to use Functional dependencies for now, for the sake of the generic equality.

Instances

~ Bool False b => HEq k x y b

HEq k x x True

HEq HNat HZero HZero True

HEq HNat HZero (HSucc n) False

HEq HNat (HSucc n) HZero False

HEq HNat n n' b => HEq HNat (HSucc n) (HSucc n') b

HEq [k] ([] k) ([] k) True

HEq [k] ([] k) (: k e l) False

HEq [k] (: k e l) ([] k) False

(HEq k e1 e2 b1, HEq [k] l1 l2 b2, ~ Bool br (HAnd b1 b2)) => HEq [k] (: k e1 l1) (: k e2 l2) br

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

Staged equality

Type-safe cast -- no longer need. We use a a ~ b

Error messages

class Fail x

A class without instances for explicit failure

module Data.Proxy