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

Is it possible to prove type non-equality in Haskell?

Ryan Ingram

25 Aug 2009 25 Aug '09

6:03 p.m.

Short version: How can I get from (Z ~ S n) to a useful contradiction? Type equality coercions[1] let us write proofs in Haskell that two types are equal:

...

{-# LANGUAGE GADTs, RankNTypes, TypeFamilies #-} {-# OPTIONS_GHC -Wall #-} module TEq where

...

data TEq a b = (a ~ b) => TEq

This provides all the expected properties for equality:

...

refl :: TEq a a refl = TEq symm :: TEq a b -> TEq b a symm TEq = TEq trans :: TEq a b -> TEq b c -> TEq a c trans TEq TEq = TEq

Here's an example use:

...

data Z = Z newtype S n = S n

...

data Nat a where Nz :: Nat Z Ns :: Nat x -> Nat (S x)

...

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

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? -- ryan [1] http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/

Show replies by date

Dan Doel

25 Aug 25 Aug

6:39 p.m.

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

Ryan Ingram

10:45 p.m.

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

Conor McBride

26 Aug 26 Aug

9:33 a.m.

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

5863

Age (days ago)

5864

Last active (days ago)

List overview

Download

3 comments

3 participants

participants (3)

Conor McBride
Dan Doel
Ryan Ingram

Ryan Ingram

Dan Doel

Ryan Ingram

Conor McBride

tags

participants (3)

Is it possible to prove type non-equality in Haskell?