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. 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

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

see Data.HList.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