Monday, March 2, 2015

New Draft: Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism and Indexed Types

Together with Joshua Dunfield, I have a new draft on bidirectional type inference to announce:

Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism and Indexed Types

Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its scalability, its error reporting, and its ease of implementation. Following principles from proof theory, bidirectional typing can be applied to many type constructs. The principles underlying a bidirectional approach to indexed types (generalized algebraic datatypes) are less clear. Building on proof-theoretic treatments of equality, we give a declarative specification of typing based on focalization. This approach permits declarative rules for coverage of pattern matching, as well as support for first-class existential types using a focalized subtyping judgment. We use refinement types to avoid explicitly passing equality proofs in our term syntax, making our calculus close to languages such as Haskell and OCaml. An explicit rule deduces when a type is principal, leading to reliable substitution principles for a rich type system with significant type inference.

We also give a set of algorithmic typing rules, and prove that it is sound and complete with respect to the declarative system. The proof requires a number of technical innovations, including proving soundness and completeness in a mutually-recursive fashion.

If you are very interested in the details, we have a long (153 pages!) technical report with all of the proofs.

Don't be put off by the proofs, though -- the algorithmic type system is only modestly more complex than our earlier paper on bidirectional typechecking, and this go-around we add a lot of new features, such as intersection types, existential types, GADT-style equality constraints, and a full account of how to do pattern matching (including coverage checking) with all of these features.

Logically speaking, the punchline of the paper is that proof theory knows of two formulations of equality -- the Martin-Lof identity type, and the Girard/Schroeder-Heister equality. (Hilariously, these two notions of equality are not the same.) Furthermore, GADTs work exactly like the Girard/Schroeder-Heister equality. Everything things works uncannily well, and our rules (even the algorithmic ones) are much simpler than many of the rules you'll find in the literature.

Thursday, February 26, 2015

Midlands Graduate School 2015

Registration for the Midlands Graduate School is open! I'll be lecturing again this year on functional reactive programming, and am very much looking forward to meeting the participants.

Overview

The Midlands Graduate School in the Foundations of Computing Science (MGS) was established in 1999 as a collaboration between researchers at the Universities of Birmingham, Leicester, Nottingham, and later Sheffield. It has two main goals: to equip PhD students with a sound basis for their research by deepening their knowledge on the mathematical and conceptual foundations of computing; and to provide a platform for making contacts with established researchers in the field and with their peers who are at a similar stage in their research careers.

This year's MGS is hosted by the Department of Computer Science at the University of Sheffield. It will start on April 07 and finish on April 11.

Information about previous events can be found at the MGS web site.

Programme

MGS 2015 consists of nine courses, each with four or five hours of lectures and exercise sessions. Three of the courses are introductory or core; they should be taken by all participants. The other courses are more advanced or specialised. Participants may select them depending on their interests.

This year the invited lectures will be given by Prof Jeremy Gibbons, Oxford.

In addition there will be early evening sessions in which participants can briefly present and discuss their own research.

Core Courses

Category Theory Roy Crole, Leicester
Typed Lambda Calculus Paul Blain Levy, Birmingham
Patterns in Functional Programming Jeremy Gibbons, Oxford

Advanced Courses

Homotopy Type Theory Thorsten Altenkirch, Nottingham
Infinite Data Structures Venanzio Capretta, Nottingham
Security Protocol Verification Eike Ritter, Birmingham
Functional Reactive Programming Neelakantan Krishnaswami, Birmingham
Building Verification Tools with Isabelle Georg Struth, Sheffield

More information about the course schedule will be given shortly.



Registration

The registration deadline for MGS 2015 is Monday March 16. The registration fee is £460.

This fee includes 5 nights of accommodation and breakfasts at Hotel Ibis in Sheffield (from Monday April 06 evening to Saturday April 11 morning) as well as lunches, coffee breaks and the conference dinner.

A reduced fee without accommodation is available on request.

Participants need to register through the University of Sheffield Online Store. Payment is by debit or credit card.

Travel

MGS 2015 takes place in the Sir Frederick Mappin Building of the University of Sheffield, which is located on Mappin Street. Information on traveling to Sheffield and finding the Mappin Building is given here. A schedule of lectures and details about the lecture halls will be announced shortly.

Accommodation for MGS 2015 is at Hotel Ibis in the city centre of Sheffield.

