If the unexamined life is not worth living, how attractive then is the life of reflection, where in the limpid pool of thought one finds again the world in miniature, and with the world, illuminations of the beyond? To the list of categories of the human, we should add “reflective animal”, to go with “rational”, and my previous favorite, “theorizing”. So perhaps it is for profound reasons that type theorists feel the pull of reflection, where elements of the type theory appear again in miniature and, crucially, in completed totalities within the type theory. I was struck, in working through the details — with the U. Iowa dependent types reading group consisting of Garrin Kimmell, Duckki Oe, Harley Eades, Frank Fu, and myself — of Conor McBride’s “Ornamental Algebras, Algebraic Ornaments”, by the broad applicability of the idea of reflection in type theory, which Conor puts to brilliant use in several different ways. First (and we have been making our way slowly through his paper, since it relies on a number of background ideas that have taken us some time to absorb), he begins by applying reflection to types. This is a well-known idea in type theory, going back, it seems, to the idea of universes in Martin-Loef type theory. One defines a datatype of types within the type theory. So just as you can declare a datatype of natural numbers or lists, you declare a datatype of types. This is the first essential ingredient of reflection: one needs the world in miniature. So far, there is nothing special here: one could do the same thing in OCaml or Java, for that matter. Just like a Golem or a pre-historic human, this type lacks the breath of life: the miniature is just a collection of stones, or scratches on a cave wall, with nothing to connect it to reality. So it is really the second ingredient of reflection that is the most important, which is the ability to give a semantics to this datatype of types. We have to be able to make the connection, within the type theory, between the world in miniature and the actual world. From signs we need to move to realities. This is something that one cannot usually do in mainstream programming languages, at least not to the extent possible in type theory. We define a function mapping elements of our datatype of types to actual types. Let us write [T] for the interpretation of T, where T is an element of the datatype of types. We can call that datatype of types a universe, following the terminology of Martin-Loef type theory. Then the benefit of reflecting types into a datatype is that we can now have a chance, at least, of writing code that behaves uniformly for all types described by our universe. A dependently typed function can take in an input T of the universe, and then an input of type [T]. This makes sense from a typing perspective, since the interpretation function takes in an element of the universe and gives us a type. So [T] is a type, and a function can request an input of that type. Now by writing this function using recursion and pattern-matching over the structure of T, we can take different action depending on the form of the sign T for the type [T]. Our datatype of types has brought the awesome inaccesible infinity of the actual world down to manageable human proportions, namely the finitely representable. This reflection is not complete — I do not know for sure, but one suspects that it cannot be in general and remain sound. But it is enough to give us new expressive power in the language.
Conor applies reflection in a second way in his article, namely to miniaturize a collection of functions. In most sensible type theories, one cannot write functions by recursion using pattern matching over the structure of functions. You can’t say things like, if the first input is a doubly nested lambda-abstraction (like ) do one thing, and if it is not, do something else. The language does not give you the power to analyze functions intensionally in that way. As an aside, I have to mention that the Archon language I designed a few years back and recently picked up again with Jacques Carette does allow you to do this. See our short paper recently accepted to PEPM ’12, or the longer earlier paper about Archon. Back to reflection: if we want to take different action based on the structure of a function, we can apply the same idea of reflection we used for types. We define a datatype Func, say, where each element has an interpretation as a function belonging to the collection of functions we wish to recurse over. This interpretation is the semantics for the datatype, and it can be defined within the type theory. We may need to apply the earlier idea of reflection for types to be able to give a type to the semantics for Func, since otherwise it won’t be clear what the type of [F] should be, for F an element of Func. Sure, if all the elements of Func were intended to represent functions of the same type X, then we could just define [F] in such a way that it has type X in all cases. But more likely, we want the elements of Func to represent functions of different types. Then we might want, for example, to refine our definition of Func somewhat, so that whenever we have F an element of Func, we know what element T of our type universe we want to associate with it. So we would have F : Func T. Then our semantics can map elements of Func T to [T]. So [F] : [T], where F : Func T. This is a very simplistic rendition of this idea, and certainly Conor’s treatment is much more sophisticated. But this hopefully conveys the basic approach.
So the idea of reflection in type theory is that there is some part of the language which is not directly accessible from within the language. It might be a collection of functions, or types, or who knows what else. And we bring that infinite inaccessibility down to the human level in the way we humans always do, by representation. These blocks are our house, this block is daddie — kids learn this idea very quickly. In type theory, the most useful representings of things are datatypes, since we can pattern match and recurse over them. To connect up our doll world with reality, we define a semantics mapping legos to houses, plastic pieces to soldiers, and so forth. In type theory, this semantics can be defined quite richly within the language itself. Mainstream programming languages can do some similar things, but without as much static information (given by the typing for the semantics) on the relationship between representation and reality.
Seeing the power of reflection in type theory is a small reminder of the centrality, perhaps essential, of the reflective impulse in human experience. Best wishes for the start of Advent, a season which is itself a representation of the exciting if disturbing idea that reflection of the infinite inaccessible down to the human level does not always have to be initiated by us…