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