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. applyAB defined below, is more complicated / verbose to define, but it offers better type inference. Most uses have been converted to applyAB, 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. An example of this is:

f op = (op (1 :: Double), op (1 :: Int))

RankNTypes

One solution is to enable `-XRankNTypes` and then write a type signature which might be `f :: (forall a. Num a => a -> a)`. This does not work in the context of HList, since we want to use functions that do not necessarily fall into the pattern of (forall a. c a => a -> a).

MultipleArguments

Another solution is to rewrite op to look like

f op1 op2 = (op1 (1:: Double), op2 (1 :: Int))

In some sense this approach works (see HZip), but the result is constrained to as many function applications as you are willing to write (ex. a function that works for records of six entries would look like hBuild f f f f f f).

Defunctionalization

Therefore the selected 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. Since applyAB Fn :: Int -> Double has a monomorphic type, this trimmed down example does not really make sense because applyAB (fromIntegral :: Int -> Double) is exactly the same. Nontheless, the other uses of ApplyAB follow this pattern, and the benefits are seen when the type of applyAB Fn has at least one type variable.

Additional explanation can be found in local functional dependencies

AmbiguousTypes

Note that ghc only allows AllowAmbiguousTypes when a type signature is provided. Thus expressions such as:

data AddJust = AddJust
instance (y ~ Maybe x) => ApplyAB AddJust x y where
   applyAB _ x = Just x

twoJustsBad = hMap AddJust . hMap AddJust -- ambiguous type

Are not accepted without a type signature that references the intermediate "b":

twoJusts :: forall r a b c. (HMapCxt r AddJust a b, HMapCxt r AddJust b c) =>
       r a -> r c
twoJusts a = hMap AddJust (hMap AddJust a :: r b)

An apply class with functional dependencies

class ApplyAB' f a b | f a -> b, f b -> a

Or with equivalent type families

class (GetB f a ~ b, GetA f b ~ a) => ApplyAB' f a b

would not require an annotation for twoJusts. However, not all instances of ApplyAB will satisfy those functional dependencies, and thus the number of classes would proliferate. Furthermore, inference does not have to be in one direction only, as the example of HMap shows.

class ApplyAB f a b where

No constraints on result and argument types

Methods

applyAB :: f -> a -> b

Instances

(~) * (Tagged k t x) tx => ApplyAB HUntag tx x

