[Haskell-cafe] in-equality type constraint?

[Steffen Schuldenzucker]

On 07/17/2010 03:50 AM, Gábor Lehel wrote:
> Does "TypeEq a c HFalse" imply proof of inequality, or unprovability
> of equality?

Shouldn't these two be equivalent for types?

> 
> On Sat, Jul 17, 2010 at 2:32 AM, Steffen Schuldenzucker
> <sschuldenzucker at uni-bonn.de> wrote:
>> On 07/17/2010 01:08 AM, Paul L wrote:
>>> Does anybody know why the type families only supports equality test
>>> like a ~ b, but not its negation?
>>>
>>
>> This has annoyed me, too. However, HList provides something quite similar,
>> namely the TypeEq[1] fundep-ed class which will answer type-equality with a
>> type-level boolean. (this is actually more powerful than a simple constraint,
>> because it allows us to introduce type-level conditionals)
>>
>> To turn it into a predicate, you can use something like
>>
>> (disclaimer: untested)
>>
>>> class C a b c where  -- ...
>>>
>>> -- for some reason, we can provide an instance C a b [c] *except* for
>>> -- a ~ c.
>>> instance (TypeEq a c x, x ~ HFalse) => a b [c] where  -- ...
>>
>> Best regards,
>>
>> Steffen
>>
>> [1]
>> http://hackage.haskell.org/packages/archive/HList/0.2.3/doc/html/Data-HList-FakePrelude.html#t%3ATypeEq
>> (Note that for it to work over all types, you have to import one of the
>> Data.HList.TypeEqGeneric{1,2} modules)
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
> 
> 
>