The Trellys project, which I’ve mentioned before, is working to design and implement a CBV functional programming language with dependent types, using community-based processes to take advantage of expertise from the dependent types and the functional programming communities.  Our first PIs’ meeting was June 30th through July 2nd, here at The University of Iowa.  In attendance were:

• Tim Sheard and Ki Yung Ahn from Portland State University.
• Stephanie Weirich, Chris Casinghino, and Vilhelm Sjoeberg (U. Penn., though Vilhelm is visiting Iowa this summer).
• Harley Eades III, Frank (Peng) Fu, Garrin Kimmel (just joining U. Iowa from Kansas U.), Duckki Oe, and myself.
• Adam Procter from U. Missouri (visiting me at Iowa this summer).

We had a very productive meeting, and have managed now, I think, to integrate several language ideas we had b[een exploring up to now: compile-time versus run-time arguments to functions, type-level computation (aka, “large eliminations”), general recursive versus terminating recursive functions, equality types $t_1 = t_2$ interpreted as something like joinability in the operational semantics of the erasures of $t_1$ and $t_2$, and bootstrapping terminating recursion for datatypes from terminating recursion on natural numbers.

At a high-level, the language is divided into two parts: a proof part and a programming part.  These parts are not distinguished syntactically, as I had done previously in Guru, and is done in other systems like Feferman’s System W (referred to in an earlier post on this blog).  Rather, the typing judgment distinguishes which expressions can soundly be viewed as falling into the proof part, and which can only be viewed as programs.  The main judgment is $\Gamma \vdash t : T\, \theta$, which means that $t$ has type $T$ in context $\Gamma$ (as usual); and $t$ is a proof expression if $\theta$ is “proof”, and a program expression if $\theta$ is “program”.  Some expressions can be safely viewed as both proofs and programs: namely, constructive proofs.  Non-constructive proofs cannot be viewed as programs, since we do not wish to give an operational semantics for them (there are well-known computational interpretations of classical logic that would allow us to do this, but it dos not fit our purpose in this language design).  General recursive functions (i.e., ones falling outside the fragment of the language that the typing rules conservatively identify as terminating) cannot be viewed as proofs.  This categorization of expressions as terminating vs. non-terminating and constructive vs. non-constructive leaves open a fourth possibility: general recursive non-constructive expressions.  But I do not see any use for these at the moment.  Indeed, even including non-constructive reasoning in the proof part is already a bit new, since most dependent type theories (with the notable exception of Luo and Adams‘s systems of logic-enriched type theory) are constructive.

To me, the most important feature we nailed down for this language is its support for what I think of as freedom of speech.  Indeed, in an amazing coincidence, the beautiful seminar room in the School of Journalism which we used for our three-day meeting had a large reproduction of the First Amendment of the U.S. Constitution on the wall.  You’ll see it when I get the group pictures from Tim or Stephanie.  Anyhow, the principle of freedom of speech is that it is ok to speak about anything you want; speaking about something is different from actually affirming it.  I can talk about violence without advocating it, for example.  In the Trellys core language, we want to be able to state and prove theorems about general-recursive programs.  So we want to write down a proof $\pi$ about a general-recursive program $P$.  This $\pi$ will, in general, have to mention $P$ — for example, to state that it is non-terminating, or perhaps to prove that it is terminating and enjoys some property.  As I mentioned above, our basic typing judgment in Trellys uses a qualifier $\theta$ to keep track of whether or not the expressions in question are proof expressions or program expressions.  To allow proofs to mention programs and yet still be counted as proofs, some of our typing rules have to be non-strict in this qualifier: some premises of the rule indicate that an expression is a program, and yet the conclusion will still indicate that other expressions are proofs.  An example is one of the application rules (we have several).  If the argument is syntactically a value, then it can be a program, and the application itself can still be a proof (if the function part of the application is a proof).  Restricting to a value here makes it possible to define the semantics of types which fall into the proof part of the language — types which we can soundly view as formulas — without being forced to define a deep semantics for more general types, which could include some pretty hair-raising features in Trellys (type:type, general-recursive computation of type expressions, etc.).  So it is more correct to say that proofs can talk about program values — but these can be quite arbitrary (including functions which would diverge if applied, or which require really rich typing features in order to type check).

So our next steps will be writing up the typing rules in detail (we have an Ott file that already has a lot of the most important details filled in), and starting to work on a prototype implementation, using some cool libraries that Stephanie and Tim have been working with to provide clean and elegant support for data with name-binders, in Haskell.  It’s going to be fun.