Thanks for your answers, Anthony and Erik.

I'll try with fundeps. I know about HList, but back at the time when I looked at it I found quite complex.

Anthony, the link you gave me [1] tends to show that actually Bool type is promoted.

type family Member x (l :: [*]) :: Bool
type instance Member x (x ': xs) = True
works.
So if I understand well, unlike what I thought when I saw the compilation fail, the two x's type variables are actually unified, but then the second instance
type instance Member x (y ': xs) = True
encompasses the first, so GHC refuses to handle it (as it would at the value level with regular case expressions).
So yes, [1] is exactly what I was trying to do.

Out of curiosity, I tried with Int, and it works too, I can express:
type family Something a :: Int
But then, the following doesn't compile
type instance Something String = 42
( The wild guess '42 does not either ) So I guess we don't have type-level integers for now. How are promoted Ints usable then?


[1] http://hackage.haskell.org/trac/ghc/wiki/NewAxioms


2012/6/8 AntC <anthony_clayden@clear.net.nz>
Yves Parès <yves.pares <at> gmail.com> writes:

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


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe