Epilogue

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.