[Haskell-cafe] Using promoted lists

[AntC]

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