Epilogue

I thought I’d scribble something about what we’re up to. The team (Pierre-Évariste Dagand, Adam Gundry, Peter Morris, James Chapman) have been hard at work. I have been otherwise engaged. As a result, there has been considerable progress. Don’t worry. I expect I’ll mess things up properly over Christmas.

We’ve decided that the best way to get our new type theory out there for you to play with, sooner rather than later, is not to wrap it up in a new version of the Epigram language, but rather to present it as is, in a low-budget command-driven interactive proof assistant. This is beginning to materialise.

One of the good things about having new people in the team is that they’ve had to learn about how we get this stuff to work, and they’ve been writing down what they’re learning in the Epitome. Literate Programming Considered Essential. We’re not trying to take over the world: we’re just trying to make stuff worth stealing. That’s an unusual optimisation problem.

So, the rumours of our death have been slightly exaggerated. My plan is to continue staying out of the way of the coders and write more articles about How It All Works. We’re plotting a bit of a New Year hacking hooley in Tallinn (Glasgow isn’t cold enough). There might be a thing that does something a bit after that.

I’m hoping that this blog will wire up to the new repo real soon, so that you can peer on in. Afore I go, though, let me remark on the importance of Haskell as an enabling technology. Our engineering philosophy is do it once: we prefer to write one abstract piece of code which captures a concept than many concrete pieces of code which follow a pattern; without higher-kind types and classes, we’d be hosed. Given that our main implementation problem is (or rather, was) No Programmers, it is only because of Haskell that a thing exists at all.

Location: Conor’s flat. Crew: Conor McBride, James Chapman, Peter Morris. Lunch: Cafézique. Cake from: Delizique. Dinner: Banana Leaf, Home Wok, Oriental West, the chippy.

Freddie Flintoff helped us to a cracking start by skittling the Aussie tail end. James implemented the setup for untyped quotation (β-normal forms), typed quotation (η-long β-normal forms), definitional equality, and bidirectional type checking.

Peter Morris implemented the feature file for Sigma-types, contributing code fragments to several components via the aspect-oriented programming technology which she supports. He also sorted out our Makefile, so that code gets preprocessed in the right order.

She is getting quite a lot of challenging work, so I’m on running repairs, and other boring jobs.

Implementing the lambda calculus is, along with buying shoes and then not wearing them, one of my worse habits. Here’s today’s cookery, in literate Haskell. I’m using a certain amount of jiggery pokery.

> {-# LANGUAGE GADTs, KindSignatures, EmptyDataDecls,
>     FlexibleInstances, FlexibleContexts
> #-}

I haven’t implemented weak normalization for a while, but Pierre Boutillier and I are currently experimenting with it, reviving my curiosity.

> module Wnf where
> import Control.Applicative
> import Data.Traversable
> import Data.Foldable

Here come all the variations on terms, at once!

> data Form       -- reducible stuff or only normal?
>   = Rdu | Nrm
> data Stage      -- syntax or internal semantic stuff?
>   = Syn Form | Sem
> data Direction  -- checking or inferring types?
>   = Chk | Inf

I’m pretending I have dependent types. It could be worse. Terms are indexed by stage, with syntactic representations for reducible terms and normal forms, and a “semantic” stage for weak normal forms. As ever, I keep parametric in the representation of parameters.

> data Tm :: {-Stage-}* -> {-Direction-}* -> * -> * where

First, the checkable stuff, for all stages.

> -- functions
>   F      :: Bnd k x -> Tm k Chk x
> -- canonical things
>   (:-)   :: Con -> [Tm k Chk x] -> Tm k Chk x
> -- noncanonical things
>   N      :: Tm k Inf x -> Tm k Chk x

Next, the inferrable stuff, likewise.

> -- parameters
>   X      :: x -> Tm k Inf x
> -- eliminations (of noncanonical stuff)
>   (:$)   :: Tm k Inf x -> Elim (Tm k Chk x) -> Tm k Inf x
> -- operations
>   (:@)   :: Op -> [Tm k Chk x] -> Tm k Inf x

Syntactic forms are permitted to use de Bruijn indices.

>   V      :: Int -> Tm (Syn a) Inf x

Syntactic, reducible forms may have definitions and type annotations.

>   (:=:)  ::  Tm (Syn Rdu) Inf x -> Bnd (Syn Rdu) x ->
>              Tm (Syn Rdu) Chk x
>   (:::)  ::  Tm (Syn Rdu) Chk x -> Tm (Syn Rdu) Chk x ->
>              Tm (Syn Rdu) Inf x

Now, what’s a binding? (more…)

Although it might seem all quiet on the Epigram front, in actual fact there is somewhat of a blitz going on at HQ and I thought I’d let you in on some of what has been going on.

As you can see in the last post Conor changed his mind slightly on what Terms where going to be, in those pictures, Up terms are those you can sythesize a type for (and are now called Synth), Down terms are terms you have to push the type into and check (and are now called Check).

Since changing to this representation would break a lot of what is already there we took our experiment ‘offline’ and Conor, James, Wouter and I set to work on implementing all the kit we needed for the new underlying terms (and values). When I say offline, I really mean we created ourselves a Darcs project as it seemed the perfect experiment of our plan to move wholesale to darcs. The results of the tinkering and the experiment can be grabbed by entering ‘darcs get http://sneezy.cs.nott.ac.uk/darcs/term’. It’s not finished, but a few days work bore many fruits.

Next up, holes and Datatypes.

Scoping traverses concrete syntax, threading some effects:

• reading the scope, being (concretely) an alist of strings to namerefs; what is its abstract interface?
• generating new namerefs, due either to an explicit binding (in a pattern or a shadow), or to an implicit binding (a previously unseen name in an lhs or a sig)
• accumulating the set of new namerefs, when we see a name which is not in an explicit binding position, we should look it up if we can and generate a new nameref if not; we must accumulate the set of these names so we can add them to the relevant shadow; this way, the elaborator will know exactly where everything is to be bound
• building imperative syntax trees: we may as well get our node identifiers from the ref supplier; also, we can equip trees with backpointers, and possibly other editor-related gubbins

Scoping will also need to generate binary applications, handling any weird operators we might allow. I’ll have a stab at the datatype of nodes in a bit.

We need a generic protocol for communicating and elaborating concrete syntax. This creates a problem. How specific should we be wrt the syntactic categories of Epigram? My inclination is not at all. We either need a generic technology which will adapt to arbitrary syntactic categories, or we need to flatten the syntactic categories. At the moment, I don’t feel like figuring out how to do the former. So I suggest we adopt some very general setup like this

type Concrete shed = (Mark, CTree shed)
data CTree shed
  = CShed shed
  | CNode Node [Concrete shed]


Remarks

• It’s polymorphic in the contents of sheds, but the elaborator is only ever sent Concrete ()
• The type Mark is some equality type which belongs to the UI: it is used to mark information coming back from the elaborator as concrete syntax is processed.
• The type Node represents both the terminal and nonterminal symbols, whatever they may be. Blah code will need to interrogate this type in arbitrary ways, so things might get a touch existential. As in
  data Blah
  = ...
  | ∀α. Case (Node → Maybe α, [String]) (α → Blah) Blah

  The function tests if the node suits the success continuation. If so, the strings name the subnodes and the success continuation executes; if not, the failure case runs. Of course, the whole thing suspends if we have a shed rather than a node.

Parsing to this representation requires that we can generate suitable elements of Mark (I suspect this may involve refs.) The real exciting stuff in the parser is more likely to involve figuring names out—more on that anon.

Printing. Hmm.