Dan Doel dan.doel at gmail.com
Tue Aug 25 18:39:06 EDT 2009

```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
>
> 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
```