It’s an obvious but not often considered fact that if you erase all the terms from a valid construction in System F, you get a bunch of perfectly sensible types. (When you erase a Λ, you need to extend the context in which the types you expose will be judged.) Erasing the types is more likely to happen, yielding perfectly sensible terms which we might have some motivation to evaluate, but erasing the terms works, too. The thing about System F is that types and terms separate like oil and water: the context may build up term variables with λ and type variables with Λ, but when you’re making a type you can’t give a term variable, and when you’re making a term, you can’t give a type variable. Worlds apart. The separation of worlds means you can erase either terms or types without damaging the residue.
GCHQ read all my communications (hi, Richard!), but I’m not entitled to read theirs. Fortunately for me, I don’t need to know what they think in order to go about my business. Without the inward flow of unprivileged information, however, GHCQ would be able to monitor only one another, which might increase the availability of office space in Cheltenham. I hasten to add (in case Richard’s getting twitchy) that I am not proposing “Cheltenham erasure”, but the fact remains that my function depends in no way on the outflow of privileged information from GCHQ. We’re worlds apart, but there’s a directed information flow between those worlds.
Meanwhile, at GHC HQ, we’ve been trying to fight our way out of the mess caused by the separation of worlds in System F and its extensions: in each world, we find ourselves building avatars for things which live in the other, awkwardly simulating dependent types. We can’t just impose dependent types, because in their absence from the type world, the terms have learned to behave rather badly. What we can do, however, is install a shared world, for things which behave perfectly sensibly in types and at run time: information may flow from the shared world to both. During typechecking, we may have to run programs from the shared world, but we don’t need to run chaotic run-time-only code. Information does not flow downwards from the types-only world, so when generating run-time code, we can still erase everything we used to, leaving the shared and the run-time-only things.
Once you start to see systems in terms of information flow, it’s hard to stop. The question is really this: which communications of data are permitted by the notion of variable scope? Perhaps not all variables are in scope for all constructions. Note that if we prevent communication by being in scope, we may not have excluded explicit communication, (cost?-)modelled as an effect. Here’s a laundry list of possibilities and wheezes.
- stage We cut execution into stages. Values persist from earlier to later stages, but dependency is forbidden the other way around. Stages are worlds.
- timing productive corecursion In Productive Corecursion via Guarded Recursion, Bob Atkey and I used a notion of time to ensure that corecursive processes can always give you ‘today’s’ behaviour before they loop. Days are worlds. At least for streams, Paula Severi is there already (e.g., her ICFP 2012 paper with Fer-Jan de Vries).
- detailsI saw Jeremy Singer give a talk about ‘AnyScale apps’ — programs (e.g. games) which move between computing environments and react dynamically to the available resources (processing power, screen resolution, etc). To make them work, you have to be able to cut off computation below a dynamically chosen level of detail. Clearly, the cruder parts had better not depend on the optional refinements. Detail levels are worlds.
- security As touched on, above, access to information can be managed via a preorder of privilege. Vincent Simonet showed the way with Flow Caml. Security levels are worlds.
- distribution I have a bunch of computers. Each of them has access to some shared libraries, but also their own private memory. Communication between computers is expensive and requires an explicit effect. Types model which knows what. Computing resources are worlds.
- Hoare logic Specifications can talk about program variables, but program code cannot talk about logic variables. Specfication and program live in different worlds.
- phase Typechecking and compilation can involve partial evaluation of arbitrary code. Program execution does not involve types. Information flows from run-time code to the typechecker, even though the temporal order is the other way around. Note that run-time values do not flow to the typechecker, just the symbols which stand for them.
It’s time we stopped thinking of these issues as separate. They have a great deal in common.
Dependent type theory has a bit of a reputation as a mish-mash: all the terms and types jumbled up together in the same syntactic category. The flow of information from terms to types is exactly the source of its power and the basis for confusion amongst casual observers. A common misconception is (or at least used to be) that the flow of information from terms to types prevents the erasure of types from terms: that’s manifest nonsense — it prevents the erasure of terms from types, so no big deal. The absence of typecase means that terms depend only parametrically on types, so type erasure still works. It would be good, however, to nail that down by a separation of worlds. To a large extent, that’s what Sheard and Mishra-Linger did, what Barras and Bernardo did (building on work by Miquel), and what Bernardy and Moulin do in spades: all in different ways. This needs said:
Parametricity arises by quantification against the flow of information.
Quantifying over information you can’t access had better mean you don’t need to care what it is. Dependent type theory needs both parametric quantification (intersection) and non-parametric quantification (product). Moreover, which you choose shouldn’t depend on the domain. I can agree with the claim that it is useful to be able to quantify parametrically over types without believing that all quantification over types should be parametric. With a clear separation of worlds, we could write datatype-generic code when we want to (and stage its execution, too), but still make it clear when parametricity applies. Too many people are trapped into believing nonsense like ‘typecase breaks parametricity’ without interrogating the unstable presumptions that make it wise in a narrow locality.
What do I propose to do about this business of worlds? I’d like to put it on a more general footing. I don’t imagine there’s one holy and perfect system of worlds. I think it’s more important to know when a construction can be transported between systems of worlds. As usual, the morphisms are more important than the objects. So we need to find the general structure. This draft is the beginning of that story, but there’s much more to dig out. I’ll sketch the basic picture here.
Start from a vanilla dependent type theory, where contexts assign types to variables and judgments explain which terms a type admits. Now put everything in a world. Worlds live in a preorder W. Every context entry has a ‘source’ world: judgments construct terms in a ‘target’ world. The variable rule, ‘a variable in the context is a term’ acquires the side-condition that information can flow from source to target.
What about quantification and functions? For a long time, I thought that each world should have its own quantifier, abstraction and application, explaining what it is to be a function over stuff in that world. We’re used to that in System F, right? We have ∀, Λ and type application for functions over types, and →, λ and term application for functions over values: the lack of information flow from terms to types means → is reliably degenerate, and the lack of information flow from types to terms means that ∀ is parametric, allowing the Church-to-Curry erasure. That story works, but it’s not good enough.
Suppose I have a world for library code which can flow into any of a number of discrete computing facilities. I want each local computation to be able to apply library functionality to its own local data. So the type of a library function had better not fix the world its argument comes from. I spent a lot of time staring at Microsoft whiteboards trying to figure out how to recompute the types of functions as they moved between worlds, renegotiating their domains. My brain hurt. Then, the penny dropped.
We need portable quantifiers, e.g., capturing what ‘locally’ means, wherever we happen to be. Let us have a set of quantifiers Q, with a monotonic action, qw, on W. Now, types mention quantifiers, never worlds; worlds live in judgments. When we check a q-λ in world w, we bind the variable in world qw; when we check an application of a q-function in world w, we check the argument in world qw. E.g., the ‘locally’ quantifier has the identity action, but we might also have an ‘intersection’ which maps every w to the world where types live. As we work through a typing derivation, the action of Q on a given w will be iterated, giving each w a local subsystem of worlds. As long as the world preorder preserves the structure of those local subsystems, we can transport constructions whenever the preorder permits.
Here is a hasty Agda formalisation of the world transportation lemma which I cooked up one Sunday morning in the middle of a fen. The less said about the rest of that day, the better.
I think world systems have a considerable potential to change the way we manage information flow (I’m reminded of Douglas Adams’s glorious phrase “rigidly defined areas of doubt and uncertainty”) across a whole bunch of application domains. At the same time, I don’t think they will disturb the way we think about the semantics of type theories: we need a Kripke semantics to manage the context inclusion preorder with which we account for open computation (values are used not only in the empty context, but rather in contexts with at least as much information as the contexts in which they are constructed), so it might as well be an interesting Kripke semantics.
Away from the blackboard, they’ll change the way we do code generation, too. A bunch of these thoughts germinated from a beer mat Edwin Brady and I once scribbled on in the Basque and Carol, and they’re informing what’s happening with erasure in Idris today.
Morphisms between local world systems are important. In our work on corecursion, Bob and I are most particular about ensuring that the time-slicing which justifies the productivity of codata need not be negotiated by its consumer: you work with more of the detail visible, it checks out, then you rub out the pencil.
There’s a lot still to think about, but I’m excited and optimistic at the prospect. The ‘worlds’ idea is altering my perception of lots of other things I work on (i.e., it’s a threshold concept), so forgive me if I’m keen to pass it on.