Wadler's Blog

There are two threads on the homotopy type theory list that may be of interest if you take another pass over this paper:

https://groups.google.com/forum/#!topic/homotopytypetheory/o-cVRGFF-Ig

and

https://groups.google.com/forum/#!topic/homotopytypetheory/OzCQ6vrzAN0

On the latter, the place to begin reading is Streicher's message of January 15. I believe he address a common misconception, which your paper does not participate in, but nor does it directly challenge -- the idea that since all propositions may be given types, then we must associate all types with propositions. This leads to such silliness as Haskell users being introduced to Curry-Howard asking what the proposition is corresponding to the type of hGetLine. (Ok, sure, this is not entirely silly, but still..).

The former thread also points to a lacunae in your paper, but again one that you are perfectly within your rights to not address -- the unfortunate (in my mind) underplaying of the role of realizability with regards to the notion of "proofs as computations." This is in a sense not directly in the CH lineage the same way BHK is, but nonetheless, it was an important step in a similar direction. Of course your paper is not just a discourse on history, but is a work intended for education and exposition, so this may all be a bit besides the point.
 

@sclv: Thanks!

It is not clear to me where Kleene's work on realisability sits in the history. Is it simply a fleshing out of BHK, or did it make a more profound contribution?

Regarding 'Propositions as Types' vs 'Types as Propositions': if it is an isomorphism, then there should be correspondences both ways. In that sense, 'What is the proposition corresponding to Nat?' or 'What is the proposition corresponding to the type of hGetLine?' is not a completely silly question. The first might be answered in terms of the definition of Nat in F2, which equates naturals with an induction principle, the second might (partially) be answered by observing the correspondence between monads and one variant of modal logic.
 

I am not clear on all the details myself on kleene, which is why i would like you to write more about it in your paper :-)

my sense, however, is this. bhk says, in a sense, that we can read propositions as rules for abstract constructions in some compositional way. kleene's realizability says much more directly we can _construct_ models of propositions in a certain mathematical system, and a _realization_ of a proposition is _itself_ a constructive proof of that proposition. so i suppose bhk tells us in general a notion of the relationship of logics to objects, and realizability gives a concrete one.

but by giving a concrete one, it also opens a conceptual leap, in much the same way godel's use of numbers to correspond to propositions did. we can now "reflect" propositions back into our proof language and think about higher order quantification, even if crudely, etc. furthermore, it was stunning to me to learn about it because it is jarring to see all these fancy formulae "flattened" directly into the domain of just plain numbers.

bhk was suggestive but never went, to my knowledge, beyond a way of attempting to understand and justify intuitionist formulae. realizability very directly takes not only those formulae, but their proofs, and renders them as familiar mathematical objects. so now we not only have propositions having a mathematical meaning, but vanilla mathematical objects "secretly" having a proof-theoretic content.

on the 'isomorphism' issue -- yes in traditional CH we have a full isomorphism. but it is interesting to "open that up". my inspiration here is awodey and bauer's bracket types paper (http://math.andrej.com/data/bracket_types.pdf) which anticipates the notion of truncation in homotopy type theory, while using modalities in a very nice fashion. even in coq we distinguish between prop and set (aka type). in hott we get even more interesting questions, such as "what proposition corresponds to the type of the hypersphere?".

we could of course say that types are propositions by fiat, and if we don't have the right logical symbols to write this proposition, this is a failure of our logic.

but we can also say that we're using logic in the traditional sense, to talk about things that merely exist or do not, and "forget" about the extra structure (in this case higher structure, in other cases, effectful structure or the like). this other view is appealing to me, at least from the standpoint of pedagogy and clarity.

Furthermore, there certainly, are more things you can do with a mere proposition than an arbitrary type, because a mere proposition carries less information around with it. There's an analogy I can't quite pin down, but is promising nonetheless, with parametricity in this regard.
 

@sclv

Thanks for your further comments. I will acknowledge you in the paper if you tell me who you are.

I will consider how I can add a line or two about Kleene realisability to the paper. I agree it is part of the story.

Regarding the view that sometimes we have a structure other than an isomorphism, where all propositions are types but not conversely, such things certainly appear in the literature but I probably won't get into that level of complication in the paper.

An example of a non-isomorphic structure, perhaps touching on your intuitions about parametricity, appears in my paper 'The Girard-Reynolds Isomorphism', which the introduction makes clear is really about the Girard-Reynolds Projection-Embedding pair. See also Bernardy and Jansson's work on encoding the logic of one Pure Type System (PTS) into another PTS.