[Haskell-cafe] Is it possible to prove type *non*-equality in Haskell?

[Ryan Ingram]

Hi Dan, thanks for the great reply!  Some thoughts/questions follow.

On Tue, Aug 25, 2009 at 3:39 PM, Dan Doel<dan.doel at gmail.com> wrote:
> Well, this isn't surprising; you wouldn't have it even in a more rigorous
> proof environment. Instead, you'd have to make the return type something like
>
>  Either (a == b) (a /= b)

Yes, and as you see I immediately headed in that direction :)

>> We know by parametricity that "contradiction n p" isn't inhabited as
>> its type is (forall a. a)
>
> But in Haskell, we know that it _is_ inhabited, because every type is
> inhabited by bottom. And one way to access this element is with undefined.

Of course.  But it is uninhabited in the sense that if you case
analyze on it, you're guaranteed not to reach the RHS of the case.
Which is as close to "uninhabited" as you get in Haskell.

> Well, matching against TEq is not going to work. The way you do this in Agda,
> for instance, is:
>
>  notZeqS :: forall n -> Not (TEq Z (S n))
>  notZeqS = Contr (\())

Yes, I had seen Agda's notation for this and I think it is quite
elegant.  Perhaps {} as a pattern in Haskell as an extension?  I'm
happy if it desugars into (\x -> x `seq` undefined) after the
typechecker proves that x is uninhabited except by _|_.  (This
guarantees that "undefined" never gets evaluated and any
exception/infinite loop happens inside of x.)

In fact, I would be happy if there was a way to localize the call to
"error" to a single location, which could then be the center of a
trusted kernel of logic functions for inequality.  But right now it
seems that I need to make a separate "notEq" for each pair of concrete
types, which isn't really acceptable to me.

Can you think of any way to do so?

Basically what I want is this function:
   notEq :: (compiler can prove a ~ b is unsound) => Not (TEq a b)

Sadly, I think you are right that there isn't a way to write this in
current GHC.

  -- ryan