Hi Dan, thanks for the great reply! Some thoughts/questions follow.
On Tue, Aug 25, 2009 at 3:39 PM, Dan Doel
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