The city centre of Sheffield is very compact. It takes about 10 minutes to walk from the train station to Hotel Ibis and about 20 min from the train station or from Hotel Ibis to Mappin Building.

There are many restaurants and pubs in the near vicinity of Mappin Building around Division Street and West Street. More restaurants can be found in the Hunter's Bar area of Sheffield along Ecclesall Road, or along London Road.

Organisation

Georg Struth (G.Struth@dcs.shef.ac.uk)

Friday, December 12, 2014

Garbage collection and purity

One of my favorite things in language design is when a high-level language feature lets you change your low-level runtime system in interesting ways. In this post, I'll talk about one such idea, which I probably won't have the time to work out in detail any time soon, but which is pretty enough that I want to offer it to the interweb.

In 2004, David Bacon, Perry Cheng, and V.T. Rajan published their paper A Unified Theory of Garbage Collection, which showed that tracing collectors and reference counting were the two extreme ends of a spectrum of memory management strategies.

Consider Cheney's two-space collector. When performing a garbage collection, it will start with the root objects, copy them from old-space to new-space, and then recursively traverse the objects reachable from the roots, moving them from old-space to new-space as it goes.

An important property of Cheney's algorithm is that it never touches any object that needs to be freed; it only follows pointers from live objects to live objects.

On the other hand, consider the naive reference counting algorithm. When the reference count on an object goes to zero, the algorithm will decrement the reference counts of everything the object points to, recursively invoke itself on all of the objects whose reference counts also went to zero, and then free the original object.

Bacon, Cheng and Rajan observed that this reference counting algorithm has the opposite property as Cheney's algorithm -- it only traverses dead objects, and never follows a pointer inside a live object.

When object lifetimes are very short, tracing collectors beat reference counting, because very few objects will be live at gc time, and tracing only follows live objects. On the other hand, when object lifetimes are very long, reference counting wins, because very few objects are dead at each collection, and reference counting only follows dead objects.

So (a) the best memory management strategy to use depends on the lifetime of the object in question, and (b) every memory management algorithm can be seen as a hybrid of reference counting and tracing, based on which objects it chooses to follow.

In 2003, Stephen Blackburn and Kathryn Mckinley gave an incredibly slick application of this idea in their paper Ulterior Reference Counting. (Yes, the chronology is backwards: research is asynchronous.)

Most production garbage collectors are based on what is called "the generational hypothesis". This says that in typical programs, most objects have a very short lifetime, and only a few have a long lifetime. So it's a good idea to allocate objects into a region of memory called "the nursery", and when it fills up, to copy live objects out of it. Because of the generational hypothesis, most objects in the nursery will be dead, and so collecting the nursery will be very fast.

Blackburn and McKinley observed that the generational hypothesis also implies that if an object survives a young collection, it's likely to live for a very long time. So in their algorithm, they have a nursery as usual for tracing collectors. But for objects copied out of the nursery, they use reference counting. That is, for objects likely to have a short lifetime, they use tracing, and for objects likely to have a long lifetime, they use reference counting!

Now, if you're a functional programmer, the mere mention of reference counting very likely rings some alarm bells --- what about cycles? Reference counting is, after all, notorious for its inability to handle cyclic data.

Blackburn and McKinley handle this issue with a backup mark-and-sweep algorithm that is periodically run on the old generation. But wouldn't it be nice if we could just know that there isn't any cyclic data in the heap? Then we could do away with the backup collector, and implement a very simple "trace young, reference count old" collector.

Surprisingly, this is possible! If we program in a pure functional language, then under the usual implementation strategies, there will never be nontrivial cycles in the heap. The only way a cyclic reference could occur is in the closure of a recursive function definition, and we can simply mark such recursive pointers as something the gc doesn't need to follow.

So a very high-level property (purity) seems to imply something about our low-level runtime (the gc strategy strategy)! Proving this works (and benchmarking it) is something I don't have room on my plate for, but it's something I wish I could do...

Tuesday, December 9, 2014

Quote of the Day

From the introduction to Jean-Louis Krivine's paper, Realizability Algebras: A Program to Well-Order $\mathbb{R}$:
Indeed, when we realize usual axioms of mathematics, we need to introduce, one after the other, the very standard tools in system programming: for the law of Peirce, these are continuations (particularly useful for exceptions); for the axiom of dependent choice, these are the clock and the process numbering; for the ultrafilter axiom and the well ordering of $\mathbb{R}$, these are no less than read and write instructions on a global memory, in other words assignment.
A better example of consilience I cannot imagine!

