[Haskell-cafe] Using promoted lists

[Erik Hesselink]

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 <yves.pares at gmail.com> wrote:
> 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 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
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>