The HList library

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

Some very basic technology for faking dependent types in Haskell.

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.

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

see Data.Proxy

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

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

We cannot use lifted Maybe since the latter are not populated

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