[Haskell-cafe] How to build an "Indicator Type" for a type class?

[Steffen Schuldenzucker]

On 06/02/2010 03:59 AM, Brent Yorgey wrote:
> Perhaps something here may be of use?
> 
>   http://okmij.org/ftp/Haskell/types.html#class-based-overloading

Enlightening. Thanks a lot. For the curious, here is my solution:

http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25907#a25907

I'm gonna read the HList paper now...

Best regards,

Steffen

>   http://okmij.org/ftp/Haskell/types.html#class-based-dispatch
> 
> -Brent
> 
> On Mon, May 31, 2010 at 01:32:18PM +0200, Steffen Schuldenzucker wrote:
>> Dear Cafe,
>>
>> let:
>>
>>> data True
>>> data False
>>>
>>> class C a
>>
>> (arbitrary instances for C may follow)
>>
>> Now, how to obtain an "Indicator Type" for C, i.e. a type IndC that is defined
>> via a type family / fundep / ... , so that
>>
>> IndC a = True 	forall a which are instances of C
>> IndC a = False 	for all other a.
>>
>> I've collected some failed approaches here[1]. My key problem is that if I
>> define (in the 3rd try):
>>
>>> instance (C a) => IndC3 a True
>>
>> , it does *not* mean "Define this instance for all a which are an instance of
>> C", but "Define the instance IndC3 a True for all types a, but it's not gonna
>> work if a is not an instance of C".
>>
>> Does anyone have another idea?
>>
>> Background:
>>
>> After having implemented type-level lists[2] and a quicksort on them[3], I'd
>> like to have type-level sets. In their most simple implementation, sets are
>> just (unsorted) lists like this:
>>
>>> data Nil
>>> data Cons a b
>>> class Elem x l
>> (instances for Elem so that Elem x l iff x is an element of the list l)
>>
>> Now I want:
>>
>>> type family Insert x s :: *
>>
>> Insert x s = s 		forall (x, s) with (Elem x s)
>> Insert x s = Cons x s 	for all other (x, s).
>>
>>
>> Thanks a lot!
>>
>> Steffen
>>
>>
>> [1] http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25832#a25832
>> [2] Kiselyov, Peyton-Jones, Shan: "Fun with type functions"
>>
>> http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/fun-with-type-funs/typefun.pdf
>> [3] I rewrote this algorithm using type families instead of fundeps:
>>
>> http://www.haskell.org/haskellwiki/Type_arithmetic#An_Advanced_Example_:_Type-Level_Quicksort
>> _______________________________________________
>> 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