Thursday, November 13, 2014

Curry-Howard for GUIs: Or, User Interfaces via Linear Temporal, Classical Linear Logic

Together with Jennifer Paykin and Steve Zdancewic, we have written a short note about the next phase of the long project to make GUI programming intellectually manageable.

Essentially, the idea is that the natural language of graphical user interfaces is $\pi$-calculus, typed using classical linear logic (plus some temporal modalities). Furthermore, we think that the implementation strategy of callbacks and event loops can be understood in terms of Paul-Andre Mellies' tensorial logic. So we think we can:

  1. Explain how there are secretly beautiful logical abstractions inside the apparent horror of windowing toolkits;
  2. Illustrate how to write higher-order programs which automatically maintain complex imperative invariants, and
  3. Write some Javascript programs which we think are actually $\pi$-calculus terms in disguise.
You can download the draft here. If you want to read something with more theorems than this note, I'd suggest looking at Jennifer and Steve's paper about their Linear/Producer/Consumer calculus for CLL.

Tuesday, November 4, 2014

Integrating Linear and Dependent Types at POPL 2015

I'm very happy to announce that Integrating Linear and Dependent Types will appear at POPL 2015! The link above goes to the final version, which (at the behest of the reviewers) has been significantly expanded from the original submission. (Added up, the total length of the reviews was almost half the length of the submission, which says something about the degree of care taken in the process.)

Also, Jeremy Yallop has put together a web page with links to many of the POPL 2015 papers. Some of the freely available ones (as of this writing) which catch my eye are:

  • Formal verification of a C static analyzer, by Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy and David Pichardie

    Astrée is one of the big success stories in verification. Apparently they are building a provably correct(!) version.

  • Space-Efficient Manifest Contracts, by Michael Greenberg

    One of the big difficulties in applying contract checking to functional programming is that it breaks tail call optimization. This paper says that you can do it without breaking TCO, which is (a) a real breakthrough, and (b) probably has all kinds of applications.

  • Functors are type refinement systems, by Paul-André Melliès and Noam Zeilberger

    I knew fibrations were important for characterizing inductive definitions in type theory, parametricity, and the semantics of dependent types. Apparently they are also important for characterizing refinement types.

  • Programming up to Congruence, by Vilhelm Sjöberg and Stephanie Weirich

    This is a dependent type theory which works up the congruence closure of the equality hypotheses in the context, rather than using a judgmental equality. The treatment of equality is the central problem in the design of dependently typed languages, so it's nice to see exploration of the design space. (This approach reminds me a bit of the Girard/Schroeder-Heister equality rule, which semi-secretly underpins GADTs.)

Monday, October 20, 2014

Focusing is not Call-by-Push-Value

Ever since I learned about them, I've thought of call-by-push-value and focusing (aka polarization) as essentially two different views of the same problem: they both give a fine-grained decomposition of higher-order effectful programs which permits preserving the full βη-theory of the language.

Until this morning, I had thought that the differences were merely cosmetic, with CBPV arising from Paul Levy's analysis of the relationship between denotational semantics and operational semantics, and focusing arising an analysis of the relationship between operational semantics and proof theory (a lot of people have looked at this, but I learned about it from Noam Zeilberger). Both systems decompose a Moggi-style computational monad into a pair of adjoint operators, which mediate between values and computations (in CBPV) and positive and negative types (in focusing). So I thought this meant that “value type” and “positive type” were synonyms, as were “computation type” and “negative type”.

This morning, I realized I was wrong! Focusing and call-by-push-value make precisely the opposite choices in their treatment of variables! To understand this point, let's first recall the syntax of types for a call-by-push-value (on top) and a polarized (on bottom) calculus.

\begin{mathpar}
\begin{array}{llcl}
\mbox{Value Types} &
X,Y,Z & ::= & \Val{A} \bnfalt 0 \bnfalt X + Y \bnfalt 1 \bnfalt X \times Y \\
\mbox{Computation Types} & 
A,B,C & ::= & \F{X} \bnfalt X \to A \bnfalt \top \bnfalt X \With Y \\[1em]

