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 rocon...@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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe