[Haskell-cafe] Using promoted lists

[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<http://hackage.haskell.org/trac/ghc/wiki/NewAxioms>


2012/6/8 AntC <anthony_clayden at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120608/f8850ca4/attachment.htm>