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 > <sschuldenzuc...@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@haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> > > > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
