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.''