[Haskell-cafe] Improving HList programming/debugging (longish)

[jeff p]

This message shows how to slightly reformulate HLists (and other type-level
things) to get better type-checking and more informative error messages. The
technique is interesting in that it uses GADTs and functional dependencies and
seems to not be implementable with associated type synonyms. It also makes
higher-order HList programming/debugging much more tractable.

Programming with HLists, at least in our experience, encourages GHC to produce
long and inscrutable type errors. This confusing behaviour is caused by the
open nature of type classes-- GHC (as per the Haskell specification) will
meekly report a conditional type (i.e. expression has type a if a constraint
holds) rather than decisively commit to reporting a type error. By using GADTs
and equality constraints, we can force GHC to be a lot more decisive.

> {-# LANGUAGE
>       EmptyDataDecls,
>       FlexibleInstances,
>       FunctionalDependencies,
>       GADTs,
>       MultiParamTypeClasses,
>       NoMonomorphismRestriction,
>       ScopedTypeVariables,
>       TypeFamilies,
>       TypeOperators,
>       UndecidableInstances
> #-}

We'll start with a standard type level list.

> data Nil
> data x :* xs
> infixr 5 :*

Rather than have direct terms for constructing these lists, we'll make a GADT
for HLists, and use the constructors from the GADT.

> data HList a where
>   Nil :: HList Nil
>   (:*) :: x -> HList xs -> HList (x :* xs)

Notice that every construction of an HList has a type of the form HList a, e.g.:

  *Main> :t 'a' :* () :* Nil
  'a' :* () :* Nil :: HList (Char :* (() :* Nil))

This definition of HLists allows the type checker to rule out malformed term
level representations of HLists:

  *Main> :t 1 :* ()

  <interactive>:1:5:
      Couldn't match expected type `HList xs' against inferred type `()'
      In the second argument of `(:*)', namely `()'
      In the expression: 1 :* ()

We can now write hHead and hTail:

> hHead :: HList (x :* xs) -> x
> hHead (x :* _) = x

> hTail :: HList (x :* xs) -> HList xs
> hTail (_ :* xs) = xs

In order to have higher-order functions on HLists (e.g. fold), we need a way
to apply and evaluate type-level representations of functions to arguments.

> class HEval f x res | f x -> res where
>     hEval :: f -> x -> res

By assuming the function argument to HEval is in weak head normal form, we
will avoid having to write a general eval function at the expense of having to
explicitly sequence calls to hEval ourselves.

We can now write hMap.

> class HMAP f xs res | f xs -> res where
>     hMap :: f -> HList xs -> HList res
> instance HMAP f Nil Nil where
>     hMap _ Nil = Nil
> instance (HEval f x v, HMAP f xs vs) => HMAP f (x :* xs) (v :* vs) where
>     hMap f (x :* xs) = hEval f x :* hMap f xs

We can turn hHead and hTail into type-level functions which can be
mapped over HLists.

> data HHead = HHead
> instance (arg ~ HList (x :* xs)) => HEval HHead arg x
>     where hEval _ = hHead

> data HTail = HTail
> instance (arg ~ HList (x :* xs)) => HEval HTail arg (HList xs)
>     where hEval _ = hTail

Notice that the result of HTail is a HList.

Here is an example:

  *Main> :t hMap HHead (('a' :* "b" :* Nil) :* (() :* Nil) :* Nil)
  hMap HHead (('a' :* "b" :* Nil) :* (() :* Nil) :* Nil)
    :: HList (Char :* (() :* Nil))

By putting an equality constraint in the context of the HEval instances and a
variable in the head, rather than putting the actual type in the head, we
force GHC to use the proper HEval clause for each type-level function, and to
eagerly type-check the evaluation of the function.

  *Main> :t hMap HHead (('a' :* "b" :* Nil) :* "c" :* Nil)

  Top level:
      Couldn't match expected type `HList (v :* xs)'
             against inferred type `[Char]'

If we use a more naive version of the HEval clause for HHead

> data HHead0 = HHead0
> instance HEval HHead0 (HList (x :* xs)) x where
>     hEval _ = hHead

then GHC won't notice the type-level type error

  *Main> :t hMap HHead0 (('a' :* "b" :* Nil) :* "c" :* Nil)
  hMap HHead0 (('a' :* "b" :* Nil) :* "c" :* Nil)
    :: (HEval HHead0 [Char] v) => HList (Char :* (v :* Nil))

until it is actually forced to look at the result type of the hMap.

  *Main> :t hMap HHead0 (('a' :* "b" :* Nil) :* "c" :* Nil) :: HList
(Char :* Char :* Nil)

  <interactive>:1:0:
      No instance for (HEval HHead0 [Char] Char)
        arising from a use of `hMap' at <interactive>:1:0-46
      Possible fix:
        add an instance declaration for (HEval HHead0 [Char] Char)
      In the expression:
            hMap HHead0 (('a' :* "b" :* Nil) :* "c" :* Nil) ::
              HList (Char :* (Char :* Nil))

And the resulting error message is a missing instance, rather than a type clash.

Incidentally, an associated type synonym version of this technique seems to
break down at this point since type indices on an associated type must match
the class instance head; i.e. we can't seem to write HEval with an associated
type synonym instead of a functional dependency.

The remainder of this message is just an exercise meant to show that this
approach really does make HList (and type-level) programming/debugging easier.

We will build the machinery needed to write a hFilter function directly (as a
type class) as well as in terms of a hFoldr. These two forms of hFilter will
behave identically in terms of type checking and error messages.

In order to write a filter for HLists, we need type-level booleans

> data HTrue
> data HFalse
> data HBool a where
>     HTrue :: HBool HTrue
>     HFalse :: HBool HFalse

and an if-then-else construct.

> class HIF yes no bool res | yes no bool -> res where
>     hIf :: yes -> no -> HBool bool -> res
> instance HIF yes no HTrue yes where
>     hIf yes _ _ = yes
> instance HIF yes no HFalse no where
>     hIf _ no _ = no
> data HIf yes no = HIf yes no
> instance (arg ~ HBool b, HIF yes no b res) => HEval (HIf yes no) arg res where
>     hEval (HIf yes no) = hIf yes no

Note that HIF is the type class for hIf, a term level function, while
HIf is a type-level version of hIf.

We can now write hFilter

> class HFILTER p xs res | p xs -> res where
>     hFilter :: p -> HList xs -> HList res
> instance HFILTER p Nil Nil where
>     hFilter _ Nil = Nil
> instance (HFILTER p xs vs,
>           HEval p x (HBool b),
>           HIF (HList (x :* vs)) (HList vs) b (HList res)
>          ) => HFILTER p (x :* xs) res
>     where
>     hFilter p (x :* xs) = hIf (x :* vs) vs (hEval p x) where vs = hFilter p xs

and observe its type-level computation in ghci:

  *Main> :t hFilter HHead ((HTrue :* "a" :* () :* Nil) :* (HFalse :*
'a' :* Nil) :* (HTrue :* Nil) :* Nil)
  hFilter HHead ((HTrue :* "a" :* () :* Nil) :* (HFalse :* 'a' :* Nil)
:* (HTrue :* Nil) :* Nil)
    :: HList
         (HList (HBool HTrue :* ([Char] :* (() :* Nil)))
          :* (HList (HBool HTrue :* Nil) :* Nil))

We can also see that type checking works as expected:

  *Main> :t hFilter HHead ((HTrue :* "a" :* () :* Nil) :* (HFalse :*
'a' :* Nil) :* HTrue :* Nil)

  Top level:
      Couldn't match expected type `HList (HBool b :* xs)'
             against inferred type `HBool HTrue'

  *Main> :t hFilter HHead (("a" :* () :* Nil) :* (HFalse :* 'a' :*
Nil) :* (HTrue :* Nil) :* Nil)

  Top level:
      Couldn't match expected type `HBool b'
             against inferred type `[Char]'
        Expected type: HList (HBool b :* xs)
        Inferred type: HList ([Char] :* (() :* Nil))

We now move on to hFoldr.

> class HFOLDR f acc xs res | f acc xs -> res where
>     hFoldr :: f -> acc -> HList xs -> res
> instance HFOLDR f acc Nil acc where
>     hFoldr _ acc _ = acc
> instance (HFOLDR f acc xs v,
>           HEval f x f1,
>           HEval f1 v res
>          ) => HFOLDR f acc (x :* xs) res
>     where
>     hFoldr f acc (x :* xs) = hEval (hEval f x) (hFoldr f acc xs)

Note that since we assume the function argument to hEval is in weak head
normal form, we must evaluate each piece of the resulting application of f to
its two arguments.

In order to have curried functions and partial applications, we will
have type-level syntactic application which is used to build up type-level
applications.

> data f :$ x = f :$ x
> infixl 3 :$

We can now write a type-level cons (:*) function, which also serves as
an example for how :$ is meant to be used.

> data Cons = Cons
> instance HEval Cons x (Cons :$ x) where
>     hEval = (:$)
> instance (arg ~ HList xs) => HEval (Cons :$ x) arg (HList (x :* xs)) where
>     hEval (Cons :$ x) = (x :*)

Note that :$ must be used with care since hEval is not a general
evaluation function.

  *Main> hEval HHead (Cons :$ "a" :$ Nil)

  <interactive>:1:0:
      Couldn't match expected type `HList (res :* xs)'
             against inferred type `(Cons :$ [Char]) :$ HList Nil'
      When generalising the type(s) for `it'

  *Main> hEval HHead (hEval (Cons :$ "a") Nil)
  "a"

The lack of type-level lambdas forces higher-order type-level programming to
be point-free. In order to facilitate point-free programming we need to be
able to uncurry type-level functions.

> data Uncurry = Uncurry
> instance (arg ~ (x, y), HEval f x f1, HEval f1 y res) => HEval (Uncurry :$ f) arg res where
>     hEval (Uncurry :$ f) (x, y) = hEval (hEval f x) y

Here is some machinery for manipulating pairs.

> data Fst = Fst
> instance (arg ~ (x, y)) => HEval Fst arg x where
>     hEval _ = fst

> data Snd = Snd
> instance (arg ~ (x, y)) => HEval Snd arg y where
>     hEval _ = snd

> (f &&& g) x = (f x, g x)
> data f :&&& g = f :&&& g
> instance (HEval f x fv, HEval g x gv) => HEval (f :&&& g) x (fv, gv) where
>     hEval (f :&&& g) = hEval f &&& hEval g

Note that we have not made :&&& fully partially applicable (nor HIf from above
either). This limitation is for convenience (we won't be needing to partially
apply either combinator) as nothing prevents writing the fully partially
applicable combinators. (*)

Since our goal is to write hFilter in terms of hFoldr, we should start by
writing filter in terms of a point-free foldr:

> fltr p = foldr (uncurry (myIf fst snd) . (p &&& ((:) &&& flip const))) []
>   where myIf yes no b = if b then yes else no

Now we just have to provide type-level versions of composition, flip and const.

> data f :. g = f :. g
> instance (HEval g x v0, HEval f v0 v) => HEval (f :. g) x v where
>     hEval (f :. g) = hEval f . hEval g

> data Flip = Flip
> instance HEval Flip f (Flip :$ f) where
>     hEval = (:$)
> instance HEval (Flip :$ f) x (Flip :$ f :$ x) where
>     hEval = (:$)
> instance (HEval (f :$ x) x0 res) => HEval (Flip :$ f :$ x0) x res where
>     hEval (Flip :$ f :$ x0) x = hEval (f :$ x) x0

> data Const = Const
> instance HEval Const x (Const :$ x) where
>     hEval = (:$)
> instance HEval (Const :$ x) y x where
>     hEval (Const :$ x) = const x

Finally we can simply write our type-level filter in terms of hFoldr

> hFltr p = hFoldr ((Uncurry :$ (HIf Fst Snd)) :. (p :&&& (Cons :&&& (Flip :$ Const)))) Nil

and observe how it works in ghci:

  *Main> :t hFltr HHead ((HTrue :* "a" :* () :* Nil) :* (HFalse :* 'a'
:* Nil) :* (HTrue :* Nil) :* Nil)
  hFltr HHead ((HTrue :* "a" :* () :* Nil) :* (HFalse :* 'a' :* Nil)
:* (HTrue :* Nil) :* Nil)
    :: HList
         (HList (HBool HTrue :* ([Char] :* (() :* Nil)))
          :* (HList (HBool HTrue :* Nil) :* Nil))

  *Main> :t hFltr HHead ((HTrue :* "a" :* () :* Nil) :* (HFalse :* 'a'
:* Nil) :* HTrue :* Nil)

  Top level:
      Couldn't match expected type `HList (HBool b :* xs)'
             against inferred type `HBool HTrue'

  *Main> :t hFltr HHead (("a" :* () :* Nil) :* (HFalse :* 'a' :* Nil)
:* (HTrue :* Nil) :* Nil)

  Top level:
      Couldn't match expected type `HBool b'
             against inferred type `[Char]'
        Expected type: HList (HBool b :* xs)
        Inferred type: HList ([Char] :* (() :* Nil))

Any comments/feedback will be appreciated.

Jeff

(*) Here is a partially applicable fanout (:&&&):

> data Fanout = Fanout
> instance HEval Fanout f (Fanout :$ f) where
>     hEval = (:$)
> instance HEval (Fanout :$ f) g (Fanout :$ f :$ g) where
>     hEval = (:$)
> instance (HEval f x fx, HEval g x gx) => HEval (Fanout :$ f :$ g) x (fx, gx) where
>     hEval (Fanout :$ f :$ g) = hEval f &&& hEval g