I have been blessed the past few days to have some amazing conversations with people working with me here at Iowa.  For one of these, I talked yesterday with Richard Blair and Ananda Guneratne about semantics of recursive types, as this is something Richard is currently working on.  The conversation was so inspiring I wrote up a short note summarizing it.  You can find this note here.

You find yourself, like Jacob, gazing up the rungs (for me, ropes)

of a ladder that seems to have constructed itself

to avoid leaving you flat on the ground.

But what, you ask, in the arching presence of the angels,

do you do at the top?

Type theories, to be consistent, cannot be uniform.  Somewhere, your power must ebb, abstractions diminish, until finally you are left with the beautiful silence of a single symbol (maybe $\Box$).  Type : type is also beautiful, but long known to be inconsistent: collapsing everything to one level ruins your type theory as a logic.  There are more subtle examples of the need to give up your power as you ascend (this starts to sound like John of the Cross).  You cannot repeat impredicative quantification one level up, for example: Girard proved this is paradoxical in his dissertation.  So if you are an impredicativist as I am, your kind level must be strictly weaker than your type level.

But what about if you are a predicativist, perhaps a devotee (as I also am) of Agda?  Agda, and also Coq via its ECC (Extended Calculus of Constructions, of Zhaohui Luo) structure, seem to avoid this quietist imperative I am mentioning.  Above the current level, there is another, with essentially the same power.  And beyond that, another, ad infinitum.  The ladder goes up forever!  We surpass the heavens!

But no, experienced Agda and Coq users know that is sadly not what happens.  Much like the tower of Babel, the predicative universe hierarchy does not satisfy the desires of abstraction.  For some constructions make sense at all levels, and hence we introduce the seductive ideas of typical ambiguity (considered for a system $\textit{CC}^\omega$ of Coquand’s which is a predecessor of ECC, by Harper and Pollack) and universe polymorphism (also considered by Harper and Pollack).  Universe polymorphism as I understood it from Agda seems a bit different from what Harper and Pollack propose.  And it seems that typical ambiguity is found more in Coq than Agda.  (I could be wrong on these points!)  In Agda, there seems to be the curious idea that we can quantify over all levels of the hierarchy explicitly.  And we are then left with the conundrum of what level such a quantification itself has?  Of course, for soundness reasons, it cannot have one of the levels covered by the level quantification.  So we have to make up a new level, namely $\omega$.  And we see that level quantification was a charade to begin with: we are definitely not quantifying over all the levels, just some prefix of them.  And it seems Agda does not make $\omega$ available to you to use in your code.  So this just seems very hacky.

More principled is something that I think is closer to the kind of universe polymorphism that Harper and Pollack were proposing, which in their work is located at global definitions (not arbitrary terms).  And this is the answer to my riddle at the beginning: when you reach the top of your ladder, you have to “go meta”.  It is a beautiful insight that we can internalize the induction scheme one finds in Peano Arithmetic as a single second-order axiom.  We have passed from the meta-level, with a family of formulas, to a single object-language formula.  I propose that when we reach the top layer of our layered type theory, we do the reverse.  We add schematic definitions.

Here at Iowa, we are working on this new Cedille type theory and system.  Some of my recent papers are about this.  There, we have a predicative hierarchy truncated at level 2.  Ha!  There are just terms, types, and kinds.  It is actually more convenient to reach the end of the ladder faster!  And going schematic means that while we do not support kind-level functions, we will allow you to define parametrized kinds.  So you can give a top-level definition of some kind parametrized by terms or types.  The definition itself does not need some funny type with $\omega$ level or some additional superkind structure.  Of course, one can only use the definition with all parameters instantiated.

Simple, but extends expressivity a bit just out of the reach of what can be internalized in the theory.

Yours truly is interviewed now on the wonderful Type Theory Podcast.  Very exciting!

This post is about double negation in constructive type theory.  Suppose you know that $\neg(\neg A)$ is true; i.e., $(A \to \perp)\to \perp$ (writing $\perp$ for false).  In classical logic, you then know that $A$ is true.  But of course, you are allowed no such conclusion in intuitionistic logic.  So far, so familiar.  But let us look at this now from the perspective of realizability.  Realizability semantics gives the meaning of a type as a set of some kind of realizers.  Let us consider untyped lambda calculus terms (or combinators) as realizers for purposes of this discussion.  Then the crucial clauses of the semantics for our purposes are

• $t \in [\negthinspace[ A \to B ]\negthinspace ]\ \Leftrightarrow\ \forall t' \in[\negthinspace[A]\negthinspace].\ t\ t'\in[\negthinspace[B]\negthinspace]$, and
• $\neg t \in [\negthinspace[\perp]\negthinspace]$

Let us work through, then, when $t\in[\negthinspace[(A\to\perp)\to\perp]\negthinspace]$ according to this definition:

$\begin{array}{ll} t\in[\negthinspace[(A\to\perp)\to\perp]\negthinspace] & \Leftrightarrow \\ \forall t'\in[\negthinspace[A\to\perp]\negthinspace].\ t\ t'\in[\negthinspace[\perp]] & \Leftrightarrow \\ \forall t'.\neg(t'\in[\negthinspace[ A \to \perp]\negthinspace]) & \Leftrightarrow \\ \neg(t'\in[\negthinspace[A\to\perp]\negthinspace]) & \Leftrightarrow \\ \neg(\forall t''\in[\negthinspace[A]\negthinspace].\ t'\ t''\in[\negthinspace[\perp]\negthinspace]) & \Leftrightarrow \\ \neg(\forall t''.\neg t''\in[\negthinspace[A]\negthinspace]) & \Leftrightarrow \\ \exists t''.t''\in[\negthinspace[A]\negthinspace] &\ \end{array}$

