On Thu, 11 Nov 2010, Dan Doel wrote:
intensional equality: two values are provably equal if they evaluate to the
same normal form
extensional equality: this incorporates non-computational rules, like the
point-wise equality of functions.
Now, in a type theory where equality is intensional, I cannot prove:
(forall x. f x = g x) -> f = g
However, both these equalities (and others in between and on either side) are
*compatible*, in that I cannot disprove the above theorem in an intensional
theory.
What seq and serialize do is break from extensional equality, and allow us to
disprove the above (perhaps not for seq within a hypothetical theory, since
the invalidating case involves non-termination, but certainly for serialize).
And that's a big deal, because extensional equality is handy for the above
reasoning about programs.
As you are well aware in Coq, and in Agda we don't have an extensionality
axiom; however this is not a problem because we simply use setoid equality
to capture extenional reasoning and prove that in every specific case
where we want to use extensioanl reasoning it is sound to do so.
Now suppose I add the following consitent axiom to Coq:
Axiom Church-Turing :
forall f:Nat -> Nat, exists e:Nat, forall n:Nat, {e}(n) = f(n)
This well-studied axiom is effectively what serialize is realizing[1].
Now, have I broken my old Coq proofs by adding this axiom? No, of course
not, because it is a consistent axioms and my proofs didn't use it. My
proofs were alreay explicity proving that extentional substitution was
sound in those cases I was using it.
The same will be true for reasoning in Haskell. Before serialization we
knew that extensional substitution was sound, but after adding
serialization we are now obligated to prove in the individual cases that
extensional subsitution is sound and/or add extentionally preconditions to
our proofs. So no big deal; people have already been doing this in Coq
and Agda for years.
[1]Actaully the realizer for serialize is *weaker* that this axioms. The
realizer for serialize would be (Nat -> Nat) -> IO Nat instead of (Nat ->
Nat) -> Nat, so should have less impact that the Church-Turing axiom.
--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
