Am Dienstag, den 11.01.2011, 20:05 -0500 schrieb 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.
Hi, a few years ago, I also experienced with using GADTs for representing heterogenous lists. However, I dropped this idea, since GADTs force you to provide type signatures in certain situations. For example, you cannot leave out the type signatures in the following definitions:
hHead :: HList (x :* xs) -> x hHead (x :* _) = x
hTail :: HList (x :* xs) -> HList xs hTail (_ :* xs) = xs
This was at odds with a feature I wanted: It should be possible to match a polymorphic value representing a family of heterogenous lists against a pattern such that the type of the pattern specifies the concrete list to use. I finally switched back to the traditional approach used in today’s HList. You can read about the pattern-matching thing in Subsection 5.4 of my paper “Generic Record Combinators with Static Type Checking” [1]. Best wishes, Wolfgang [1] http://www.informatik.tu-cottbus.de/~jeltsch/research/ppdp-2010-paper.pdf