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

Dan Doel dan.doel at gmail.com
Fri Nov 12 21:05:09 EST 2010


It took me a bit to decide whether this was an adequate counter to my 
objection, but ultimately, I don't think it is. I'll try to explain as well as 
possible.

On Friday 12 November 2010 1:40:10 pm roconnor at theorem.ca wrote:
> 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 extensional reasoning it is sound to do so.

If we are talking about writing programs in a closed world, and proving things 
about said world, this is fine. But this is not always what we are doing in 
Haskell. For instance, if I am writing a library, am I justified in changing:

  f (g x) (g x)

to:

  let y = g x in f y y

without bumping the "semantics breaking change" version number? In a closed 
world, where I have proved that all the relevant code I have written admits 
extensionality, the answer is, "yes." But in an open world, where people are 
free to use serialize to inspect my implementations in pure code, the answer 
is, "no."

> Now suppose I add the following consistent axiom to Coq:
> 
> Axiom Church-Turing :
>    forall f:Nat -> Nat, exists e:Nat, forall n:Nat, {e}(n) = f(n)

So, your argument is, if I'm not mistaken, that intensional type theory can be 
consistently extended with this axiom. I believe this. In fact, I'd even be 
willing to accept that purely as an axiom, it might be consistent to add it to 
extensional type theory. However, this is not the whole story.

One question I have to ask is: how does this compute? In Agda, and I suspect 
Coq, axioms simply do not compute (and this is the reason I'd be willing to 
believe Church-Turing is consistent with an extensional theory). However, 
serialize *will* compute, and I expect it to compute like this:

  forall e:Nat. serialize {e} => e

And I can believe that even this is consistent with intensional type theory. 
In an intensional theory, I can imagine (Nat -> Nat) being interpreted not as 
a type of functions, but as a type of algorithms. There may be many algorithms 
that compute the same function, and Nat -> Nat contains them all. 
serialize/Church-Turing returns the source code of each one.

When we assert extensionality, though, Nat -> Nat can no longer be inhabited 
by mere algorithms, though. In an extensional theory, Nat -> Nat is a quotient 
of the set of algorithms. And then we have only a few options:

  1) serialize/Church-Turing violates the quotient
  2) serialize/Church-Turing computes extensional equality of algorithms, and
     chooses a single 'source code' representation for each equivalence class
  3) It is impossible for two different pieces of source code to compute the
     same function (so serialize {e} => e is valid because there is no e' /= e
     such that forall x. {e} x = {e'} x)
  *) ...

2 is, I think, impossible, and 3 is simply false, so the choice is 1, meaning 
that ITT + a Church-Turing that actually computes cannot be consistently 
extended with extensionality. And it is this that I care about, and what I was 
referring to in the mail you replied to:

  - Intensional type theory can be consistently extended to extensional type
    theory.
  - serialize is anti-extensional (similar to the way impredicative Set
    and injective type constructors are anti-classical).

And it is this consistent extension that I care about. And, going back to my 
library example, the reason to care about this is abstraction. I want clients 
of my library to program to the abstraction of my code as functions, not as 
algorithms/source code, because that allows me leeway to tweak the algorithms 
as I see fit, so long as they compute the same function.

And, for that matter, the compiler can do this kind of mucking around with 
algorithms. I think it's a big deal if, to enable optimization of a function, 
we have to prove that all code in our program treats it extensionally (I don't 
believe the compiler can do it, currently, barring serialize simply not being 
used; and say goodbye to separate compilation).

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

I have no problem with serialize :: (Nat -> Nat) -> IO Nat. The problem is 
with (Nat -> Nat) -> Nat. The former can respect the quotient in question via 
IO hand waving. Perhaps this distinction is frivolous, but it seems wrong to 
make the language in general anti-extensional when it could instead be put 
inside the sin bin. My quarrel is more with, "let's dump out the sin bin and 
just be careful."

-- Dan

[*] I have seen a paper about a type theory with quotients that has a 
function:

  choose : T / R -> T

such that:

  choose (squish x) => x

but it was meticulously designed to allow that in ways that I don't really 
remember, so I'm going to pretend it doesn't exist at the moment.


More information about the Haskell-Cafe mailing list