[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