[Haskell-cafe] Serialization of (a -> b) and IO a

[roconnor at theorem.ca]

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