in-equality type constraint?

Paul L

16 Jul 2010 16 Jul '10

7:08 p.m.

Does anybody know why the type families only supports equality test like a ~ b, but not its negation? -- Regards, Paul Liu Yale Haskell Group http://www.haskell.org/yale

Show replies by date

I was wondering this. I was recently able to write some code for negation of type equality, using the encoding "Not p" == "p -> forall a. a" But it doesn't generalize; you need to create a witness of inequality for every pair of types you care about. {-# LANGUAGE RankNTypes, TypeFamillies, ExistentialQuantification #-} module NotEq where data TypeEqual a b = (a ~ b) => Refl newtype Void = Void { voidElim :: forall a. a } type Not p = (p -> Void) data family IntVsBool a newtype instance IntVsBool Int = OK () newtype instance IntVsBool Bool = NotOK Void liftEq :: TypeEqual a b -> TypeEqual (f a) (f b) liftEq Refl = Refl cast :: TypeEqual a b -> a -> b cast Refl = id int_neq_bool :: Not (TypeEqual Int Bool) int_neq_bool = \int_eq_bool -> case (cast (liftEq int_eq_bool) (OK ())) of (NotOK v) -> v On Fri, Jul 16, 2010 at 4:08 PM, Paul L wrote:

...

Does anybody know why the type families only supports equality test like a ~ b, but not its negation?

-- Regards, Paul Liu

Yale Haskell Group http://www.haskell.org/yale _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Ivan Lazar Miljenovic

8:12 p.m.

Paul L writes:

...

Does anybody know why the type families only supports equality test like a ~ b, but not its negation?

At a guess, solely because no-one has implemented such functionality. -- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com IvanMiljenovic.wordpress.com

Steffen Schuldenzucker

8:32 p.m.

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-... (Note that for it to work over all types, you have to import one of the Data.HList.TypeEqGeneric{1,2} modules)

Paul L

9:28 p.m.

HList certainly provides an alternative. But given the use of UndecidableInstances and OverlappingInstances, I was hoping that type families could come a little cleaner. Or does it not matter? On Fri, Jul 16, 2010 at 8:32 PM, Steffen Schuldenzucker 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-... (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

-- Regards, Paul Liu Yale Haskell Group http://www.haskell.org/yale

Gábor Lehel

9:50 p.m.

Does "TypeEq a c HFalse" imply proof of inequality, or unprovability of equality? On Sat, Jul 17, 2010 at 2:32 AM, Steffen Schuldenzucker 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-... (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

-- Work is punishment for failing to procrastinate effectively.

Steffen Schuldenzucker

17 Jul 17 Jul

3:35 a.m.

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 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-... (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

Christopher Lane Hinson

16 Jul 16 Jul

10:29 p.m.

On Fri, 16 Jul 2010, Paul L wrote:

...

Does anybody know why the type families only supports equality test like a ~ b, but not its negation?

I would suggest that type equality is actually used for type inference, whereas proof of type inequality would have no consequence (that I can think of) for the compiler. Friendly, --Lane

wren ng thornton

17 Jul 17 Jul

3:14 a.m.

Christopher Lane Hinson wrote:

...

On Fri, 16 Jul 2010, Paul L wrote:

...
Does anybody know why the type families only supports equality test like a ~ b, but not its negation?

I would suggest that type equality is actually used for type inference, whereas proof of type inequality would have no consequence (that I can think of) for the compiler.

Also, it's a lot easier to solve a system of constraints when you only have positive constraints. Adding negative constraints greatly complicates the solver. In many cases it's still doable, though the structure of types might pose some additional challenges above the usual ones. (And they're usually called "disequality" constraints, since inequalities are only interesting when you have subtyping.) -- Live well, ~wren

5424

Age (days ago)

5425

Last active (days ago)

List overview

Download

8 comments

7 participants

participants (7)

Christopher Lane Hinson
Gábor Lehel
Ivan Lazar Miljenovic
Paul L
Ryan Ingram
Steffen Schuldenzucker
wren ng thornton