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

[Conor McBride]

Hi all

Interesting stuff. Thanks for this.

On 26 Aug 2009, at 03:45, Ryan Ingram wrote:

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

I think that's close enough to make "uninhabited" a useful
shorthand.

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

Something of the sort has certainly been suggested before. At
the very least, we should have empty case expressions, with at
least a warning generated when there is a constructor case
apparently possible.

[..]

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

I think it's likely to be quite tricky, but you might be able
to minimize the burden by adapting an old trick (see my thesis,
or "Eliminating Dependent Pattern Matching" by Goguen, McBride,
McKinna, or "A Few Constructions on Constructors" by the same
authors).

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

Perhaps it's not exactly what you want, but check this out. I've
used SHE, but I'll supply the translation so you know there's no
cheating.

 > {-# OPTIONS_GHC -F -pgmF she #-}
 > {-# LANGUAGE GADTs, KindSignatures, TypeOperators, TypeFamilies,  
FlexibleContexts,
 >     MultiParamTypeClasses, UndecidableInstances, RankNTypes,
 >     EmptyDataDecls #-}

 > module NoConfusion where

Some type theorists call the fact that constructors are injective
and disjoint the "no confusion" property, and the fact (?) that
they cover the datatype the "no junk" property. In Haskell, junk
there is, but there is strictly no junk.

 > import ShePrelude

 > data Nat :: * where
 >   Z :: Nat
 >   S :: Nat -> Nat
 >   deriving SheSingleton

The "deriving SheSingleton" bit makes the preprocessor build the
singleton GADT for Nat. From ShePrelude we have

   type family SheSingleton ty :: * -> *

and from the above, we get

   data SheTyZ = SheTyZ
   data SheTyS x1 = SheTyS x1
   type instance SheSingleton (Nat) = SheSingNat
   data SheSingNat :: * -> * where
     SheWitZ :: SheSingNat  (SheTyZ)
     SheWitS :: forall  sha0. SheSingleton (Nat ) sha0 -> SheSingNat   
(SheTyS sha0)

Now, let's have

 > newtype Naught = Naught {naughtE :: forall a. a}

Thanks to Dave Menendez for suggesting this coding of
the empty type.

 > data EQ :: forall (a :: *). {a} -> {a} -> * where
 >   Refl :: EQ a a

It may look like I've given EQ a polykind, but after translation,
the forall vanishes and the {a}s become *s. My EQ is just the
usual thing in * -> * -> *.

OK, here's the trick I learned from Healf Goguen one day
in 1997. Define a type-level function which explains
the consequences of knowing that two numbers are equal.

 > type family WhatNatEQProves (m :: {Nat})(n :: {Nat}) :: *
 > type instance WhatNatEQProves {Z}    {Z}    = ()
 > type instance WhatNatEQProves {Z}    {S n}  = Naught
 > type instance WhatNatEQProves {S m}  {Z}    = Naught
 > type instance WhatNatEQProves {S m}  {S n}  = EQ m n

Those type-level {Z} and {S n} guys just translate to
SheTyZ and (SheTyS n), respectively.

Now, here's the proof I learned from James McKinna, ten
minutes later.

 > noConf :: pi (m :: Nat). pi (n :: Nat). EQ m n -> WhatNatEQProves m n
 > noConf m n Refl = noConfDiag m

 > noConfDiag :: pi (n :: Nat). WhatNatEQProves n n
 > noConfDiag {Z}   = ()
 > noConfDiag {S n} = Refl

This pi (n :: Nat). ... is translated to

   forall n. SheSingleton Nat n -> ...

which computes to

   forall n. SheSingNat n -> ...

The expression-level {Z} and {S n} translate to
SheWitZ and (SheWitS n), accessing the singleton family.
Preprocessed, we get

   noConf :: forall m . SheSingleton ( Nat) m ->  forall n .  
SheSingleton ( Nat) n ->  EQ m n -> WhatNatEQProves m n
   noConf m n Refl = noConfDiag m

   noConfDiag :: forall n . SheSingleton ( Nat) n ->  WhatNatEQProves  
n n
   noConfDiag (SheWitZ)   = ()
   noConfDiag (SheWitS n) = Refl

James's cunning idea was to match on the equation first,
so that we need only consider the diagonal cases where
there is genuine work to do.

If this looks like a nuisance, compared to exploiting
unification on types, it is! It's how I showed that the
type-unification approach to pattern matching with GADTs
could be explained in terms of case analysis operators
like the ones Ryan likes to define.

So yes, it would be nice to have a neater way to refute
falsehood which says "this really can't happen" rather
than "this merely shouldn't happen". But this is not an
example which necessitates that feature.

All the best

Conor