Yves Parès
The doc page http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/kind-
polymorphism-and-promotion.html#promotion show that lists are now usable as types.So I'm trying to make a type level function to test if a type list contains a type. Unless I'm wrong, that calls to the use of a type family. {-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies #-} data HBool = HTrue | HFalse -- Mandatory as Bool type is not currently promoted to a kind type family Member x (l :: [*]) :: HBool type instance Member x (x ': xs) = HTrue type instance Member x (y ': xs) = Member x xs type instance Member x (y ': '[]) = HFalse
But the compiler complains about my instance conflicting.
Hi Yves, always when you're asking a question like this, give the error message in full -- usually it will explain what's wrong. In this case I can guess: you have overlapping instances (the first overlaps the second, the third overlaps the second), which are not allowed for type functions (currently -- unless the equations are confluent). There's some early work on introducing overlaps to type functions (in a controlled way). http://hackage.haskell.org/trac/ghc/wiki/NewAxioms And as it happens, several threads are going on in the lists re options and implications.
Is what I'm trying to do feasible?
Promoted lists are really just the same as HLists, but using the standard Haskell syntax. A membership test is feasible with FunDeps (because they do allow overlaps), but I guess you know the HList stuff, judging from your HBool. It's feasible using type equality constraints to achieve the same as HList (so ~ is equivalent to HList's TypeCast), also with overlaps.
Second question: how can type level tuples (also mentioned in the doc page) be exploited? Aren't they redundant with type-level lists?
Type-level tuples are fixed length, and provide a flat structure (any element is equally accessible), whereas lists are expandable, with a nested structure that means you have to scan down the structure to get to the element you want. AntC