Michael Dummett

The British philosopher Michael Dummett's books The Logical Basis of Metaphysics and Frege: Philosophy of Language were some of the most useful books I read during my degree. His analysis of Frege's sense-reference distinction has been very helpful to my understanding of dependent type theory, and his explanation of intuitionism was quite helpful in understanding the relationship between the structural-proof-theoretic view of types and the realizability interpretation of types.

So I was disappointed to learn that he died last week, but pleased  to read the reminiscences of him by his colleagues posted on the New York Times.

Adding Equations to System F, at ESOP 2012

Our paper on adding equations to system F was accepted to ESOP 2012!

The reviewers suggested rather a lot of improvements to the paper, so I'm taking the draft down while we incorporate their suggestions. It will go up again in a few weeks, after the revisions are done, and undoubtedly in a much-improved state. 

Updata

The final version of our POPL paper on space-bounded FRP is available now -- we bought two extra pages from the ACM, and used them to add a lot more detail to the examples. With luck the paper will be a lot clearer now.

Also, Bob Atkey has a new blog post on using delay operators to model guarded definitions in type theory. He takes advantage of the fact that delay is a strong lax monoidal functor (with respect to the monoidal structure of products) to use the syntax of applicative functors.

This is a very elegant way of embedding these things into Haskell. Unfortunately, I have never liked the typing rules for the idiom syntax, since they don't work solely on the outermost type constructor. This means type-theoretic properties like normalization are messier to prove. (Bob evades this problem with semantic techniques, though.)


All his other posts are very good, too.

Adding Equations to System F

Nick and I have a new draft out, on adding types for term-level equations to System F. Contrary to the experience of dependent types, this is not a very hairy extension -- in fact, I would not even hesitate to call it simple.

However, it does open the door to all sorts of exciting things, such as many peoples' long-standing goal of putting semantic properties of modules into the module interfaces. This is good for documentation, and also (I would hope) good for compilers --- imagine Haskell, if the Monad typeclass definition also told you (and ghc!)  all the equational rewriting that it was supposed to do.

Higher-Order Functional Reactive Programming in Bounded Space

I just learned that our (with Nick Benton and Jan Hoffmann) paper, Higher-Order Functional Reactive Programming in Bounded Space, was accepted for publication at POPL 2012!

I am very happy with this work, since it resolves some of the thorniest problems in FRP (memory usage and space leaks) without giving up the highly expressive higher-order abstractions that makes FRP attractive in the first place.

A technical surprise in this work is that this stuff is the first place I've seen where the magic wand of separation logic is actually essential. The denotational model in this paper is a variation on Martin Hofmann's length space model, which forms a doubly-closed category modelling bunched implications. In this paper, we needed both function spaces: we needed the linear function space to control allocation, and we needed the ordinary function space to make use of sharing.

It would be interesting to see if there are ways to transport some of these ideas back to Hoare-style separation logic to find some interesting new invariants.

Radical predicativism

This isn't really on-topic for this blog, but I can't resist posting this: the Princeton mathematician Edward Nelson claims to have found an inconsistency in arithmetic! On the FOM mailing list, he posted:

I am writing up a proof that Peano arithmetic (P), and even a small fragment of primitive-recursive arithmetic (PRA), are inconsistent. This is posted as a Work in Progress at http://www.math.princeton.edu/~nelson/books.html

A short outline of the book is at:

http://www.math.princeton.edu/~nelson/papers/outline.pdf

The outline begins with a formalist critique of finitism, making the case that there are tacit infinitary assumptions underlying finitism. Then the outline describes how inconsistency will be proved. It concludes with remarks on how to do modern mathematics within a consistent theory.

There's some discussion of this at The n-Category Cafe, including a brief (so far) discussion between Terry Tao and Nelson himself. Obviously, I expect a flaw will be found in his proof -- but I sure hope he's right! That would mean all of mathematics will be in need of revision.

Update: Nelson says that Tao has indeed found a hole in the proof. Exponentiation remains total, for now.

The most surprising paper at ICFP

I was just at ICFP, which was very nice -- it was my first trip ever to Japan, and I found the people very friendly. (The cuisine, alas, is not so vegetarian-friendly, if you do not regard fish as a vegetable. But the people made up for it!) There were many excellent talks, but only one result which really shocked me:

Linearity and PCF: a semantic insight!, by Marco Gaboardi, Luca Paolini, and Mauro Piccolo.

Linearity is a multi-faceted and ubiquitous notion in the analysis and the development of programming language concepts. We study linearity in a denotational perspective by picking out programs that correspond to linear functions between coherence spaces.

We introduce a language, named SlPCF*, that increases the higher-order expressivity of a linear core of PCF by means of new operators related to exception handling and parallel evaluation. SlPCF* allows us to program all the finite elements of the model and, consequently, it entails a full abstraction result that makes the reasoning on the equivalence between programs simpler.

Denotational linearity provides also crucial information for the operational evaluation of programs. We formalize two evaluation machineries for the language. The first one is an abstract and concise operational semantics designed with the aim of explaining the new operators, and is based on an infinite-branching search of the evaluation space. The second one is more concrete and it prunes such a space, by exploiting the linear assumptions. This can also be regarded as a base for an implementation.

In this paper, the authors considered a really simple language based on coherence spaces, consisting of the flat coherence space of natural numbers and the linear function space. The nice thing about this model is that tokens of function spaces are just trees with natural numbers at the leaves, with branching determined by the parenthesization of the function type. This really shows off how concrete, simple, and easy-to-use coherence spaces are. Then they found the extension to PCF for which this model was fully abstract, as semanticists are prone to doing.

But: the additional operator and its semantics are really bizarre and ugly. I don't mean this as a criticism -- in fact it is exactly why I liked their paper so much! It implies that there are fundamental facts about linear types which we don't understand. I asked Marco Gaboardi about it after his talk, and he told me that he thinks the issue is that the properties of flat domains in coherence spaces are not well understood.

Anyway, this was a great paper, in a "heightening the contradictions" sort of way.