More Is Not Always Better

In a previous post I discussed the status of Church’s Law in type theory, showing that it fails to hold internally to extensional type theory, even though one may see externally that the definable numeric functions in ETT are λ-definable, and hence Turing computable.  The distinction between internal and external is quite important in logic, mainly because a logical formalism may be unable to express precisely an externally meaningful concept.  The classical example is the Löwenheim-Skolem Theorem of first-order logic, which says that any theory with an infinite model has a countable model.  In particular the theory of sets has a countable model, which would seem to imply that the set of real numbers, for example, is countable.  But internally one can prove that the reals are uncountable (Cantor’s proof is readily expressed in the theory), which seems to be a paradox of some kind.  But no, all it says is that the function witnessing the countability of the term model cannot be expressed internally, and hence there is no contradiction at all.

A similar situation obtains with Church’s Law.  One may observe empirically, so to say, that Church’s Law holds externally of ETT, but this fact cannot be internalized.  There is a function given by Church’s Law that “decompiles” any (extensional) function of type N→N by providing the index for a Turing machine that computes it.  But this function cannot be definable internally to extensional type theory, because it may be used to obtain a decision procedure for halting of Turing machines, which is internally refutable by formalizing the standard undecidability proof.  In both of these examples it is the undefinability of a function that is important to the expressive power of a formalism, contrary to naïve analyses that would suggest that, when it comes to definability of functions, the more the merrier.  This is a general phenomenon in type theory.  The power of type theory arises from its strictures, not its affordances, in direct opposition to the ever-popular language design principle “first-class x” for all imaginable values of x.

Another perspective on the same issue is provided by Martin-Löf’s meaning explanation of type theory, which is closely related to the theory of realizability for constructive logic.  The high-level idea is that a justification for type theory may be obtained by starting with an untyped concept of computability (i.e., a programming language given by an operational semantics for closed terms), and then giving the meaning of the judgments of type theory in terms of such computations.  So, for example, the judgment A type, where A is a closed expression means that A evaluates to a canonical type, where the canonical types include, say, Nat, and all terms of the form A’→A”, where A’ and A” are types.  Similarly, if A is a type, the judgment a:A means that A evaluates to a canonical type A’ and that a evaluates to a canonical term a’ such that a’ is a canonical element of A’, where, say, any numeral for a natural number is a canonical member of Nat.  To give the canonical members of the function type A’→A” requires the further notion of equality of elements of a type, a=b:A, which all functions are required to respect.  A meaning explanation of this sort was suggested by Martin-Löf in his landmark paper Constructive Mathematics and Computer Programming, and is used as the basis for the NuPRL type theory, which extends that account in a number of interesting directions, including inductive and coinductive types, subset and quotient types, and partial types.

The relation to realizability emerges from applying the meaning explanation of types to the semantics of propositions given by the propositions-as-types principle (which, as I’ve previously argued, should not be called “the Curry-Howard isomorphism”).  According to this view a proposition P is identified with a type, the type of its proofs, and we say that P true iff P evaluates to a canonical proposition that has a canonical member.  In particular, for implication we say that P→Q true if and only if P true implies Q true (and, in addition, the proof respects equality, a condition that I will suppress here for the sake of simplicity).  More explicitly, the implication is true exactly when the truth of the antecedent implies the truth of the consequent, which is to say that there is a constructive transformation of proofs of P into proofs of Q.

In recursive realizability one accepts Church’s Law and demands that the constructive transformation be given by the index of a Turing machine (i.e., by a program written in a fixed programming language).  This means, in particular, that if P expresses, say, the decidability of the halting problem, for which there is no recursive realizer, then the implication P→Q is vacuously true!  By taking Q to be falsehood, we obtain a realizer for the statement that the halting problem is undecidable.  More generally, any statement that is not realized is automatically false  in the recursive realizability interpretation, precisely because the realizers are identified with Turing machine indices.  Pressing a bit further, there are statements, such as the statement that every Turing machine either halts or diverges on its own input, that are true in classical logic, yet have no recursive realizer, and hence are false in the realizability interpretation.

In contrast in the meaning explanation for NuPRL Church’s Law is not assumed.  Although one may show that there is no Turing machine to decide halting for Turing machines, it is impossible to show that there is no constructive transformation that may do so.  For example, an oracle machine would be able to make the required decision.  This is entirely compatible with intuitionistic principles, because although intuitionism does not affirm LEM, neither does it deny it.  This point is often missed in some accounts, leading to endless confusions.  Intuitionistic logic, properly conceived, is compatible with classical logic in that classical logic may be seen as an idealization of intuitionistic logic in which we heuristically postulate that all propositions are decidable (all instances of LEM hold).

The crucial point distinguishing the meaning explanation from recursive realizability is precisely the refusal to accept Church’s Law, a kind of comprehension principle for functions as discussed earlier.  This refusal is often called computational open-endedness because it amounts to avoiding a commitment to the blasphemy of limiting God’s programming language to Turing machines (using an apt metaphor of Andrej Bauer’s).  Rather, we piously accept that richer notions of computation are possible, and avoid commitment to a ”final theory” of computation in which Church’s Law is postulated outright.  By avoiding the witnessing function provided by Church’s Law we gain expressive power, rather than losing it, resulting in an elegant theory of constructive mathematics that enriches, rather than diminishes, classical mathematics.    In short, contrary to “common sense” (i.e., uninformed supposition), more is not always better.

Update: corrected minor technical error and some typographical errors.

Update: clarified point about incompatibility of recursive realizability with classical logic.

Univalent Foundations at IAS

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 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, , has as elements the endpoints , and a path between and within .  The circle, has an element and a path from to itself within .

