[Haskell-cafe] Is it possible to prove type *non*-equality in
Haskell?
Ryan Ingram
ryani.spam at gmail.com
Tue Aug 25 18:03:31 EDT 2009
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/
More information about the Haskell-Cafe
mailing list