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

[Dan Doel]

On Tuesday 25 August 2009 6:03:31 pm Ryan Ingram wrote:
> > proveEq :: Nat a -> Nat b -> Maybe (TEq a b)
> > proveEq Nz Nz = return TEq
> > proveEq (Ns a) (Ns b) = do
> >     TEq <- proveEq a b
> >     return TEq
> > proveEq _ _ = Nothing
>
> But if you get "Nothing" back, there's no proof that the two types are
> in fact non-equal.

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)

> You can use "_|_ as negation":
> > newtype Not p = Contr { contradiction :: forall a. p -> a }
> >
> > nsymm :: Not (TEq a b) -> Not (TEq b a)
> > nsymm pf = Contr (contradiction pf . symm)
>
> 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.

> But I can't figure out a way to write this without "error":
> > notZeqS :: forall n. Not (TEq Z (S n))
> > notZeqS = Contr (\x -> x `seq` error "impossible")
>
> As a first step, I'd like to write this:
> > -- notZeqS = Contr (\TEq -> error "impossible")

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 (\())

Where () is the 'absurd pattern'. It's used to indicate that argument is 
expected to have an uninhabited type, and if Agda can prove that it is 
uninhabited, then a lambda expression like the above denotes the empty 
function.

But Haskell has no such animal. You could kind of adapt it to empty case 
expressions:

  notZeqS = Contr (\pf -> case pf of {})

And perhaps require that the type system can verify that the types of such 
cases are uninhabited except for bottom (although that isn't strictly 
necessary; you could leave it as simply desugaring to a catch-all call to 
error and it'd work), if that's even a feasible thing to do.

Currently, though, you'll get a parse error on }.

> but the compiler complains immediately about the pattern match being
> unsound: TEq.lhs:39:20:
>     Couldn't match expected type `S n' against inferred type `Z'
>     In the pattern: TEq
>     In the first argument of `Contr', namely
>         `(\ TEq -> error "impossible")'
>     In the expression: Contr (\ TEq -> error "impossible")
>
> Is there any way to use the obvious unsoundness we get from (Z ~ S n) to
> generate a contradiction?
>
> Ideally I'd like to be able to implement
> ] natEqDec :: Nat a -> Nat b -> Either (TEq a b) (Not (TEq a b))
>
> as follows:
> > predEq :: TEq (f a) (f b) -> TEq a b
> > predEq TEq = TEq
> >
> > natEqDec :: Nat a -> Nat b -> Either (TEq a b) (Not (TEq a b))
> > natEqDec Nz     Nz     = Left TEq
> > natEqDec (Ns a) (Ns b) = case natEqDec a b of
> >     Left TEq -> Left TEq
> >     Right pf -> Right $ Contr $ \eq -> contradiction pf (predEq eq)
> > natEqDec Nz     (Ns _) = Right notZeqS
> > natEqDec (Ns _) Nz     = Right (nsymm notZeqS)
>
> Which compiles successfully, but the "error" call in "notZeqS" is a
> big wart.  Is there a better implementation of "Not" that allows us to
> avoid this wart?

You could build more complex, positive proofs of inequality (having a 3-way 
decision between m < n, m == n and m > n might be a good one), but I don't 
think you'll find a notion of negation that avoids some sort of call to 
undefined in GHC as it currently stands.

-- Dan