Respect for homotopy means that, for example, a family of types indexed by the type must be such that if and are isomorphic sets, then there must be an equivalence between the types and allowing us to transport objects from one “fiber” to the other.  And any function with domain must respect bijection—it could be the cardinality function, for example, but it cannot be a function that would distinguish from .

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 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 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 (-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 , for example.  Of course there is no path between and .  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.

Polarity in Type Theory

There has recently arisen some misguided claims about a supposed opposition between functional and object-oriented programming.  The claims amount to a belated recognition of a fundamental structure in type theory first elucidated by Jean-Marc Andreoli, and developed in depth by Jean-Yves Girard in the context of logic, and by Paul Blain-Levy and Noam Zeilberger in the context of programming languages.  In keeping with the general principle of computational trinitarianism, the concept of polarization has meaning in proof theory, category theory, and type theory, a sure sign of its fundamental importance.

Polarization is not an issue of language design, it is an issue of type structure.  The main idea is that types may be classified as being positive or negative, with the positive being characterized by their structure and the negative being characterized by their behavior.  In a sufficiently rich type system one may consider, and make effective use of, both positive and negative types.  There is nothing remarkable or revolutionary about this, and, truly, there is nothing really new about it, other than the terminology.  But through the efforts of the above-mentioned researchers, and others, we have learned quite a lot about the importance of polarization in logic, languages, and semantics.  I find it particularly remarkable that Andreoli’s work on proof search turned out to also be of deep significance for programming languages.  This connection was developed and extended by Zeilberger, on whose dissertation I am basing this post.

The simplest and most direct way to illustrate the ideas is to consider the product type, which corresponds to conjunction in logic.  There are two possible ways that one can formulate the rules for the product type that from the point of view of inhabitation are completely equivalent, but from the point of view of computation are quite distinct.  Let us first state them as rules of logic, then equip these rules with proof terms so that we may study their operational behavior.  For the time being I will refer to these as Method 1 and Method 2, but after we examine them more carefully, we will find more descriptive names for them.

Method 1 of defining conjunction is perhaps the most familiar.  It consists of this introduction rule

and the following two elimination rules

.

Method 2 of defining conjunction is only slightly different.  It consists of the same introduction

and one elimination rule

.

From a logical point of view the two formulations are interchangeable in that the rules of the one are admissible with respect to the rules of the other, given the usual structural properties of entailment, specifically reflexivity and transitivity.  However, one can discern a difference in “attitude” in the two formulations that will turn out to be a manifestation of the concept of polarity.

Method 1 is a formulation of the idea that a proof of a conjunction is anything that behaves conjunctively, which means that it supports the two elimination rules given in the definition.  There is no commitment to the internal structure of a proof, nor to the details of how projection operates; as long as there are projections, then we are satisfied that the connective is indeed conjunction.  We may consider that the elimination rules define the connective, and that the introduction rule is derived from that requirement.  Equivalently we may think of the proofs of conjunction as being coinductively defined to be as large as possible, as long as the projections are available.  Zeilberger calls this the pragmatist interpretation, following Count Basie’s principle, “if it sounds good, it is good.”

Method 2 is a direct formulation of the idea that the proofs of a conjunction are inductively defined to be as small as possible, as long as the introduction rule is valid.  Specifically, the single introduction rule may be understood as defining the structure of the sole form of proof of a conjunction, and the single elimination rule expresses the induction, or recursion, principle associated with that viewpoint.  Specifically, to reason from the fact that to derive , it is enough to reason from the data that went into the proof of the conjunction to derive .  We may consider that the introduction rule defines the connective, and that the elimination rule is derived from that definition.  Zeilberger calls this the verificationist interpretation.

These two perspectives may be clarified by introducing proof terms, and the associated notions of reduction that give rise to a dynamics of proofs.

When reformulated with explicit proofs, the rules of Method 1 are the familiar rules for ordered pairs:

.

The associated reduction rules specify that the elimination rules are post-inverse to the introduction rules:

.

In this formulation the proposition is often written , since it behaves like a Cartesian product of proofs.

When formulated with explicit proofs, Method 2 looks like this:

with the reduction rule

.

With this formulation it is natural to write as , since it behaves like a tensor product of proofs.

Since the two formulations of “conjunction” have different internal structure, we may consider them as two different connectives.  This may, at first, seem pointless, because it is easily seen that for some and that for some , so that the two connectives are logically equivalent, and hence interchangeable in any proof.  But there is nevertheless a reason to draw the distinction, namely that they have different dynamics.

It is easy to see why.  From the pragmatic perspective, since the projections act independently of one another, there is no reason to insist that the components of a pair be evaluated before they are used.  Quite possibly we may only ever project the first component, so why bother with the second?  From the verificationist perspective, however, we are pattern matching against the proof of the conjunction, and are demanding both components at once, so it makes sense to evaluate both components of a pair in anticipation of future pattern matching.  (Admittedly, in a structural type theory one may immediately drop one of the variables on the floor and never use it, but then why give it a name at all?  In a substructural type theory such as linear type theory, this is not a possibility, and the interpretation is forced.)  Thus, the verficationist formulation corresponds to eager evaluation of pairing, and the pragmatist formulation to lazy evaluation of pairing.

Having distinguished the two forms of conjunction by their operational behavior, it is immediately clear that both forms are useful, and are by no means opposed to one another.  This is why, for example, the concept of a lazy language makes no sense, rather one should instead speak of lazy types, which are perfectly useful, but by no means the only types one should ever consider.  Similarly, the concept of an object-oriented language makes no sense, because it amounts to focusing attention solely on the pragmatist conception, to the exclusion of the verificationist, by insisting that only the elimination forms (the so-called “methods”) are relevant in defining an object, and not the introduction forms.

More broadly, it is useful to classify types into two polarities, the positive and the negative, corresponding to the verificationist and pragmatist perspectives.  Positive types are inductively defined by their introduction forms; they correspond to colimits, or direct limits, in category theory.  Negative types are coinductively defined by their elimination forms; they correspond to limits, or inverse limits, in category theory.  The concept of polarity is intimately related to the concept of focusing, which in logic sharpens the concept of a cut-free proof and elucidates the distinction between synchronous and asynchronous connectives, and which in programming languages provides an elegant account of pattern matching, continuations, and effects.

As ever, enduring principles emerge from the interplay between proof theory, category theory, and type theory.  Such concepts are found in nature, and do not depend on cults of personality or the fads of the computer industry for their existence or importance.

Extensionality, Intensionality, and Brouwer’s Dictum

There seems to be a popular misunderstanding about the propositions-as-types principle that has led some to believe that intensional type theory (ITT) is somehow preferable to or more sensible than extensional type theory (ETT).  Now, as a practical matter, few would dispute that ETT is much easier to use than ITT for mechanizing everyday mathematics.  Some justification for this will be given below, but I am mainly concerned with matters of principle.  Specifically, I wish to dispute the claim that t ETT is somehow “wrong” compared to ITT.  The root of the problem appears to be a misunderstanding of the fundamental ideas of intuitionism, which are expressed by the proposition-as-types principle.

The most popular conception appears to be the trivial one, namely that certain inductively defined formal systems of logic correspond syntactically to certain inductively defined formal systems of typing.  Such correspondences are not terribly interesting, because they can easily be made to hold by construction: all you need to do is to introduce proof terms that summarize a derivation, and then note that the proofs of a proposition correspond to the terms of the associated type.  In this form the propositions-as-types principle is often dubbed, rather grandly, the Curry-Howard Isomorphism.  It’s a truism that most things in mathematics are named after anyone but their discoverers, and that goes double in this case.  Neither Curry nor Howard discovered the principle (Howard himself disclaims credit for it), though they both did make contributions to it.  Moreover, this unfortunate name deprives credit to those who did the real work in inventing the concept, including Brouwer, Heyting, Kolmogorov, deBruijn, and Martin-Löf.  (Indeed, it is sometimes called the BHK Correspondence, which is both more accurate and less grandiose.)  Worse, there is an “isomorphism” only in the most trivial sense of an identity by definition, hardly worth emphasizing.

The interesting conception of the propositions-as-types principle is what I call Brouwer’s Dictum, which states that all of mathematics, including the concept of a proof, is to be derived from the concept of a construction, a computation classified by a type.  In intuitionistic mathematics proofs are themselves “first-class” mathematical objects that inhabit types that may as well be identified with the proposition that they prove.  Proving a proposition is no different than constructing a program of a type.  In this sense logic is a branch of mathematics, the branch concerned with those constructions that are proofs.  And mathematics is itself a branch of computer science, since according to Brouwer’s Dictum all of mathematics is to be based on the concept of computation.  But notice as well that there are many more constructions than those that correspond to proofs.  Numbers, for example, are perhaps the most basic ones, as would be any inductive or coinductive types, or even more exotic objects such as Brouwer’s own choice sequences.  From this point of view the judgement stating that is a construction of type is of fundamental importance, since it encompasses not only the formation of “ordinary” mathematical constructions, but also those that are distinctively intuitionistic, namely mathematical proofs.

An often misunderstood point that must be clarified before we continue is that the concept of proof in intuitionism is not to be identified with the concept of a formal proof in a fixed formal system.  What constitutes a proof of a proposition is a judgement, and there is no reason to suppose a priori that this judgement ought to be decidable.  It should be possible to recognize a proof when we see one, but it is not required that we be able to rule out what is a proof in all cases.  In contrast formal proofs are inductively defined and hence fully circumscribed, and we expect it to be decidable whether or not a purported formal proof is in fact a formal proof, that is whether it is well-formed according to the given inductively defined rules.  But the upshot of Gödel’s Theorem is that as soon as we fix the concept of formal proof, it is immediate that it is not an adequate conception of proof simpliciter, because there are propositions that are true, which is to say have a proof, but have no formal proof according to the given rules.  The concept of truth, even in the intuitionistic setting, eludes formalization, and it will ever be thus.  Putting all this another way, according to the intuitionistic viewpoint (and the mathematical practices that it codifies), there is no truth other than that given by proof.  Yet the rules of proof cannot be given in decidable form without missing the point.

It is for this reason that the first sense of the propositions-as-types principle discussed above is uninteresting, for it only ever codifies a decidable, and hence incomplete, conception of proof.  Moreover, the emphasis on an isomorphism between propositions and types also misses the point, because it fails to account for the many forms of type that do not correspond to propositions.  The formal correspondence is useful in some circumstances, namely those in which the object of study is a formal system.  So, for example, in LF the goal is to encode formal systems, and hence it is essential in the LF methodology that type checking be decidable.  But when one is talking about a general theory of computation, which is to say a general theory of mathematical constructions, there is no reason to expect either an isomorphism or decidability.  (So please stop referring to propositions-as-types as “the Curry-Howard Isomorphism”!)

We are now in a position to discuss the relationship between ITT and ETT, and to correct the misconception that ETT is somehow “wrong” because the typing judgement is not decidable.  The best way to understand the proper relationship between the two is to place them into the broader context of homotopy type theory, or HTT.  From the point of view of homotopy type theory ITT and ETT represent extremal points along a spectrum of type theories, which is to say a spectrum of conceptions of mathematical construction in Brouwer’s sense.  Extensional type theory is the theory of homotopy sets, or hSets for short, which are spaces that are homotopically discrete, meaning that the only path (evidence for equivalence) of two elements is in fact the trivial self-loop between an element and itself.  Therefore if we have a path between and in , which is to say a proof that they are equivalent, then and are equal, and hence interchangeable in all contexts.  The bulk of everyday mathematics takes place within the universe of hSets, and hence is most appropriately expressed within ETT, and experience has born this out.  But it is also interesting to step outside of this framework and consider richer conceptions of type.

For example, as soon as we introduce universes, one is immediately confronted with the need to admit types that are not hSets.  A universe of hSets naturally includes non-trivial paths between elements witnessing their isomorphism as hSets, and hence their interchangeability in all contexts.  Taking a single universe of hSets as the sole source of such additional structure leads to (univalent) two-dimensional type theory.  In this terminology ETT is then to be considered as one-dimensional type theory.  Universes are not the only source of higher dimensionality.  For example, the interval has two elements, and connected by a path, the segment between them, which may be seen as evidence for their interchangeability (we can slide them along the segment one to the other).  Similarly, the circle is a two-dimensional inductively defined type with one element, a base point, and one path, a non-reflexive self-loop from the base point to itself.  It is now obvious that one may consider three-dimensional type theory, featuring types such as , the sphere, and so forth.  Continuing this through all finite dimensions, we obtain finite-dimensional type theory, which is just ITT (type theory with no discreteness at any dimension).

From this perspective one can see more clearly why it has proved so awkward to formalize everyday mathematics in ITT.  Most such work takes place in the universe of hSets, and makes no use of higher-dimensional structure.  The natural setting for such things is therefore ETT, the theory of types as homotopically discrete sets.  By formalizing such mathematics within ITT one is paying the full cost of higher-dimensionality without enjoying any of its benefits.  This neatly confirms experience with using NuPRL as compared to using Coq for formulating the mathematics of homotopy sets, and why even die-hard ITT partisans find themselves wanting to switch to ETT for doing real work (certain ideological commitments notwithstanding).  On the other hand, as higher-dimensional structure becomes more important to the work we are doing, something other than ETT is required.  One candidate is a formulation of type theory with explicit levels, representing the dimensionality restriction appropriate to the problem domain.  So work with discrete sets would take place within level 1, which is just extensional type theory.  Level 2 is two-dimensional type theory, and so forth, and the union of all finite levels is something like ITT.  To make this work requires that there be a theory of cumulativity of levels, a theory of resizing that allows us to move work at a higher level to a lower level at which it still makes sense, and a theory of truncation that allows suppression of higher-dimensional structure (generalizing proof irrelevance and “squash” types).

However this may turn out, it is clear that the resulting type theory will be far richer than merely the codification of the formal proofs of some logical system.  Types such as the geometric spaces mentioned above do not arise as the types of proofs of propositions, but rather are among the most basic of mathematical constructions, in complete accordance with Brouwer’s dictum.

Church’s Law

A new feature of this year’s summer school was a reduction in the number of lectures, and an addition of daily open problem sessions for reviewing the day’s material. This turned out to be a great idea for everyone, because it gave us more informal time together, and gave the students a better chance at digesting a mountain of material. It also turned out to be a bit of an embarrassment for me, because I posed a question off the top of my head for which I thought I had two proofs, neither of which turned out to be valid. The claimed theorem is, in fact, true, and one of my proofs is easily corrected to resolve the matter (the other, curiously, remains irredeemable for reasons I’ll explain shortly). The whole episode is rather interesting, so let me recount a version of it here for your enjoyment.

The context of the discussion was extensional type theory, or ETT, which is characterized by an identification of judgemental with propositional equality: if you can prove that two objects are equal,then they are interchangeable for all purposes without specific arrangement. The alternative, intensional type theory,or ITT, regards judgemental equality as definitional equality (symbolic evaluation), and gives computational meaning to proofs of equality of objects of a type, allowing in particular transport across two instances of a family whose indices are equal. NuPRL is an example of an ETT; CiC is an example of an ITT.

Within the framework of ETT, the principle of function extensionality comes “for free”, because you can prove it to hold within the theory. Function extensionality states that whenever . That is, two functions are if they are equal on all arguments (and, implicitly, respect equality of arguments). Function extensionality holds definitionally if your definitional equivalence includes the and rules, but in any case does not have the same force as extensional equality. Function extensionality as a principle of equality cannot be derived in ITT, but must be added as an additional postulate (or derived from a stronger postulate, such as univalence or the existence of a one-dimensional interval type).

Regardless of whether we are working in an extensional or an intensional theory, it is easy to see that all functions of type definable in type theory are computable. For example, we may show that all such functions may be encoded as recursive functions in the sense of Kleene, or in a more modern formulation we may give a structural operational semantics that provides a deterministic execution model for such functions (given , run on until it stops, and yield that as result). Of course the proof relies on some fairly involved meta-theory, but it is all constructively valid (in an informal sense) and hence provides a legitimate computational interpretation of the theory. Another way to say the same thing is to say that the comprehension principles of type theory are such that every object deemed to exist has a well-defined computational meaning, so it follows that all functions defined within it are going to be computable.

This is all just another instance of Church’s Law, the scientific law stating that any formalism for defining computable functions will turn out to be equivalent to, say, the λ-calculus when it comes to definability of number-theoretic functions. (Ordinarily Church’s Law is called Church’s Thesis, but for reasons given in my Practical Foundations book, I prefer to give it the full status of a scientific law.) Type theory is, in this respect, no better than any other formalism for defining computable functions. By now we have such faith in Church’s Law that this remark is completely unsurprising, even boring to state explicitly.

So it may come as a surprise to learn that Church’s Law is false. I’m being provocative here, so let me explain what I mean before I get flamed to death on the internet. (The only worse offense is pointing out the deficiencies of object-oriented programming, but we’ll leave that for another occasion.) The point I wish to make is that there is an important distinction between the external and the internal properties of a theory. For example, in first-order logic the Löwenheim-Skolem Theorem tells us that if a first-order theory has an infinite model, then it has a countable model. This implies that, externally to ZF set theory, there are only countably many sets, even though internally to ZF set theory we can carry out Cantor’s argument to show that the powerset operation takes us to exponentially higher cardinalities far beyond the countable. One may say that the “reason” is that the evidence for the countability of sets is a bijection that is not definable within the theory, so that it cannot “understand” its own limitations. This is a good thing.

The situation with Church’s Law in type theory is similar. Externally we know that every function on the natural numbers is computable. But what about internally? The internal statement of Church’s Law is this: , where the notation means, informally, that is the code of a program that, when executed on input , evaluates to . In Kleene’s original notation this would be rendered as , where the predicate encodes the operational semantics, and the predicate extracts the answer from a successful computation. Note that the expansion makes use of the identity type at the type . The claim is that Church’s Law, stated as a type (proposition) within ETT, is false, which is to say that it entails a contradiction.

When I posed this as an exercise at the summer school, I had in mind two different proofs, which I will now sketch. Neither is valid, but there is a valid proof that I’ll come to afterwards.

Both proofs begin by applying the so-called Axiom of Choice. For those not familiar with type theory, the “axiom” of choice is in fact a theorem, stating that every total binary relation contains a function. Explicitly,

The function is the “choice function” that associates a witness to the totality of to each argument . In the present case if we postulate Church’s Law, then by the axiom of choice we have

.

That is, the functional picks out, for each function in , a (code for a) program that witnesses the computability of . This should already seem suspicious, because by function extensionality the functional must assign the same program to any two extensionally equal functions.

We may easily see that is injective, for if is , then both track both and , and hence and are (extensionally) equal. Thus we have an injection from into , which seems “impossible” … except that it is not! Let’s try the proof that this is impossible, and see where it breaks down. Suppose that is injective. Define , and consider so and we are done. Not so fast! Since is only injective, and not necessarily surjective, it is not clear how to define . The obvious idea is to send to , and any outside the image of to, say, the identity. But there is no reason to suppose that the image of is decidable, so the attempted definition breaks down. I hacked around with this for a while, trying to exploit properties of to repair the proof (rather than work with a general injection, focus on the specific functional ), but failed. Andrej Bauer pointed out to me, to my surprise, that there is a model of ETT (which he constructed) that contains an injection of into ! So there is no possibility of rescuing this line of argument.

(Incidentally, we can show within ETT that there is no bijection between and , using surjectivity to rescue the proof attempt above. Curiously, Lawvere has shown that there can be no surjection from onto , but this does not seem to help in the present situation. This shows that the concept of countability is more subtle in the constructive setting than in the classical setting.)

But I had another argument in mind, so I was not worried. The functional provides a decision procedure for equality for the type : given , compare with . Surely this is impossible! But one cannot prove within type theory that is undecidable, because type theory is consistent with the law of the excluded middle, which states that every proposition is decidable. (Indeed, type theory proves that excluded middle is irrefutable for any particular proposition : .) So this proof also fails!

At this point it started to seem as though Church’s Law could be independent of ETT, as startling as that sounds. For ITT it is more plausible: equality of functions is definitional, so one could imagine associating an index with each function without disrupting anything. But for ETT this seemed implausible to me. Andrej pointed me to a paper by Maietti and Sambin that states that Church’s Law is incompatible with function extensionality and choice. So there must be another proof that refutes Church’s Law, and indeed there is one based on the aforementioned decidability of function equivalence (but with a slightly different line of reasoning than the one I suggested).

First, note that we can use the equality test for functions in to check for halting. Using the predicate described above, we can define a function that is constantly iff a given (code of a) program never halts on given input. We may then use the above-mentioned equality test to check for halting. So it suffices to show that the halting problem for (codes of) functions and inputs is not computable to complete the refutation of the internal form of Church’s Law.

Specifically, assume given that, given a code for a function and an input, yields or according to whether or not that function halts when applied to that input. Define by , the usual diagonal function. Now apply the functional obtained from Church’s Law using the Axiom of Choice to obtain , the code for the function , and consider to derive the needed contradiction. Notice that we have used Church’s Law here to obtain a code for the type-theoretic diagonal function, which is then passed to the halting tester in the usual way.

As you can see, the revised argument follows along lines similar to what I had originally envisioned (in the second version), but requires a bit more effort to push through the proof properly. (Incidentally, I don’t think the argument can be made to work in pure ITT, but perhaps it would go through for ITT enriched with function extensionality.)

Thus, Church’s Law is false internally to extensional type theory, even though it is evidently true externally for that theory. You can see the similarity to the situation in first-order logic described earlier. Even though all functions of type are computable, type theory itself is not capable of recognizing this fact (at least, not in the extensional case). And this is a good thing, not a bad thing! The whole beauty of constructive mathematics lies in the fact that it is just mathematics, free of any self-conscious recognition that we are writing programs when proving theorems constructively. We never have to reason about machine indices or any such nonsense, we just do mathematics under the discipline of not assuming that every proposition is decidable. One benefit is that the same mathematics admits interpretation not only in terms of computability, but also in terms of continuity in topological spaces, establishing a deep connection between two seemingly disparate topics.

(Hat tip to Andrej Bauer for help in sorting all this out. Here’s a link to a talk and a paper about the construction of a model of ETT in which there is an injection from to .)

Types and Cells

The doctrine of computational trinitarianism implies that there should be a categorial analogue of two-dimensional type theory … and indeed there is.  It is called, oddly enough, two-dimensional category theory, which arose first for numerous reasons.  What is two-dimensional category theory?  And how does it relate to two-dimensional type theory?

Two-dimensional category theory may be seen as an instance of the general concept of enriched categories in which the collection of morphisms between any two objects is endowed with some additional structure. A locally small category is one for which the maps between any two objects form a set, called the hom set.  An order-enriched category is one in which the morphisms form an ordered set, which is a set equipped with a pre-order (reflexive and transitive relation) on maps such that composition is monotone.  Order-enriched categories were used by Mitchell Wand and Gordon Plotkin and Mike Smyth in their development of the category-theoretic interpretation of recursive types.  Specifically, an O-category is an order-enriched category whose objects are cpo’s (pre-orders closed under sup’s of chains, and hence containing a least element) and whose hom sets are themselves cpo’s and for which composition is continuous (monotone and preserves suprema of chains).

More generally still, one may  consider (different forms of) category-enriched categories, in which the hom sets are structured as categories with their own vertical notion of identity and composition that meshes well with the horizontal notion of identity and composition of the category itself.  (I will not give here the precise meaning of “meshes well with”, since there are several possible notions and I will be discussing this structure in the type-theoretic setting below.)  The vertical maps are maps between maps that can be interpreted in several ways.  One way is as “witnesses” to an ordering relation among maps, viewing a category as a “pre-order with witnesses”, perhaps an approximation relation among maps such as arises in domain theory.  Another is to view these maps as homotopies between continuous functions on a space; these are the continuous deformations of one map into another.  (This is usually expressed by introducing a “time” coordinate ranging over the unit interval, and stating that a homotopy h between maps f and g is a continuous mapping such that at time zero h agrees with f, at time 1 agrees with g, and smoothly varies at times between.)  An important special case of category-enriched categories are those whose morphisms form (not just a category but also) a groupoid, a category in which each map is invertible.  These can be thought of as “equivalence relations with evidence”; the vertical maps are “proofs” that two horizontal maps are equivalent (for example, homotopic).

The sort of category-enriched categories that I have in mind are called (strict) 2-categories.  And as the terminology suggests, there is nothing special about the number 2 here; one can consider -categories for any number , and even -categories that incorporate all of these into one grand structure (strictly or weakly).  To help manage this structure, the categorists have a uniform terminology that I wish to introduce here, called cells.  The objects in a category are the 0-cells, the maps are the 1-cells, the maps between maps (transformations, homotopies, …) are the 2-cells, and so forth.  A 2-category is one for which we stop at 2-cells; all higher cells being degenerate and hence ignored.  Often the 2-cells (and higher) form groupoids (in one of two senses that I will come back to later); a (2,1)-category is a 2-category in which the 2-cells form a groupoid (but the 1-cells need only form a category).  The class of -categories are the subject of intense interest these days, in part because of their importance in homotopy theory.  They are, however, notoriously hard to manage, and, from what I understand, it is not yet clear what is even the correct definition.

Returning to two-dimensional type theory, and applying the types-as-categories correspondence, we get that types are 0-cells, terms (with free variables) are 1-cells, and transformations are 2-cells.  General terms are not invertible, but transformations are, giving rise to a (strict) groupoid structure expressed by the judgement .  The rules for composition of transformations expresses the vertical structure as forming a strict groupoid.  Ordinary substitution expresses the horizontal structure of terms as maps (plugging in terms for free variables).  But how do these interact?  In strict two-dimensional type theory this interaction is expressed by definitional equalities that express the interchange law between horizontal and vertical composition.  Specifically, we have the following rule:

(More generally one must consider arbitrary contexts, and transformations between substitutions, but this instance of the general case expresses the essential idea.)

This “substitution” principle must satisfy some equational laws that amount to the following conditions:

1. Identity: .
2. Composition: .
3. Interchange: .
4. Delegation: .

(Here is the application of a transformation to a term; it is there to “get the types right”.)  The interchange law is the type-theoretic analogue of the required interaction between 1-composition and 2-composition in a (strict) 2-category.

This is the judgmental structure of strict two-dimensional type theory.  There are several directions we can go from here.  One is to clarify the strict/weak distinction that has been underlying our discussions so far.  Another is to consider how to extend this to three- and higher-dimensional (or, dare I say it, infinite-dimensional) type theory.  The crucial ingredient for both of these discussions is one particular type constructor (more precisely, family of type constructors) that internalizes the hom structure as a type.  In the groupoidal case, where the higher structure is symmetric (invertible), this corresponds to (a version of) the Martin-Löf identity type.  The introduction rule is reflexivity, and the elimination rule is, in essence, the Yoneda Lemma from category theory.  When interpreted in terms of homotopy theory, this is the type of paths in a space, which is critical for defining the fundamental group(oid) of a space, and to clarifying the hinted-at distinction between weak and strict structure in higher dimensions.  More on that later!

Transformations as strict groupoids

The distinguishing feature of higher-dimensional type theory is the concept of equivalence of the members of a type that must be respected by all families of types.  To be sufficiently general it is essential to regard equivalence as a structure, rather than a property.  This is expressed by the judgement

which states that and are equivalent members of type , as evidenced by the transformation .  Respect for equivalence is ensured by the rule

which states that equivalent members determine equivalent instances of a family of types.  The equivalence between instances is mediated by the operation , which sends members of to members of .  We call this mapping the action of the family on the transformation .

For reasons that will only become apparent as we go along, it is important that “equivalence” really be an equivalence: it must be, in an appropriate sense, reflexive, symmetric, and transitive.  The “appropriate sense” is precisely that we require the existence of transformations

Moreover, these transformations must be respected by the action of any family, in a sense that we shall make clear momentarily.  Before doing so, let us observe that these transformations constitute the operations of a groupoid, which we may think of either as an equivalence relation equipped with evidence or a category in which every map is invertible (a generalized group).  While the former interpretation may not suggest it, the latter formulation implies that we should impose some requirements on how these transformations interact, namely the axioms of a groupoid:

1. Composition (multiplication) is associative: .
2. Identity is the unit of composition: and .
3. Inverses cancel: and .

These conditions, which impose equalities on transformations, demand that the second-dimensional structure of a type form a strict groupoid.  I will come back to an important weakening of these requirements later.

We further require that the action of a type family preserve the groupoid structure.  For this it is enough to require that it preserve identities and composition:

and

.

Thinking of a groupoid as a category, these conditions state that the action of a type family be (strictly) functorial.  (Here again we are imposing strong requirements in order to facilitate the exposition; eventually we will consider a relaxation of these conditions that will admit a richer range of applications.)

(The alert reader will note that I have not formally introduced the concept of a transformation between types, nor the equality of these, into the theory.  There are different ways to skin this cat; for now, I will be a bit loose about the axiomatics in order to focus attention on the main ideas.  Rest assured that everything can be made precise!)

By demanding that the groupoid axioms hold strictly (as equalities) and that the action of families be strictly functorial, we have simplified the theory considerably by restricting it to dimension 2.  To relax these restrictions requires higher dimensions.  For example, we may demand only that the groupoid conditions hold up to a transformation of transformations, but hold strictly from then on; this is the 3-dimensional case.  Or we can relax all such conditions to hold only up to a higher transformation, resulting in finite dimensional type theory.  Similar considerations will apply to other conditions that we shall impose on the action of families, in particular to specify the action of type constructors on transformations, which I will discuss next time.  The presentation of finite-dimensional type theory will be aided by the introduction of identity types (also called path types).  Identity types avoid the need for an ever-expanding nesting of transformations between transformations between ….  More on that later!

Update (August 2012): Egbert Rijke has written lucidly on the topic of Yoneda’s Lemma and it’s relation to homotopy type theory in his Master’s Thesis, which I encourage readers to consult for a nice summary of higher-dimensional type theory.

Higher-Dimensional Type Theory

Ideas have their time, and it’s not for us to choose when they arrive.  But when they do, they almost always occur to many people at more or less the same time, often in a slightly disguised form whose underlying unity becomes apparent only later.  This is perhaps not too surprising, the same seeds taking root in many a fertile mind.  A bit harder to explain, though, is the moment in time when an idea comes to fruition.  Often all of the ingredients are available, and yet no one thinks to put two-and-two together and draw what seems, in retrospect, to be the obvious inference.  Until, suddenly, everyone does.  Why didn’t we think of that ages ago?  Nothing was stopping us, we just didn’t notice the opportunity!

The recent development of higher-dimensional structure in type theory seems to be a good example.  All of the ingredients have been present since the 1970′s, yet as far as I know no one, until quite recently, no one quite put together all the pieces to expose the beautiful structure that has been sitting there all along.  Like many good ideas, one can see clearly that the ideas were foreshadowed by many earlier developments whose implications are only now becoming understood.  My plan is to explain higher type theory (HTT) to the well-informed non-expert, building on ideas developed by various researchers, including Thorsten Altenkirch, Steve Awodey, Richard Garner, Martin Hofmann, Dan Licata, Peter Lumsdaine, Per Martin-Löf, Mike Shulman, Thomas Streicher, Vladimir Voevodsky, and Michael Warren.  It will be useful in the sequel to be familiar with The Holy Trinity, at least superficially, and preferably well enough to be able to move back and forth between the three manifestations that I’ve previously outlined.

One-dimensional dependent type theory is defined by derivation rules for these four fundamental forms of judgement (and, usually, some others that we suppress here for the sake of concision):

A context, , consists of a sequence of declarations of variables of the form , where it is presupposed, for each , that is derivable.

The key notion of dependent type theory is that of a family of types indexed by (zero or more) variables ranging over a type.  The judgement states that is a family of types indexed by the variables given by .  For example, we may have , specifying that is a closed type (a degenerate family of types), and , specifying that is a type (say, of sequences of naturals of length ) for each .  The rules of type theory ensure, either directly or indirectly, that the structural properties of the hypothetical/general judgement are valid.  In particular families of types respect equality of indices:

In words, if is a family of types indexed by , and if and are equal members of type , then every member of is also a member of .

The generalization to two- (and higher-) dimensional type theory can be motivated in several ways.  One natural source of higher-dimensional structure is a universe, a type whose elements correspond to types.  For example, we may have a universe of sets given as follows:

and so forth, ensuring that is closed under typical set-forming operations whose interpretations are given by in terms of standard type-theoretic concepts.

In many situations, including much of informal (yet entirely rigorous) mathematics, it is convenient to identify sets that are isomorphic, so that, for example, the sets and would be interchangeable.  In particular, these sets should have the “same” (type of) elements.  But obviously these two sets do not have the same elements (one consists of pairs, the other of functions, under the natural interpretation of the sets as types), so we cannot hope to treat and as equal, though we may wish to regard them as equivalent in some sense.  Moreover, since two sets can be isomorphic in different ways, isomorphism must be considered a structure on sets, rather than a property of sets.  For example, is isomorphic to itself in two different ways, by the identity and by negation (swapping).  Thus, equivalence of the elements of two isomorphic sets must take account of the isomorphism itself, and hence must have computational significance.

It is precisely the desire to accommodate equivalences such as this that gives rise to higher dimensions in type theory.  Specifically, we introduce two-dimensional structure by adding a new judgement to type theory stating that two members of a type are related by a specified transformation:

Crucially, families of types must respect transformation:

A transformation should be thought of as evidence of interchangeability of the members of a type; the map operation puts the evidence to work.

Returning to our example of the universe of sets, let us specify that a transformation from one set to another is an pair of functions constituting a bijection between the elements of the two sets:

(The equational conditions here are rather strong; I will return to this point in a future post.  For now, let us just take this as the defining criterion of isomorphism between two sets.)

Evidence for the isomorphism of two sets induces a transformation on types given by the following equation:

(suppressing the obvious typing premises for and ).  In words an isomorphism between sets and induces a transformation between their elements given by the isomorphism itself.

This, then, is the basic structure of two-dimensional type theory, but there is much more to say!  In future posts I intend to develop the ideas further, including a discussion of these topics:

1. The definition of is given by induction over the structure of .  The above equation covers only one case; there are more, corresponding to each way of forming a family of types .  The extension to function types will expose the role of the inverse of the isomorphism between sets.
2. The judgement may be internalized as a type, which will turn out to correspond to the identity type in Martin-Löf’s type theory, albeit with a different interpretation given by Altenkirch.  The identity type plays an important role in the extension to all higher dimensions.
3. To ensure coherence and to allow for greater expressiveness we must also discuss equality and equivalence of transformations and how these influence the induced transformation of families of types.  In particular transformations admit a groupoid structure which expresses reflexivity, symmetry, and transitivity of transformation; these conditions can be considered to hold strongly or weakly, giving rise to different applications and interpretations.
4. Higher-dimensional type theory admits a fascinating interpretation in terms of homotopy theory which types are interpreted as spaces, members as points in those spaces, and transformations as paths, or homotopies.  This, together with a generalization of the treatment of universes outlined above, is the basis for Voevodsky’s work on univalent foundations of mathematics.
5. One may consider relaxing the groupoid structure on transformations to a “monoidoid” (that is, category) structure by not requiring symmetry (inverses).  The structure of type theory changes significantly in the absence of symmetry, posing significant open problems, but admitting a wider range of applications of higher-dimensional structure in both CS and mathematics.

To keep up to date with the latest developments in this area, please visit the Homotopy Type Theory blog!

The Holy Trinity

The Christian doctrine of trinitarianism states that there is one God that is manifest in three persons, the Father, the Son, and the Holy Spirit, who together form the Holy Trinity.   The doctrine of computational trinitarianism holds that computation manifests itself in three forms: proofs of propositions, programs of a type, and mappings between structures.  These three aspects give rise to three sects of worship: Logic, which gives primacy to proofs and propositions; Languages, which gives primacy to programs and types; Categories, which gives primacy to mappings and structures.  The central dogma of computational trinitarianism holds that Logic, Languages, and Categories are but three manifestations of one divine notion of computation.  There is no preferred route to enlightenment: each aspect provides insights that comprise the experience of computation in our lives.

Computational trinitarianism entails that any concept arising in one aspect should have meaning from the perspective of the other two.  If you arrive at an insight that has importance for logic, languages, and categories, then you may feel sure that you have elucidated an essential concept of computation—you have made an enduring scientific discovery.  Advances in our understanding of computation may arise from insights gained in many ways (any data is useful and relevant), but their essential truth does not depend on their popularity.

Logic tells us what propositions exist (what sorts of thoughts we wish to express) and what constitutes a proof (how we can communicate our thoughts to others).  Languages (in the sense of programming) tells us what types exist (what computational phenomena we wish to express) and what constitutes a program (how we can give rise to that phenomenon).  Categories tell us what structures exist (what mathematical models we have to work with) and what constitutes a mapping between them (how they relate to one another).  In this sense all three have ontological force; they codify what is, not how to describe what is already given to us.  In this sense they are foundational; if we suppose that they are merely descriptive, we would be left with the question of where these previously given concepts arise, leading us back again to foundations.  It is the foundations that I wish to describe here, because I believe it will help to clarify some common misunderstandings about the notions of proposition, type, and structure.  Of particular interest here is that a “type system” is not, under this conception, an arbitrary collection of conditions imposed on a previously given notion of program (whether written with horizontal lines, or not).  It is, rather, a way to say what the programs are in the first place, and what they mean as proofs and as mappings.

Here I will outline the basic correspondences between logic, languages, and categories by examining their structural properties (and, for now, nothing more).

The fundamental notion in logic is that of entailment, written , expressing derivability of from .  This means that is derivable from the rules of logic, given the as axioms.  In contrast to admissibility (which I will not discuss further here) this form of entailment does not express implication!  In particular, an entailment is never vacuously true.  Entailment enjoys at least two crucial structural properties, making it a pre-order:

.

In addition we often have the following additional structural properties:

.

These state that “extra” axioms do not affect deduction; the “order” of axioms does not matter; “duplication” of axioms does not matter.  (These may seem inevitable, but in substructural logics any or all of these may be denied.)

In languages we have the fundamental concept of a typing judgement, written , stating that is an expression of type $A$ involving variables of type $A_i$.  A typing judgement must satisfy the following basic structural properties:

We may think of the variables as names for “libraries”, in which case the first states that we may use any library we wish, and the second states closure under “linking” (as in the Unix tool ld or its relatives), with being the result of linking in to the library .  Typically we expect analogues of the “extra”, “reordering”, and “duplication” axioms to hold as well, though this ain’t necessarily so.  I will leave their formulation as an exercise for the reader.

In categories we have the fundamental concept of a mapping between structures and .  The most elementary structures, perhaps, are sets, and mappings are functions, but it is more common to consider, say, that and are topological spaces, and $f$ is a continuous function between them.  Mappings satisfy analogous structural properties:

These express, respectively, the existence of the identity map, and the closure of maps under composition.  They correspond to reflexivity and transitivity of entailment, and to the library and linking rule of languages.  As with types, one may expect additional closure conditions corresponding to the “extra”, “reordering”, and “duplication” axioms by giving suitable meaning to multiple assumptions.  I will not go into this here, but numerous standard sources treat these conditions in detail.

What I find captivating about computational trinitarianism is that it is beautiful!  Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof!  Imagine a world in which the code is the math, in which there is no separation between the reasoning and the execution, no difference between the language of mathematics and the language of computing.  Trinitarianism is the central organizing principle of a theory of computation that integrates, unifies, and enriches the language of logic, programming, and mathematics.  It provides a framework for discovery, as well as analysis, of computational phenomena.  An innovation in one aspect must have implications for the other; a good idea is a good idea, in whatever form it may arise.  If an idea does not make good sense logically, categorially, and typically (sorry for the neologism), then it cannot be a manifestation of the divine.