A fable

[Noam Zeilberger]

John Reynolds, one of the visionaries of type theory, sadly passed away yesterday.  In his honor, members of this list may enjoy reading one of his most beautiful and very influential papers:

Types, Abstraction, and Parametric Polymorphism

ftp://ftp.cs.cmu.edu/usr/jcr/typesabpara.pdf

This paper was one of the first to give a mathematical explanation of the idea that types enable reasoning-up-to-isomorphism through a syntactic discipline of different levels of abstraction.  It begins with a "fable", which I reproduce below:

====

Once upon a time, there was a university with a peculiar tenure policy. All faculty were tenured, and could only be dismissed for moral turpitude. What was peculiar was the definition of moral turpitude: making a false statement in class. Needless to say, the university did not teach computer science. However, it had a renowned department of mathematics.

One semester, there was such a large enrollment in complex variables that two sections were scheduled. In one section, Professor Descartes announced that a complex number was an ordered pair of reals, and that two complex numbers were equal when their corresponding components were equal. He went on to explain how to convert reals into complex numbers, what "i" was, how to add, multiply, and conjugate complex numbers, and how to find their magnitude.

In the other section, Professor Bessel announced that a complex number was an ordered pair of reals the first of which was nonnegative, and that two complex numbers were equal if their first components were equal and either the first components were zero or the second components differed by a multiple of 2π. He then told an entirely different story about converting reals, "i", addition, multiplication, conjugation, and magnitude.

Then, after their first classes, an unfortunate mistake in the registrar's office caused the two sections to be interchanged. Despite this, neither Descartes nor Bessel ever committed moral turpitude, even though each was judged by the other's definitions. The reason was that they both had an intuitive understanding of type. Having defined complex numbers and the primitive operations upon them, thereafter they spoke at a level of abstraction that encompassed both of their definitions.

The moral of this fable is that:

Type structure is a syntactic discipline for enforcing levels of abstraction.

====

Noam