## Exceptions Are Shared Secrets

December 3, 2012

Exceptions are commonly criticized as being the “goto’s” of modern programming languages.  Raising an exception transfers control to an unknown destination, it is said, and this is a bad thing on engineering grounds.  I disagree.  It is perfectly predictable where a raised exception will be handled, provided that exceptions are done properly, which, unfortunately, is not always the case.

The crucial point that exception values are shared secrets. Let us distinguish two parties, the raiser of the exception, and the handler of it. The fundamental idea of exceptions is to transfer a value from the raiser to the handler without the possibility of interception by another party. While the language of secrecy seems appropriately evocative, I hasten to add that I am not here concerned with “attackers” or suchlike, but merely with the difficulties of ensuring modular composition of programs from components. In such a setting the “attacker” is yourself, who is not malicious, but who is fallible.

By raising an exception the raiser is “contacting” a handler with a message. The raiser wishes to limit which components of a program may intercept that message. More precisely, the raiser wishes to ensure that only certain previously agreed-upon components may handle that exception, perhaps only one. This property should remain stable under extension to the program or composition with any other component. It should not be possible for an innocent third party to accidentally intercept a message that was not intended for it.

Achieving this requires a secrecy mechanism that allows the raiser and the handler(s) to agree upon their cooperation. This is accomplished by dynamic classification, exactly as it is done properly in Standard ML (but not O’Caml). The idea is that the raiser has access to a dynamically generated constructor for exception values, and any handler has access to the corresponding dynamically generated matcher for exception values. This means that the handler, and only the handler, can decode the message sent by the raiser; no other party can do anything with it other than pass it along unexamined. It is “perfectly encrypted” and cannot be deciphered by any unintended component.

The usual exception mechanisms, as distinct from exception values, allow for “wild-card handlers”, which means that an exception can be intercepted by a third party. This means that the raiser cannot ensure that the handler actually receives the message, but it can ensure, using dynamic classification, that only a legitimate handler may decipher it. Decades of experience with Standard ML shows that this is a very useful thing indeed, and has application far beyond just the simple example considered here. For full details, see my forthcoming book, for a full discussion of dynamic classification and its role for ensuring integrity and confidentiality in a program. Dynamic classification is not just for “security”, but is rather a good tool for everyday programming.

Haskell is one language that does not get exceptions right.  Allocating an exception incurs a storage effect, and so would have to be confined to the IO monad in Haskell.  But this would destroy the utility of exceptions in pure code.  The result is an exception mechanism that is arguably broken and that does not provide the guarantees that make exceptions a perfectly pleasant and useful way to write code.

Update: Reworked last paragraph to clarify the point I am making; the previous formulation appears to have invited misinterpretation.

Update: This account of exceptions also makes clear why the perennial suggestion to put exception-raising information into types makes no sense to me. I will write more about this in a future post, but meanwhile contemplate that a computation may raise an exception that is not even in principle nameable in the type. That is, it is not conservativity that’s at issue, it’s the very idea.

Update: Wordsmithing, removal of irrelevant remarks to focus on the main point about dynamic exceptions.

## Practical Foundations for Programming Languages Is Out

December 3, 2012

Practical Foundations for Programming Languages, published by Cambridge University Press, is now available in print! It can be ordered from the usual sources, and maybe some unusual ones as well. If you order directly from Cambridge using this link, you will get a 20% discount on the cover price (pass it on).

Since going to press I have, inevitably, been informed of some (so far minor) errors that are corrected in the online edition. These corrections will make their way into the second printing. If you see something fishy-looking, compare it with the online edition first to see whether I may have already corrected the mistake. Otherwise, send your comments to me.

By the way, the cover artwork is by Scott Draves, a former student in my group, who is now a professional artist as well as a researcher at Google in NYC. Thanks, Scott!

Update: The very first author’s copy hit my desk today!

## Univalent Foundations at IAS

December 3, 2012

As many of you may know, the Institute for Advanced Study is sponsoring a year-long program, called “Univalent Foundations for Mathematics” (UF), which is developing the theory and applications of Homotopy Type Theory (HTT).  The UF program is organized by Steve Awodey (CMU), Thierry Coquand (Chalmers), and Vladimir Voevodsky (IAS).  About two dozen people are in residence at the Institute to participate in the program, including Peter Aczel, Andrej Bauer, Peter Dybjer, Dan Licata, Per Martin-Löf, Peter Lumsdaine, Mike Shulman, and many others.  I have been shuttling back and forth between the Institute and Carnegie Mellon, and will continue to do so next semester.

The excitement surrounding the program is palpable.  We all have the sense that we are doing something important that will change the world.  A typical day consists of one or two lectures of one or two hours, with the rest of the day typically spent in smaller groups or individuals working at the blackboard.  There are many strands of work going on simultaneously, including fundamental type theory, developing proof assistants, and formulating a body of informal type theory.  As visitors come and go we have lectures on many topics related to HTT and UF, and there is constant discussion going on over lunch, tea, and dinner each day.  While there I work each day to the point of exhaustion, eager to pursue the many ideas that are floating around.