((~) * 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

((~) * aa (a, a), Monoid a) => ApplyAB UncurryMappend aa a

((~) * x (Proxy * y), Monoid y) => ApplyAB ConstMempty x y

(~) * 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

(~) * tx (Tagged k t x) => ApplyAB TaggedFn x tx

((~) * x (Tagged k t (Maybe e), [Variant v]), (~) * y [Variant ((:) * (Tagged k t e) v)], MkVariant k t e ((:) * (Tagged k t e) v)) => ApplyAB HMaybiedToVariantFs x y

(~) * y (Tagged k t (Maybe e)) => ApplyAB ConstTaggedNothing x y

((~) * mx (Maybe x), (~) * my (Maybe y), HCast y x) => ApplyAB HCastF mx my

((~) * ee (e, e), Eq e, (~) * bool Bool) => ApplyAB UncurryEq ee bool

((~) * x (Tagged k l v), (~) * y (HList ((:) * (Label k l) ((:) * v ([] *))))) => ApplyAB TaggedToKW x y

((~) * ux (RecordU x), (~) * hx (HList x), RecordUToRecord x) => ApplyAB BoxF ux hx

((~) * hx (HList x), (~) * ux (RecordU x), RecordToRecordU x) => ApplyAB UnboxF hx ux

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

((~) * y (ReadP x), Read x) => ApplyAB ReadElement (Proxy * x) y

(Read v, ShowLabel k l, (~) * x (Tagged k l v), (~) * (ReadP x) y) => ApplyAB ReadComponent (Proxy * x) y

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

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

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

((~) * x (t a), (~) * y (t b), Functor t, ApplyAB f a b) => ApplyAB (HFmap f) x y

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

((~) * hxs (HList xs), (~) * hxxs (HList ((:) * x xs))) => ApplyAB (FHCons2 x) hxs hxxs

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

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

(HMapCxt HList f a b, (~) * as (HList a), (~) * bs (HList b)) => ApplyAB (HMapL f) as bs

(HMapCxt r f a b, (~) * as (r a), (~) * bs (r b)) => ApplyAB (HMap f) as bs

(HMapCxt Record f x y, (~) * rx (Record x), (~) * ry (Record y)) => ApplyAB (HMapR f) rx ry

((~) * vx (Variant x), (~) * vy (Variant y), HMapAux Variant (HFmap f) x y, SameLength * * x y) => ApplyAB (HMapV f) vx vy

apply a function to all values that could be in the variant.

(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 k cxt geta) a b

(FunCxt k cxt a, (~) * (FunApp k1 getb a) b) => ApplyAB (Fun k k 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 plus1f x = if x < 5 then x+1 else 5
>>> let plus1 = Fun plus1f :: Fun '[Num, Ord] '()
>>> :t applyAB plus1
applyAB plus1 :: (Num b, Ord b) => b -> b

>>> let xs = [1 .. 8]
>>> map (applyAB plus1) xs == map plus1f xs
True

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

>>> 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 k 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 k cxt geta) a b

type family FunApp fns a

Instances

type FunApp * fn a = fn

type FunApp () fn a = a

type FunApp (* -> *) fn a = fn a

type family FunCxt cxts a :: Constraint

Instances

type FunCxt * cxt a = (~) * cxt a

type FunCxt () cxt a = ()

should there be so many ways to write no constraint?

type FunCxt [k] ([] k) a = ()

type FunCxt [* -> Constraint] ((:) (* -> Constraint) x xs) a = (x a, FunCxt [* -> Constraint] xs a)

type FunCxt (* -> Constraint) cxt a = cxt a

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

newtype HFmap f

fmap

Constructors

HFmap f

Instances

((~) * x (t a), (~) * y (t b), Functor t, ApplyAB f a b) => ApplyAB (HFmap f) x y

newtype LiftA2 f

liftA2

Constructors

LiftA2 f

Instances

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

data HUntag

untag

Constructors

HUntag

Instances

(~) * (Tagged k t x) tx => ApplyAB HUntag tx x

Proxy

see Data.Proxy

data Label l

A special Proxy for record labels, polykinded

Constructors

Label

Instances

HEqBy * k HLeFn x y b => HEqBy * * HLeFn (Label k x) (Label k y) b

(~) * (Label k t) (Label Symbol t') => SameLabels * Symbol (Label k t) t'

(~) * (Label k t) (Label k1 t') => SameLabels * * (Label k t) (Label k t')

(~) * (Label k t) (Label k1 t') => SameLabels * * (Label k t) (Tagged k t' a)

(~) * (Label k t) (Label * (Lbl ix ns n)) => SameLabels * * (Label k t) (Lbl ix ns n)

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

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

HExtend (Label * (Lbl n ns desc)) (Proxy [Symbol] ((:) Symbol x xs))

Mixing two label kinds means we have to include Label:

>>> let r = label3 .*. label6 .*. emptyProxy
>>> :t r
r :: Proxy '[Label (Lbl 'HZero () ()), Label "6"]