So this is saying that if $[\negthinspace[A]\negthinspace]$ is nonempty, then $[\negthinspace[(A\to\perp)\to\perp]\negthinspace]$ is universal (contains all terms); and otherwise (if $[\negthinspace[A]\negthinspace]$ is empty), $[\negthinspace[(A\to\perp)\to\perp]\negthinspace]$ is empty.

So if you have a function $F$, say, realizing $\neg\neg A)\to B$ for some $B$, what this means is that $F$ can make use of the fact that $A$ is true, but not how it is true.  If $F$ were simply given a proof of $A$, then it could compute with this proof.  But here, with $\neg\neg A$, the proof of $A$ is hidden behind an existential quantifier (as we deduced above), and so it cannot be used.  Only if someone is reasoning at the metalevel about $F$, they can make use of the fact that $A$ is true when checking that the body of $F$ realizes $B$.

So semantically, $\neg\neg A$ is news you can’t use: we know $A$ is true, but we have no access to how it is true.  For example, if $A$ is a disjunction, you cannot case split, within the type theory, on the disjuncts.  Only at the metalevel are you entitled to consider the behavior of a term in light of the fact that one or the other of the disjuncts must hold.

Greetings, QA9 reader(s).  It has been a while since I posted, for which I offer the usual excuses.  I have a backlog of interesting technical things I’m hoping to write about sometime pretty soon: failure of subject reduction in lambda2 with eta-contraction, which I learned about maybe a year ago but did not record in a post; also intriguing things I am reading about deep inference, although there the problem is the stuff is, well, deep and I haven’t understood it well enough yet to have too much to say.  I also had high hopes of posting about the super fun summer I had here at U. Iowa working on Cedille with great new U. Iowa graduate students Chad Reynolds, Ananda Guneratne, and Richard Blair; great visiting Indiana doctoral student Matthew Heimerdinger; and inspiring visitors Stéphane Graham-Lengrand, Olivier Hermant, and Vincent St-Amour.  In a perfect world I would have some pictures to post of all this stimulating interaction, but here I am photo-less.

But what impels me to write today is getting bitten again by performance problems with well-founded recursion in Agda.  Just for fun, I will tell you the story.  We are working on this new interactive theorem prover called Cedille based on dependently typed lambda encodings.  You can read about this in the project report we just revised to submit for the TFP 2016 post-proceedings.  Thanks to the determination of Matthew (Heimerdinger), we have a highlighting mode — actually several — for Cedille in our emacs interface.  One funny wrinkle was that we could not highlight comments, because our parser was just dropping them, and we did not want to store information about them in our abstract syntax trees (which would then become very cluttered).  We hit upon a daring (for us, anyway) solution: parse input files a second time, with a different grammar that is recognizing just whitespace and comments.  It is nice to find the whitespace, too, in addition to the comments, since then we can set highlighting to the default for those spans of the text in the emacs mode.  Otherwise, with the way our interaction between emacs frontend and Agda backend works (see that revised project report), if you type in whitespace you will likely get a non-default highlighting color, from the span containing that whitespace.

Ok, so we (Richard) wrote the grammar for this, and we started producing comment and whitespace spans to send to the frontend, only to see some very sluggish performance on a couple longer files.  We misdiagnosed this as coming from doing lots of string appends (with what correspond to slow strings in Haskell; i.e., lists of characters), and I dutifully changed the code to print the spans to a Haskell Handle, rather than computing one big string for all the spans and then printing that.  Distressingly, this optimization, which took maybe an hour or so to implement, with finding the right Haskell stuff to hook up to, did not improve performance.  Well shucks!  Let’s get out our handy Haskell profiler and see what is going wrong.  Now sadly, I am still on Agda 2.4.2.4, which lacks this nifty agda-ghc-names tool that is part of Agda 2.5.1 now.  That tool translates Haskell names that are generated by the Agda compiler, back to names from the Agda source.  But this tool was not needed to see the following:

COST CENTRE MODULE %time %alloc

d179.\.\.\ MAlonzo.Code.QnatZ45Zthms 35.9 18.8
d179.\ MAlonzo.Code.QnatZ45Zthms 11.6 48.8
d191.\ MAlonzo.Code.QnatZ45Zthms 9.6 7.5
d179 MAlonzo.Code.QnatZ45Zthms 5.7 0.0
d191 MAlonzo.Code.QnatZ45Zthms 5.2 0.0
d179.\.\ MAlonzo.Code.QnatZ45Zthms 4.7 11.3

Oh pondwater.  Over half the time is being spent in functions in nat-thms.agda in the IAL.  That file contains, as the name suggests, just theorems about the natural numbers — not code I expect to be running intensively during execution of the Cedille backend.  But I have seen this before, as I noted.  These are lemmas getting called again and again during a well-founded recursion, to show that certain less-than facts hold.  Which well-founded recursion was it?  It turns out it was for the function that converts a natural number to a string.  We are doing that operation many times, to print character positions in the input Cedille source file.  Just removing the well-founded recursion and marking the nat-to-string function as needing NO_TERMINATION_CHECK reduced the running time to less than half what it was.

The moral of this story is the same as the moral of the previous story: be wary of well-founded recursion in Agda for code you intend to run (as opposed to just reason about).

Have a blessed start of fall!