Entertainingly, dub types fit elimination-with-a-motive very nicely. The dub types in a problem get refined along with everything else, leaving the same identifiers in scope, but with more informative definitions. That way, we can reliably stack up a sequence of refinement strategies and be sure that the later strategies still make sense in the scope resulting from the earlier strategies. Once refinement’s done, the business of elaborating the next “left-hand side” is to transform the problem into an equivalent one with more dub types inserted, in accordance with the programmer’s use of pattern variables.

We used to have much more ghastly ways to work on this problem. Epigram 1 relied on choosing a particular α-variant of the goal to make the names in scope fit the programmer’s choices. That such an approach violates several of my own principles about meaning and naming should have been a warning to me earlier…

By the way, is there something to say on how the dubbing assumptions (’x’ : S = s) get used? The post only shows their introduction.

did you mean “checkable term” instead?

If Coq supported that, I’d use it. But I won’t hold my breath :)

It would also be nice if you could have multiple rules lined up horizontally, though that would necessitate using a different character for the left and right sides (rather than “!” for both).

I know it sounds silly, but there’s something productivity-enhancing about being able to fit all of your type system’s rules on the screen at once.

I’m expecting that most reasonably customizable editors would allow us to spawn an elaborator on the current buffer contents in the background, then merge the changes made by the elaborator with the changes you’ve made in the meantime, marking conflicts. Just like the elaborator is your annoying coauthor!

Reloading from scratch each time is the easiest thing to get right, but we have been known to make “local undo” work. The logic’s quite tricky: definitions are either Unchanged, Improved, Degraded or Deleted, in increasing order of badness. The worse the news, the harder you have to scrutinize downward dependencies. That way, you can start from the textual damage to the source file and compute how much of a hole it blows in the proof state. It’s worth noting that a construction always amounts to a pair of definitions (T : Set, t : T), which can’t be knocked out by bad news from elsewhere (because Set is always ok, and if T is a Set, it’s reasonable to define a t : T). At a crude level, then, the worst that happens is that we figure out which constructions are downstream of stuff that has changed and we re-elaborate only them. (But is it worth the trouble?)

Elaboration in parallel is very much on the thought-agenda. The elaborator is a kind of multithreaded operating system: it could very well run multithreadedly. A crucial property (sometimes hard to ensure, and not true in Agda or Coq) is that refinement of solutions respects refinement of problems. You can kick off an elaboration problem that isn’t entirely defined and be sure that whatever progress you can make on that basis will not be regretted when the problem becomes more defined. Representing incomplete definitions gives us the basis of a non-blocking read.

Modules, at least in the weak sense of file-and-naming structure, will not be long away. The proof state has a modular structure; the source language will piggyback on that. As for first-class modules, we’re in the fabulous position that (i) all constructions are definitions (ii) (needs implementation, but the result is due to Nicolas Oury) we can always turn a definition into an abstraction with a propositional equation. Representation abstraction needs more thought…

Exports… In dependently typed languages, definitions don’t go out of scope while anything depends on them. While it should be up to the importing module to decide which imported definitions get local short names, everything’s available in principle, so it may be helpful to prepare a candidate import list that isn’t full of incidental crap.

More source language syntax coming soon, and the punctuation details are always up for grabs, but I’m working from the outside in. I have a prejudice about layout (which forces a certain simplicity): it should visibly work in a proportionally spaced font. The question is what cues indentation.

It is, of course, difficult to please. When things are new and strange, it’s a mistake to choose an ill-fitting but familiar-looking notation. Better to be clear that something odd is happening. I expect there’ll be a bit of that.

You’re using your favourite editor, not something I’ve chosen for you then banjaxed specially… It’s a straightforward file transducer, whose primary mode is source-in-source-out… We don’t have a read-eval-print-loop.

So your basic cycle is “save, run transducer, reload file”, perhaps with changes highlighted by your editor in some way? I think a scratch evaluator would still be useful (I found the normaliser very useful in your Agda course), but maybe not – in the same way that a saved, re-runnable test suite is better than evaluating expressions at a REPL.

A useful secondary mode is to keep the system live and maintain an elaboration state in sync with the document: it is then sufficient to trade patches.

Are you thinking of just re-running the transducer from scratch on the patched document, or of maintaining persistent structures and altering them as needed? The latter would have obvious advantages for programming in the large, but strikes me as hard to get right – I know the Factor team had to do a lot of work to get this to work properly.

The glory of lhs2TeX has taught us that it is important to embed programs and program fragments in other documents, especially LaTeX files, allowing the very code that is rendered to be checked.

I think K&R got there first :-)

It should also be possible to mark a definition as something to be elaborated but not brought into scope: we should be able to discuss candidate definitions for something and check that those candidates make sense without necessarily committing to them.

See also: usage examples embedded in documentation. There’s even a Python testing library based around this idea.

every comment sits in a scope, so that escaped expressions (probably) written |expression| can be checked.

Whoa. Cool.

with || signalling end-of-line comments.

You just freaked out every C programmer on the planet :-)

So far, it looks like we have three kinds of construction: datatypes (keyword ‘data’, functions (keyword ‘let’), and proofs (keyword ‘lemma’).

I like this. Simple and clean.

I’m just trying to give an impression of a source language for proofs where one expresses proof strategies and readily verifiable consequences

Looks good to me. I guess you’d need more complicated examples to nail the syntax down, though.

A simple topological sort should be sufficient to yield a suitable elaboration order

This is an implementation detail (one could also imagine, say, bottom-up elaboration in parallel): the hard part is detecting the dependencies (or rather, making them unambiguously detectable). I like your brutal solution, precisely because it’s brutal: simple, memorable rules are generally easier to work with than subtle heuristics that work 99.9% of the time but go wrong in mind-bending edge cases.

Not that I want to get into module system design just now

Don’t put it off for too long: the more I program, the more convinced I become that providing a good-enough module system design is among the most important tasks of a language designer (he says, with precisely zero language designs under his belt). Leave it too late and you end up with #include. You want to provide enough of a module system that programmers feel no need to roll their own, otherwise your community will either fracture or never develop a culture of code-sharing. IMHO, you want to have a Comprehensive Epigram Archive Network up and running as soon as possible (could you piggyback one on Hackage? If not, let me offer my services as a hosting provider).

Plus, I think there’s probably scope to do really interesting things with modules in dependently-typed languages. OCaml’s functors become simple functions from types to tuples of types, but is it possible to write pragmas in user code?

that would suggest using longnames by default for stuff in imported modules, with a manual override allowing imports to name the things which should be usable by short names.

This is considered best practice in the Perl community: it seems to work pretty well. Apart from anything else, it allows you to find where a name comes from by simply searching the current file with your editor.

How do we manage exports?

I’m not sure I understand the problem. Perl modules are expected to provide two arrays, @EXPORT and @EXPORT_OK: the former is all the symbols that are exported by default (best practice is for this to be empty), and the latter is all the symbols that can be exported if requested by client code (this mechanism is actually implemented in userspace code: see here). I guess this mechanism doesn’t make so much sense for a statically-typed language, but the general idea of having two lists should work.

I haven’t said anything about layout yet

Again, I’d suggest – no, beg – that you keep this brutally simple.

That said, the usual inductive-recursive method for making models of predicative type theories might struggle without an inductive characterization of the hierarchy. I wonder what we’d do instead…

Meanwhile, I chose to add ‘bot and ‘top, and to bound the lists at both ends, because these ordered lists are but one instance of a general scheme for constructing ordered data structures. It’s certainly possible to define ordered cons-lists with only a lower bound, but binary search trees require both bounds.

The grammar F ::= 1 | F+F | F[]F | rec determines a class of functors whose fixpoints are readily orderable, given some notion of element X with order < =

[[_]] : F -> (X -> X -> Set) -> (X -> X -> Set)
[[ 1 ]] R l u = :- l <= u
[[ F + F' ]] R l u = [[ F ]] R l u + [[ F' ]] R l u
[[ F [] F’ ]] R l u = (x : X) * [[ F ]] R l x * [[ F' ]] R x u
[[ Rec ]] R l u = R l u

The idea is that everywhere there’s a pair, there’s a pivot. Ordered lists are given by the code 1 + (1 [] Rec). Binary search trees are given by the code 1 + (Rec [] Rec).