[Haskell-cafe] Safe lists with GADT's

[oleg at pobox.com]

Stefan O'Rear wrote:
> Personally I like the GADT approach best since it is very flexible and
> convienient.  I have never used a purpose-build computer proof system,
> but (modulo _|_) it took me less than 10 minutes to answer
> LoganCapaldo (on #haskell)'s challenge to proof that + was commutative
> ( http://hpaste.org/522 )

I'm afraid it may be premature to call this a proof. Here's your code

> data S x
> data Z
>
> data Add :: * -> * -> * -> * where
>   AddZZ :: Add Z Z Z
>   AddS1 :: !(Add x y z) -> Add (S x) y (S z)
>   AddS2 :: !(Add x y z) -> Add x (S y) (S z)
>
> add_is_commutatative :: Add a b c -> Add b a c
> add_is_commutatative (AddZZ) = AddZZ
> add_is_commutatative (AddS1 a) = AddS2 (add_is_commutatative a)
> add_is_commutatative (AddS2 a) = AddS1 (add_is_commutatative a)


First of all, where is the coverage proof? Given two numbers, S (S Z)
and S Z, how to find their sum using the above code? Someone needs to
construct the sequence of Adds, _at run-time_! But where is the proof
that the sequence of Add applications expresses all possible ways of
computing the sum, and each possible sum can be represented as a
sequence of Adds? One may say -- this is so trivial; to which I reply
that the original question was trivial as well. If we talk about the
formal _proof_, then let's do it rigorously and formally all the way.

Also, we can write
> main = let x = AddS1 (undefined::Add Z Z (S Z)) in print "OK"
> main2 = let x = add_is_commutatative (undefined::Add Z Z (S Z)) in print "OK"

and the evaluation of 'main' and main2 prints OK. Thus we need to do forcing
_all_ the way. But what if we forget some forcing? Incidentally, this
is exactly what happened: add_is_commutatative should have been
strict. But the code above misses the strictness annotation and still
it compiles and seems to work -- and gives one a reason to call it a
proof despite the deficiency. I'm afraid I have little trust in the
system that permits such lapses.

>  but (modulo _|_)
That is quite an unsatisfactory disclaimer! From the CH point of view,
Haskell is inconsistent as every type is populated. Showing that a
function is total is precisely demonstrating that the function is the proof
of its type. So, showing the absence of bottoms is precisely making
the proof!

The problem with GADTs and other run-time based evidence is just
that: _run-time_ based evidence and pattern-matching. In a non-strict
system, checking that the evidence is really present is the problem on
and of itself. BTW, Omega, Dependent ML and a few other systems with
GADTs are strict.