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.d...@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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