\mbox{Positive Types} & 
P,Q & ::= & \Down{N} \bnfalt 0 \bnfalt P + Q \bnfalt 1 \bnfalt P \times Q \\
\mbox{Computation Types} & 
M,N & ::= & \Up{P} \bnfalt P \to N \bnfalt \top \bnfalt M \With N \\
\end{array}
\end{mathpar}

At first glance, these two grammars look identical, save only for the renamings $\Val{-} \iff \Down{-}$ and $\F{-} \iff \Up{-}$. But this is misleading! If they are actually the same idea, the reason has to be much more subtle. The reason for this is that the typing judgements for these two systems are actually quite different.

In call-by-push-value, the idea is that $\Val{A}$ is a functor which is left adjoint to $\F{X}$. As a result, values are interpreted in a category of values $\ValueOp$, and computations are interpreted in a category of computations $\CompOp$. The adjunction between values and computations means that the hom-set $\VHom{X}{\Val{A}}$ is ismorphic to the hom-set $\CHom{\F{X}}{A}$. This adjunction gives rise to the two basic judgement forms of call-by-push-value, the value judgement $\judge{\Gamma}{v}{X}$ and the computation judgement $\judgec{\Gamma}{t}{A}$. The idea is that $\interp{\judgev{\Gamma}{v}{X}} \in \VHom{\Gamma}{X}$ and $\interp{\judgec{\Gamma}{t}{A}} \in \CHom{\F{\Gamma}}{A}$.

The key bit is in the interpretation of contexts in computations, so let me highlight that:

$\interp{\judgec{\Gamma}{t}{A}} \in \CHom{\F{\Gamma}}{A}$

Note that we interpret contexts as $\F{\Gamma}$, and so this says that variables refer to values.

However, in a polarized type theory, we observe that positive types are “left-invertible”, and negative types are “right-invertible”. In proof theory, a rule is invertibile when the conclusion implies the premise. For example, the right rule for implication introduction in intuitionistic logic reads

\begin{mathpar}
\inferrule*[]
          {\judgend{\Gamma, S}{T}}
          {\judgend{\Gamma}{S \to T}}
\end{mathpar}

This is invertible because you can prove, as a theorem, that

\begin{mathpar}
\inferrule*[]
          {\judgend{\Gamma}{S \to T}}
          {\judgend{\Gamma, S}{T}}
\end{mathpar}

is an admissible rule of the system. Similarly, sums have a left rule:

\begin{mathpar}
\inferrule*[]
          {\judgend{\Gamma, S}{Q} \\ \judgend{\Gamma, T}{Q}}
          {\judgend{\Gamma, S + T}{Q}}
\end{mathpar}

such that the following two rules are admissible:

\begin{mathpar}
\inferrule*[]
          {\judgend{\Gamma, S + T}{Q}}
          {\judgend{\Gamma, S}{Q}}

\and

\inferrule*[]
          {\judgend{\Gamma, S + T}{Q}}
          {\judgend{\Gamma, T}{Q}}
\end{mathpar}

The key idea behind polarization is that one should specify the calculus modulo the invertible rules. That is, the judgement on the right should fundamentally be a judgement that a term has a positive type, and the hypotheses in the context should be negative. That is, the two primary judgements of a polarized system are the positive introduction judgement

$\judge{\Gamma}{v}{P}$

which explains how introductions for positive types work, and the negative elimination (or spine judgement)

$\spine{\Gamma}{s}{N}{P}$

which explains how eliminations for negative types work. The eliminations for positive types are derived and the introductions for negative types are derived judgements (which end up being rules for pattern matching and lambda-abstractions) which make cut-elimination hold, plus a few book-keeping rules to hook these two judgements together. The critical point is that the grammar for $\Gamma$ consists of negative types:

$\Gamma ::= \cdot \bnfalt \Gamma, x:N$

This is because positive types are (by definition) left-invertible, and so there is no reason to permit them to appear as hypotheses. As a result, the context clearly has a very different character than in call-by-push-value.

I don't have a punchline for this post, in the sense of “and therefore the following weird things happen as a consequence”, but I would be astonished if there weren't some interesting consequences! Both focalization and call-by-push-value teach us that it pays large dividends to pay attention to the fine structure of computation, and it's really surprising that they are apparently not looking at the same fine structure, despite apparently arising from the same dichotomy at the type level.