As you may know (for example, from my interview a little while back on the fantastic Type Theory Podcast), we are working here at U. Iowa on a new dependent type theory implementation called Cedille.  It is based on a new extrinsic (aka Curry-style) type theory, and aims to be a very compact theory in which standard parts of dependent type theory like inductive (and hopefully coinductive) datatypes can be defined from the more primitive constructs of the theory.

At our first Cedille meeting of the fall semester — also in attendance Larry Diehl, Richard Blair, Chris Jenkins, Tony Cantor, Colin McDonald, Nadav Kohen — I gave a rather long overview of the current state of Cedille, which I recorded as a screencast and as the notes I was drawing (.ora and .jpg formats) while talking.  While we are (still! [sigh]) not quite ready to make a public release, I think we will get there this fall, as I mention in the screencast.  A few quick highlights are: we have a derivation of induction that is parametrized by a functor (actually, we have two: one for Church encoding and one for Mendler encoding); we can do some surprising and cool things with casts, which are derivable in the theory, including define within Cedille monotone recursive types and get proof reuse between types which can be cast to each other, like lists and vectors; and we just need to complete a (very basic) module system and solve an unpleasant performance issue with our parser, and we should be ready to make a release.

I recently (May 1) gave a short presentation touching on ethics and technology, as well as the ethics of Internet pornography.  I am sharing the slides here.  Sadly, most of the references on the seemingly unending list of harms and evils associated with pornography are behind paywalls, although the article by Max Waltman is freely available.  As always when reading about this topic, please be aware that some of the material can be quite upsetting for people who have experienced sexual assault, abuse, childhood assault, or other traumatic experiences, as well as for young readers.

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!