So, why is homotopy type theory so exciting?  For me, and I think for many of us, it is the most exciting development in type theory since its inception.  It brings together two seemingly disparate topics, algebraic topology and type theory, and provides a gorgeous framework in which to develop both mathematics and computer science.  Many people have asked me why it’s so important.  My best answer is that it’s too beautiful to be ignored, and such a beautiful concept bmust be good for something!  We’ll be at this for years, but it’s too soon to say yet where the best applications of HTT will arise.  But I am sure in my bones that it’s as important as type theory itself.

Homotopy type theory is based on two closely related concepts:

1. Constructivity.  Proofs of propositions are mathematical objects classified by their types.
2. Homotopy.  Paths between objects of a type are proofs of their interchangeability in all contexts.  Paths in a type form a type whose paths are homotopies (deformations of paths).

Homotopy type theory is organized so that maps and families respect homotopy, which, under the identification of paths with equality proofs, means that they respect equality.  The force of this organization arises from axioms that specify what are the paths within a type.   There are two major sources of non-trivial paths within a type, the univalence axiom, and higher inductive types.

The univalence axiom specifies that there is an equivalence between equivalences and equalities of the objects of a universe.  Unravelling a bit, this means that for any two types inhabiting a universe, evidence for their equivalence (a pair of maps that are inverse up to higher homotopy, called weak equivalence) is evidence for their equality.  Put another way, weak equivalences are paths in the universe.  So, for example, a bijection between two elements of the universe $\textsf{Set}$ of sets constitutes a proof of the equality (universal interchangeability) of the two sets.

Higher inductive types allow one to define types by specifying their elements, any paths between their elements, any paths between those paths, and so on to any level, or dimension.  For example, the interval, $I$, has as elements the endpoints $0, 1 : I$, and a path $\textsf{seg}$ between $0$ and $1$ within $I$.  The circle, $S^1$ has an element $\textsf{base}$ and a path $\textsf{loop}$ from $\textsf{base}$ to itself within $S^1$.

Respect for homotopy means that, for example, a family $F$ of types indexed by the type $\textsf{Set}$ must be such that if $A$ and $B$ are isomorphic sets, then there must be an equivalence between the types $F(A)$ and $F(B)$ allowing us to transport objects from one “fiber” to the other.  And any function with domain $\textsf{Set}$ must respect bijection—it could be the cardinality function, for example, but it cannot be a function that would distinguish $\{\,0,1\,\}$ from $\{\,\textsf{true},\textsf{false}\,\}$.

Univalence allows us to formalize the informal convention of identifying things “up to isomorphism”.  In the presence of univalence equivalence types (spaces) are, in fact, equal.  So rather than rely on convention, we have a formal account of such identifications.

Higher inductives generalize ordinary inductive definitions to higher dimensions.  This means that we can now define maps (computable functions!) between, say, the 4-dimensional sphere and the 3-dimensional sphere, or between the interval and the torus.  HTT makes absolutely clear what this even means, thanks to higher inductive types.  For example, a map out of $S^1$ is given by two pieces of data:

1. What to do with the base point.  It must be mapped to a point in the target space.
2. What to do with the loop.  It must be mapped to a loop in the target space based at the target point.

A map out of $I$ is given similarly by specifying

1. What to do with the endpoints.  These must be specified points in the target space.
2. What to do with the segment.  It must be a path between the specified points in the target space.

It’s all just good old functional programming!  Or, rather, it would be, if we were to have a good computational semantics for HTT, a topic of intense interest at the IAS this year.  It’s all sort-of-obvious, yet also sort-of-non-obvious, for reasons that are difficult to explain briefly.  (If I could, they would probably be considered obvious, and not in need of much explanation!)

A game-changing aspect of all of this is that HTT provides a very nice foundation for mathematics in which types ($\infty$-groupoids) play a fundamental role as classifying all mathematical objects, including proofs of propositions, which are just types.  Types may be classified according to the structure of their paths—and hence propositions may be classified according to the structure of their proofs.  For example, any two proofs of equivalence of two natural numbers are themselves equivalent; there’s only one way to say that $2+2=4$, for example.  Of course there is no path between $2+2$ and $5$.  And these two situations exhaust the possibilities: any two paths between natural numbers are equal (but there may not even be one).  This unicity of paths property lifts to function spaces by extensionality, paths between functions being just paths between the range elements for each choice of domain element.  But the universe of Sets is not like this: there are many paths between sets (one for each bijection), and these are by no means equivalent.  However, there is at most one way to show that two bijections between sets are equivalent, so the structure “peters out” after dimension 2.

The idea to apply this kind of analysis to proofs of propositions is a distinctive feature of HTT, arising from the combination of constructivity, which gives proofs status as mathematical objects, and homotopy, which provides a powerful theory of the equivalence of proofs.  Conventional mathematics ignores proofs as objects of study, and is thus able to express certain ideas only indirectly.  HTT brings out the latent structure of proofs, and provides an elegant framework for expressing these concepts directly.

Update: edited clumsy prose and added concluding paragraph.