HExtend (Label * (Lbl n ns desc)) (Proxy [*] ((:) * (Lbl n' ns' desc') xs))

If possible, Label is left off:

>>> let q = label3 .*. label3 .*. emptyProxy
>>> :t q
q :: Proxy '[Lbl 'HZero () (), Lbl 'HZero () ()]

HExtend (Label Nat y) (Proxy [Symbol] ((:) Symbol x xs))

HExtend (Label Nat y) (Proxy [*] ((:) * x xs))

HExtend (Label Nat y) (Proxy [Nat] ((:) Nat x xs))

HExtend (Label Symbol y) (Proxy [Nat] ((:) Nat x xs))

HExtend (Label Symbol y) (Proxy [*] ((:) * x xs))

Mixing two label kinds means we have to include Label:

>>> let s = label6 .*. label3 .*. emptyProxy
>>> :t s
s :: Proxy '[Label "6", Label (Lbl 'HZero () ())]

HExtend (Label Symbol y) (Proxy [Symbol] ((:) Symbol x xs))

>>> let labelX = Label :: Label "x"
>>> let labelY = Label :: Label "y"
>>> let p = labelX .*. labelY .*. emptyProxy
>>> :t p
p :: Proxy '["x", "y"]

HExtend (Label k x) (Proxy [*] ([] *))

to keep types shorter, .*. used with Proxy avoids producing a Proxy :: Proxy '[Label x,Label y,Label z] if Proxy :: Proxy '[x,y,z] is not a kind error (as it is when mixing Label6 and Label3 labels).

ghc-7.6 does not accept Proxy ('[] :: [k]) so for now require k ~ *

type UnLabel k proxy ((:) * (Label k x) xs) = (:) k x (UnLabel k proxy xs)

type ZipTagged * ((:) * (Label k t) ts) ((:) * v vs) = (:) * (Tagged k t v) (ZipTagged * ts vs)

type HExtendR (Label * (Lbl n ns desc)) (Proxy [Symbol] ((:) Symbol x xs)) = Proxy [*] ((:) * (Label * (Lbl n ns desc)) (MapLabel Symbol ((:) Symbol x xs)))

type HExtendR (Label * (Lbl n ns desc)) (Proxy [*] ((:) * (Lbl n' ns' desc') xs)) = Proxy [*] ((:) * (Lbl n ns desc) ((:) * (Lbl n' ns' desc') xs))

type HExtendR (Label Nat y) (Proxy [Symbol] ((:) Symbol x xs)) = Proxy [*] ((:) * (Label Nat y) (MapLabel Symbol ((:) Symbol x xs)))

type HExtendR (Label Nat y) (Proxy [*] ((:) * x xs)) = Proxy [*] ((:) * (Label Nat y) (MapLabel * ((:) * x xs)))

type HExtendR (Label Nat y) (Proxy [Nat] ((:) Nat x xs)) = Proxy [Nat] ((:) Nat y ((:) Nat x xs))

type HExtendR (Label Symbol y) (Proxy [Nat] ((:) Nat x xs)) = Proxy [*] ((:) * (Label Symbol y) (MapLabel Nat ((:) Nat x xs)))

type HExtendR (Label Symbol y) (Proxy [*] ((:) * x xs)) = Proxy [*] ((:) * (Label Symbol y) (MapLabel * ((:) * x xs)))

type HExtendR (Label Symbol y) (Proxy [Symbol] ((:) Symbol x xs)) = Proxy [Symbol] ((:) Symbol y ((:) Symbol x xs))

type HExtendR (Label k x) (Proxy [*] ([] *)) = Proxy [k] ((:) k x ([] k))

type LabelsOf ((:) * (Label k l) r) = (:) * (Label k l) (LabelsOf r)

labelToProxy :: Label l -> Proxy l

class ShowLabel l where

Methods

showLabel :: Label l -> String

Instances

Typeable * x => ShowLabel * x

Equality on labels

Show label

KnownNat x => ShowLabel Nat x

KnownSymbol x => ShowLabel Symbol x

Show desc => ShowLabel * (Lbl 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

Instances

type HAnd False t = False

type HAnd True t = t

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

demote to values

Disjunction

type family HOr t1 t2 :: Bool

Instances

type HOr False t = t

type HOr True t = True

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

type family HNot x :: Bool

Instances

type HNot False = True

type HNot True = False

class HNotFD b nb | b -> nb, nb -> b

as compared with HNot this version is injective

Instances

HNotFD False True

HNotFD True False

hNot :: HNotFD a notA => Proxy a -> Proxy notA

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

Instances

type HBoolEQ False False = True

type HBoolEQ False True = False

type HBoolEQ True False = False

type HBoolEQ True True = True

Naturals

data HNat

The data type to be lifted to the type level

Constructors

HZero

HSucc HNat

Instances

Typeable HNat HZero

(~) [*] xxs ([] *) => HLengthEq1 HNat xxs HZero

(~) Bool (HLe x y) b => HEqBy * HNat HLeFn x y b

(HLengthEq xs n, (~) [*] xxs ((:) * x xs)) => HLengthEq1 HNat xxs (HSucc n)

(~) HNat zero HZero => HLengthEq2 HNat ([] *) zero

HFindMany k ([] k) r ([] HNat)

(HLengthEq xs n, (~) HNat sn (HSucc n)) => HLengthEq2 HNat ((:) * x xs) sn

(HFind k l r n, HFindMany k ls r ns) => HFindMany k ((:) k l ls) r ((:) HNat n ns)

HNats2Integrals ([] HNat)

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

And lift to the list of types

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

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

HNat2Integral n => Show (Proxy HNat n)

Typeable (HNat -> * -> * -> *) Lbl

Typeable (HNat -> HNat) HSucc

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)

(HNats2Integrals ns, HNat2Integral n) => HNats2Integrals ((:) HNat n ns)

(HNat2Integral n, (~) * (HLookupByHNatR n u) le, (~) * le (Tagged k l e), IArray UArray e, (~) * e (GetElemTy u)) => HLookupByHNatUS1 (Left HNat HNat t) n u us le

HLookupByHNatUS t us e => HLookupByHNatUS1 (Right HNat HNat t) n u us e

type KMember n ([] HNat) = False

type KMember n ((:) HNat n1 l) = HOr (HNatEq n n1) (KMember n l)

type ApplyR (FHLookupByHNat l) (Proxy HNat n) = HLookupByHNatR n l

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

type ApplyR (Proxy Bool True, FHUProj sel ns) (HList ((:) * e l), Proxy HNat n) = HJust (e, (HList l, Proxy HNat (HSucc n)))

type ApplyR (FHUProj sel ns) (HList ((:) * e l), Proxy HNat n) = ApplyR (Proxy Bool (HBoolEQ sel (KMember n ns)), FHUProj sel ns) (HList ((:) * e l), Proxy HNat n)

type HNats ((:) * (Proxy HNat n) l) = (:) HNat n (HNats l)

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

KnownNat (HNat2Nat n) => HNat2Integral n

type family HNat2Nat n :: Nat

Instances

type HNat2Nat HZero = 0

type HNat2Nat (HSucc n) = (+) 1 (HNat2Nat n)

class HNats2Integrals ns where

Methods

hNats2Integrals :: Integral i => Proxy ns -> [i]

Instances

HNats2Integrals ([] HNat)

(HNats2Integrals ns, HNat2Integral n) => HNats2Integrals ((:) HNat n ns)

type family HNatEq t1 t2 :: Bool

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

Instances

type HNatEq HZero HZero = True

type HNatEq HZero (HSucc n) = False

type HNatEq (HSucc n) HZero = False

type HNatEq (HSucc n) (HSucc n') = HNatEq n n'

type family HLt x y :: Bool

Less than

Instances

type HLt HZero HZero = False

type HLt HZero (HSucc n) = True

type HLt (HSucc n) HZero = False

type HLt (HSucc n) (HSucc n') = HLt n n'

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

type family HLe x y :: Bool

Less than or equal to

Instances

type HLe HZero HZero = True

type HLe (HSucc x) y = HLt x y

hLe :: Proxy x -> Proxy y -> Proxy (HLe x y)

type family HDiv2 x :: HNat

HDiv2 x behaves like x div 2

Instances

type HDiv2 HZero = HZero

type HDiv2 (HSucc (HSucc a)) = HSucc (HDiv2 a)

type HDiv2 (HSucc HZero) = HZero

Maybies

We cannot use lifted Maybe since the latter are not populated

data HNothing

Constructors

HNothing

Instances

Show HNothing

HUnfoldFD p HNothing ([] *)

FromHJust l => FromHJust ((:) * HNothing l)

type HUnfoldR p HNothing = [] *

type FromHJustR ((:) * HNothing l) = FromHJustR l

newtype HJust x

Constructors

HJust x

Instances

(Apply p s, HUnfoldFD p (ApplyR p s) z) => HUnfoldFD p (HJust (e, s)) ((:) * e z)

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)

type HUnfoldR p (HJust (e, s)) = (:) * e (HUnfoldR p (ApplyR p s))

type FromHJustR ((:) * (HJust e) l) = (:) * e (FromHJustR 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

type HEqK x y b = HEq (Proxy x) (Proxy y) b

Equality for types that may have different kinds. This definition allows operations on Record [Tagged "x" a, Tagged 2 b] to work as expected.

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

class HEqByFn f => HEqBy f x y b | f x y -> b

this class generalizes HEq by allowing the choice of f to allow equating only part of x and y

Instances

((~) * txv (Tagged k x v), (~) * tyw (Tagged k1 y w), HEq * v w b) => HEqBy * * EqTagValue txv tyw b

(~) Bool ((<=?) x y) b => HEqBy * Nat HLeFn x y b

only in ghc >= 7.7

(HEq Ordering (CmpSymbol x y) GT nb, (~) Bool (HNot nb) b) => HEqBy * Symbol HLeFn x y b

only in ghc >= 7.7

>>> let b1 = Proxy :: HEqBy HLeFn "x" "y" b => Proxy b
>>> :t b1
b1 :: Proxy 'True

>>> let b2 = Proxy :: HEqBy HLeFn "x" "x" b => Proxy b
>>> :t b2
b2 :: Proxy 'True

>>> let b3 = Proxy :: HEqBy HLeFn "y" "x" b => Proxy b
>>> :t b3
b3 :: Proxy 'False

(~) Bool (HLe x y) b => HEqBy * HNat HLeFn x y b

HEqBy * k HLeFn x y b => HEqBy * * HLeFn (Proxy k x) (Proxy k y) b

HEqBy * k HLeFn x y b => HEqBy * * HLeFn (Label k x) (Label k y) b

HEqBy * k HLeFn x y b => HEqBy * * HLeFn (Tagged k x v) (Tagged k y w) b

(HEqBy * HNat HLeFn n m b, (~) * ns ns') => HEqBy * * HLeFn (Lbl n ns desc) (Lbl m ns' desc') b

Data.HList.Label3 labels can only be compared if they belong to the same namespace.

(HEqBy k1 k le y x b1, (~) Bool (HNot b1) b2) => HEqBy * k (HNeq k le) x y b2

HEqBy k1 k f y x b => HEqBy * k (HDown k f) x y b

class HEqByFn f

Every instance of this class should have an instance of HEqBy

Instances

HEqByFn * HLeFn

HEqByFn * EqTagValue

HEqByFn k a => HEqByFn * (HNeq k a)

HEqByFn k a => HEqByFn * (HDown k a)

Arity

type Arity f n = (ArityFwd f n, ArityRev f n)

class ArityFwd f n | f -> n

calculate the number of arguments a function can take

Instances

(~) HNat hZero HZero => ArityFwd f hZero

Arity f n => ArityFwd (x -> f) (HSucc n)

class ArityRev f n

given the number of arguments a function can take, make sure the function type actually matches

Instances

ArityRev f HZero

((~) * xf (x -> f), ArityRev f n) => ArityRev xf (HSucc n)

Staged equality

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

Cast

class HCast x y where

Named after cast, which behaves the same at runtime. One difference is that there is a HCast instance for every type, while Typeable instances can be missing sometimes.

Methods

hCast :: x -> Maybe y

Instances

(HEq * x y b, HCast1 b x y) => HCast x y

class HCast1 b x y where

helper for HCast

Methods

hCast1 :: Proxy b -> x -> Maybe y

Instances

HCast1 False x y

(~) * x y => HCast1 True x y

Error messages

class Fail x

A class without instances for explicit failure

Uses of fail

these could be replaced by `'("helpful message", l)`, but these look better.

data ExtraField l

data FieldNotFound l

Instances

Fail * (FieldNotFound k l) => HasField k l (Record ([] *)) (FieldNotFound k l)

type TypeablePolyK a = Typeable a

Constraining Lists

Length

class SameLength' es1 es2

Ensure two lists have the same length. We do case analysis on the first one (hence the type must be known to the type checker). In contrast, the second list may be a type variable.

Instances

(~) [k1] es2 ([] k1) => SameLength' k k ([] k) es2

(SameLength' k k1 xs ys, (~) [k1] es2 ((:) k1 y ys)) => SameLength' k k ((:) k x xs) es2

class (SameLength' x y, SameLength' y x) => SameLength x y where

symmetrical version of SameLength'. Written as a class instead of

type SameLength a b = (SameLength' a b, SameLength' b a)

since ghc expands type synonyms, but not classes (and it seems to have the same result)

Minimal complete definition

Nothing

Methods

sameLength :: (r x `p` f (q y)) -> r x `p` f (q y)

SameLength x y => Equality (r x) (q y) (r x) (q y)

used like simple, except it restricts the type-level lists involved to have the same length, without fixing the type of container or the elements in the list.

Instances

(SameLength' k k1 x y, SameLength' k1 k y x) => SameLength k k x y

asLengthOf :: SameLength x y => r x -> s y -> r x

type family SameLengths xs :: Constraint

Instances

type SameLengths k ([] [k]) = ()

type SameLengths k ((:) [k] x ([] [k])) = ()

type SameLengths k ((:) [k] x ((:) [k] y ys)) = (SameLength k k x y, SameLengths k ((:) [k] y ys))

Labels

class SameLabels x y

Instances

SameLabels * k (Label Symbol t) s => SameLabels Symbol k t s

(~) * (Label k t) (Label Symbol t') => SameLabels * Symbol (Label k t) t'

(~) * (Label k t) (Label k1 t') => SameLabels * * (Label k t) (Label k t')

(~) * (Label k t) (Label k1 t') => SameLabels * * (Label k t) (Tagged k t' a)

(~) * (Label k t) (Label * (Lbl ix ns n)) => SameLabels * * (Label k t) (Lbl ix ns n)

SameLabels * k (Label k1 t) s => SameLabels * k (Tagged k t a) s

SameLabels [k] [k] ([] k) ([] k)

SameLabels [k] [k] ([] k) ((:) k x xs)

SameLabels [k] [k] ((:) k x xs) ([] k)

(SameLabels k k1 x y, SameLabels [k] [k1] xs ys) => SameLabels [k] [k] ((:) k x xs) ((:) k y ys)

sameLabels :: SameLabels x y => p (r x) (f (q y)) -> p (r x) (f (q y))

sameLabels constrains the type of an optic, such that the labels (t in Tagged t a) are the same. x or y may have more elements than the other, in which case the elements at the end of the longer list do not have their labels constrained.

see also sameLength

A list has only Tagged values

class HAllTaggedLV ps

The Record, Variant, TIP, TIC type constructors only make sense when they are applied to an instance of this class

Instances

HAllTaggedLV ([] *)

(HAllTaggedLV xs, (~) * x (Tagged k t v)) => HAllTaggedLV ((:) * x xs)

type family ZipTagged ts vs :: [*]

see Data.HList.Record.zipTagged

Instances

type ZipTagged k ([] k) ([] *) = [] *

type ZipTagged * ((:) * (Label k t) ts) ((:) * v vs) = (:) * (Tagged k t v) (ZipTagged * ts vs)

type ZipTagged * ((:) * (Lbl ix ns n) ts) ((:) * v vs) = (:) * (Tagged * (Lbl ix ns n) v) (ZipTagged * ts vs)

type ZipTagged Symbol ((:) Symbol t ts) ((:) * v vs) = (:) * (Tagged Symbol t v) (ZipTagged Symbol ts vs)

module Data.Proxy

module Data.Tagged

class Monoid a where

The class of monoids (types with an associative binary operation that has an identity). Instances should satisfy the following laws:

• mappend mempty x = x

• mappend x mempty = x

• mappend x (mappend y z) = mappend (mappend x y) z

• mconcat = foldr mappend mempty

The method names refer to the monoid of lists under concatenation, but there are many other instances.

Minimal complete definition: mempty and mappend.

Some types can be viewed as a monoid in more than one way, e.g. both addition and multiplication on numbers. In such cases we often define newtypes and make those instances of Monoid, e.g. Sum and Product.

Minimal complete definition

mempty, mappend

Methods

mempty :: a

Identity of mappend

mappend :: a -> a -> a

An associative operation

mconcat :: [a] -> a

Fold a list using the monoid. For most types, the default definition for mconcat will be used, but the function is included in the class definition so that an optimized version can be provided for specific types.

Instances

Monoid Ordering

Monoid ()

Monoid All

Monoid Any

Monoid Text

Monoid Text

Monoid [a]

Monoid a => Monoid (Dual a)

Monoid (Endo a)

Num a => Monoid (Sum a)

Num a => Monoid (Product a)

Monoid (First a)

Monoid (Last a)

Monoid a => Monoid (Maybe a)

Lift a semigroup into Maybe forming a Monoid according to http://en.wikipedia.org/wiki/Monoid: "Any semigroup S may be turned into a monoid simply by adjoining an element e not in S and defining e*e = e and e*s = s = s*e for all s ∈ S." Since there is no "Semigroup" typeclass providing just mappend, we use Monoid instead.

(Ord a, Bounded a) => Monoid (Min a)

(Ord a, Bounded a) => Monoid (Max a)

Monoid m => Monoid (WrappedMonoid m)

Semigroup a => Monoid (Option a)

(Hashable a, Eq a) => Monoid (HashSet a)

(HProxies a, HMapCxt HList ConstMempty (AddProxy [*] a) a, HZip HList a a aa, HMapCxt HList UncurryMappend aa a) => Monoid (HList a)

Analogous to the Monoid instance for tuples

>>> import Data.Monoid
>>> mempty :: HList '[(), All, [Int]]
H[(),All {getAll = True},[]]

>>> mappend (hBuild "a") (hBuild "b") :: HList '[String]
H["ab"]

Monoid (HList r) => Monoid (Record r)

Monoid (HList a) => Monoid (TIP a)

(Monoid x, Monoid (Variant ((:) * a b))) => Monoid (Variant ((:) * (Tagged k t x) ((:) * a b)))

XXX check this mappend is legal

(Unvariant ((:) * (Tagged k t x) ([] *)) x, Monoid x) => Monoid (Variant ((:) * (Tagged k t x) ([] *)))

Monoid (Variant l) => Monoid (TIC l)

Monoid b => Monoid (a -> b)

(Monoid a, Monoid b) => Monoid (a, b)

Monoid a => Monoid (Const a b)

Monoid (Proxy * s)

(Eq k, Hashable k) => Monoid (HashMap k v)

Typeable (* -> Constraint) Monoid

(Monoid a, Monoid b, Monoid c) => Monoid (a, b, c)

Monoid a => Monoid (Tagged k s a)

(Monoid a, Monoid b, Monoid c, Monoid d) => Monoid (a, b, c, d)

(Monoid a, Monoid b, Monoid c, Monoid d, Monoid e) => Monoid (a, b, c, d, e)