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/