Hi Yves,
The type level numbers have kind Nat, not Int (and so also can't be
negative). They have to be imported from GHC.TypeLits (I'm not sure if
this will change). So the following code works for me in HEAD:
{-# LANGUAGE TypeFamilies, DataKinds #-}
import GHC.TypeLits
type family Something a :: Nat
type instance Something String = 42
Regards,
Erik
On Fri, Jun 8, 2012 at 8:45 AM, Yves Parès
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
Yves Parès
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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe