Epilogue

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.

More to say about this anon, but here are some boards, before I clean them to write some more.

Just a thought, which I decided to scribble down before I forgot it.

Key policy: Epigram is a declare-before-use language, temporally as well as spatially. When you say x, you get the most local existing x at that time, or you get a new x generated as locally as possible. In a declaration, spare names go into the generalisation prefix; in a rhs, spare names go into the where clause, one way or another. Naming is a surrogate for pointing, so once the bond of reference is created, it must not be broken by ill-propagated renamings, capturings, or whatever. It’s this policy which enables scope resolution at any point in time: there should never be any issue about the referent of an identifier.

Now, we go backwards as well as forwards, this time around, so what happens when you delete information. Well, there are at least two sorts of undo: devaluation (removing (parts of) the value of a symbol) and degeneration (removing the symbol altogether). Now, you propagate a devaluation by rechecking and devaluing everything which depends on a devalued symbol. Degeneration is much scarier. But I remember now, there’s a funny thing. If you set things up right, you don’t need degeneration, exactly…

Imagine we have only let (the sooner we turn data into sugar for let, the better). You can devalue a let, replacing the top rhs by a shed. Now, key editing move: you can commute one let past another by turning

let f blah ; let g waffle

into

let g waffle ; let f blah

if waffle does not depend on f, or

let g waffle where f blah ; let f blah

otherwise. Degeneration is thus the repetition of this refactoring until the global f falls off the end!

(For data as it is now, you need to generate a bunch of lets for the type, its constructors and its various gadgets.)

In terms of what happens to typedness, we should try to ensure that devaluation cannot increase the amount of brown. Intuitively, removing information cannot increase the amount of stuff which is definitely wrong. Of course, we should expect yellow all over the shop.

I mention this largely because this is pretty fundamental stuff, in terms of the propagation of updates around the system. It’s rooted in the proof engine, below the elaboration layer, so the time to figure it out is now.

Points from today’s meeting:

• darcs is being tested but we’ll hold off using it for epigram for a week or so.
• Still waiting for
• Epigram now has a independent type checker for terms and the parser is connected so that it can be tested out. Consumers of this service to follow. Thorsten questioned whether it was sensible to test it via the parser or whether we should generate terms using quickcheck to test it.
• Wouter has written some haskell to handle expanding includes in Epigram 1. This hasn’t been been hooked up yet
  as it requires some elisping.
• Whilst on the subject of elisp we considered whether it might be feasible to move to GNU Emacs for Epigram 1 as the carbon version for OS X is quite nice.

Turning into code at a whiteboard near you…well, near me, anyway…

There were a few concrete points that did come out of today’s meeting.

Wouter should write a few bits of Haskell to fix Thorsten’s problems using include.

We also need several mailing lists:

• Epigram general e-mail address - epigram-help at epig etc
• Epigram developers - epigram-dev at cs dot nott etc
• Epigram nottingham crew - epigram-notts at cs dot nott etc
• General epigram discussion - epigram at durham etc

All with suitable links on e-pig if it’s relevant.

Conor also showed that lambda abstracting neutral terms requires more work than you might think at first.

After hooking Conor’s dummy elaborator to the bits of my crummy editor, the result is the very first preview of Epigram 2 in action.

The editor doesn’t do much and the elaborator says everything type checks, but it’s a start.

Try:

> cvs update -d
> cd current/src/
> make
> echo 'lam X : * => X' > Lam.epi
> ./epigram Lam.epi


You should see a poorly pretty printed version of the original, with highlighted identifiers on a grey background. Try giving the following commands to the editor:

> down
> right
> left
> up

You should see the focus change as you navigate the abstract syntax tree.

To quit the editor, just type quit.

There’s not much else you can do at the moment. Next on the todo list are better pretty printing and actually being able to request elaboration after filling in a shed.

Last week we went through the brainshitting list we produced in Durham early this year to see where we are and where we should go. A bit delayed here is the commented list:

(more…)

Hank dropped by. I scribbled this.

In a funny mood on Saturday, wrote this. Have several more important things to do, but as displacement activity goes, it could be worse. I recommend this kind of berserking: just typeset a program you happen to have handy, then explain what’s going on. Everyone should try it.

Meanwhile, comments welcome, especially WTFs from those with a more conventional perspective.

First instalment of an Epigram 1 change I’ve been intending to do for ages. Almost no effort required! I’ve fixed things so that variables named but not declared in the premises of a rule get inserted implicitly at the left end of the rule (as James McKinna used to argue) rather than as locally as possible (as Randy Pollack used to argue). vcons now gets X and n implicitly before x and xs; n used to come in the middle, unless you explicitly forced it leftward. Generally, I find that partial applications work more pleasantly more often with James’s convention. You can still force things rightward with an explicit premise (which doesn’t mean the arg has to be explicit).

Anyhow, I imagine this change may cause minor damage. I’ve tried a few examples, and I had to tweak a thing or two: mostly stuff that was a bit chancy anyway and should have been cleaned up long ago. I suggest that regulars try out their favourites and howl if they aren’t readily fixable.

There will be a second and more subtle change: at the moment, uninstantiated metavariables in rules are generalised to yield implicit arguments wherever they end up; these also should be shunted leftward where possible. Probably won’t do any damage, except to code which relies on the current morally random placement.

I don’t think we should generate new binaries just yet; I’ll try and get this cleaned up as soon as possible.

If we want darcs, we need to consider some issues and make sure everyone is happy to make some changes in the way they work on Epigram.

Firstly, why is it a good idea, without getting into CVS bashing?

1. It’s Haskell — thats good politically (we like functional programs), and, maybe even, practically (if it don’t work fix it!).
2. The theory of patches is an good idea. It gives us more control over different versions/experiments/dead ends. Say I had a copy of the main development trunk, but also an experimental version of my own devising, if Conor writes a bug fix on the main version I can (if appropriate) apply that patch to both my versions. If I do some work on a file that breaks the main trunk I need only send a patch to Conor who can propogate the changes through the rest of the system before we make both patches publicly available. I can think of many more such situations. Perhaps you can too.
3. OK I promised no CVS bashing but… wouldn’t it be nice to move files/folders and keep their history (there, I said it).

There is no halfway house here though, we can’t piggy back CVS on DARCS or vice versa… We either twist and get everyone up to speed on the new practices asap or we stick save the wandering around in the dark for a bit but, in my opinion, lose out in the long run.

So what about the practicalities, well anyone with darcs will be able to pull down a copy from the website, from then on we make these changes:

cvs commit
becomes
darcs record
(locally) or
darcs push
globally
cvs update
becomes
darcs pull

Theres a big list of cvs -> darcs translations here. The rest of that page is a good introduction to why DARCS is different, it’s worth a read.

So what about it?

Just to let yiz know, Andres has just sent me our current HCAR entry to update. I’ve put it under cvs here, so we can all tweak it as we see fit.

Here’s a suggestion about how we might replace Epigram’s datatypes by a universe of containers. It’s distinctly undercooked, but we’ll see how it goes. There are lots of design choices, so I’ll try to flag the issues.

We’ll be wanting some sort of

That is, we’re coding up dependent containers with given input and output sorts. Variations: we could use a sequence of input sorts, or just use sums; we could represent sorts by telescopes, rather than types. I suggest that both of these, although they require more work to set up, deliver functionality which is closer to what we actually want to use. But later…

The semantics is hardwired. It’s not an inductive definition, nor should it be. Moreover, I’m only giving the introduction behaviour here; the elimination behaviour will be peculiar, no doubt.
(more…)

Today’s administrative tasks:
1. Rebuild binaries and add platform specific READMEs.
2. Conor is fed up of being the first line of support. We need a tech support mailing list.
3. Libraries need to be made usable by handling working directories and the like.
4. We want GNU Emacs like Agda! (for version 1 (if it’s cheap))
5. There are a few loose ends (Jamesist generalisation etc.) that really should be fixed.
6. We want darcs.
7. We want cabal.

Current thoughts on Epigram 2:
1. We need a sensible experiment to see if STM is a sensible idea.
2. Reflection as a means to program generically with containers.
3. Investigate hs-plugins by implementing Foul. Robert.

Been a bit quiet around here for a while, largely on account of travel broadening the mind. Hopefully, come October, the distractions will be fewer and we can just get on with it. Earlier progress is unlikely, what with reports to write, and the odd paper. No meeting this morning, with Thorsten away and the Ashes and such. Last week’s meeting was quite useful, though, so I thought I’d blog a little.

We had a chat about how the elaborator is likely to work. This involved a certain amount of naming-of-parts, so here goes

• Framework: the language of parametrised and modular metavariables and definitions in which the state of the elaborator constitutes a valid module; some metavariables are attached to computations which explain how they are to be computed, given sufficient information; these computations are the suspended executions of programs written in…[this may not be a good name, although it does resemble a Logical Framework in character, even if its purpose is not exactly the same]
• Blah: the language in which elaboration rules are expressed; Blah’s main constructs are case analysis on the concrete syntax to be elaborated and refinement of a problem into subproblems; Blah has an evolving on-paper syntax which will translate to a combinator library [a toy prototype can be found here ]
• Igor: the program which updates the elaborator state in the light of new information, comprising the implementation of the Blah combinators, the substitution-and-scheduling algorithm ambulando and various other bits and pieces

The object of defining Blah is to provide a means to explain to ourselves and to others what on earth is going on, and why it might correspond to the typing rules. Indeed, Blah programs correspond to syntax directed typing rules in which the flow of information from conclusion to hypotheses and back has been made explicit.

Now, a key question addressed unsatisfactorily in Epigram 1 is ‘what are the types of metavariables?’. We shall clearly need to have at least the types of the Epigram language, in order to express unknown expressions of a given type, but do we need other stuff as well, in order to facilitate elaboration? What do we need to represent? What does the elaborator deliver? Not just terms, but also telescopes (from signatures and left-hand sides) and programming problem refinements (from right-hand sides).

The latter, James and I handled by extending the type theory with types corresponding to programming problems, constructors ‘return’ and destructors ‘call’: it was important to extend the type theory in this way because we needed programming problems to occur in the motives constructed for the ↞ operator, hence in inductive hypotheses etc. Eliminators are emphatically not ‘meta-level’ notions: we program them, as well as programming with them.

But what about telescopes? We need to be able to say ‘a binder comprises a telescope and a body parametrised over that telescope’. Does this mean we need to add telescopes to the type theory, or just to the framework? My suspicion is that we’ll want them in the theory sooner or later. More anon…

In between coats of paint, I’ve managed to get a bit of concurrent editor-elaborator communication going, without possessing either an editor or an elaborator. The fake elaborator I wrote just likes everything and invents nothing, which should serve to let folk fiddle with editing technology. I’m just a-thinking that we should actually figure out how to elaborate module imports (of pre-elaborated objects) before we do anything cleverer. But anyhow, check it out!

James and I have submitted a paper to POPL ‘06, titled Phase Distinctions In The Compilation Of Epigram, all about how we can use an erasure semantics through the identification of compile-time only values.
I’ve also added the sources to CVS. Enjoy…

Been doing a bit of thinking about how to lash the editor and the elaborator together without being too specific about how it’s actually got to work. I reckon the elaborator provides something like

subscribe :: (Response → IO ()) → IO (Request → IO ())

where Response and Request are part of the interface—types of signals from and to the elaborator.

Editors thus explain how they listen and are taught in return how to ask. There is no other way to get a straight answer from the elaborator. Stuff happens, as and when. An ‘editor’ might serve merely to write Responses to stdio and read Requests from stdin.

There is also no reason why multiple editors should not simultaneously subscribe (corresponding either to having multiple users, or to visiting multiple files). The elaborator should broadcast updates to all subscribers, but should respond privately to requests for information. Update responses will carry the name of what’s being updated, so the listener which an editor sends may perfectly well filter out uninteresting responses server-side.

Carry on like this and we’ll be doing eScience!

Peter and I started writing the Scoper earlier. See Scoper.lhs. In particular, check out the definition of Concrete, which is about as simple as it’s likely to get. We’ve suspended any funny ideas about imperative data structures for concrete syntax, but we are using imperative refs for ‘acts of naming’, allowing change of the associated string.

Given some feverish after-dinner hacking with Wouter, we now have scoping for a good chunk of CTerm, including all of CPat, and it seems to be doing the right thing. Our mechanism for accumulating ‘shadows’ is in place, but we haven’t yet implemented anything which might discharge a shadow, so it’s hard to see the point just now.

(more…)