Epilogue

The rain inside has stopped, now that the window in the office upstairs has been closed. Meanwhile, we’ve been reconstructing Ecce to have a matriarchal proof state. The file EcceThump.lhs (which we’ll be splitting into more sensibly named and structured pieces real soon now) is where we’re at. Just now, it even compiles. As I write, the ManChap is hacking up the navigation operations. Together, we’ve been trying to figure out the (anti-)progress propagation stuff. We might even have something worth playing with in a day or two.
(more…)

Despite torrential rain outside (and more surprisingly inside) the Epigram team show total commitment to the task in hand.

I’ve been thinking about Epigram back ends again, and come up with this, which I hope will develop into more than just a toy:

http://www.dcs.st-and.ac.uk/~eb/esc.php

It is an implementation of a simple, mostly untyped, supercombinator language with a few bells and whistles for talking to the outside world, separate compilation, arbitrary precision arithmetic etc. Also, following the philosophy that computer programs might be used by other programs as well as humans, it exports an API - the idea would be that Epigram could target this API; the language itself is independent of whatever method Epigram might ultimately use for IO.

(more…)

It think it’s safe to assume the darcs experiment is a success, but I think we’ve been neglecting to think about how the missing pieces fit together — the web site, papers and the building of documentation.

Well, it’s probably time for us to stick our heads above the parapet…

(more…)

This is perhaps the latest in a long line of overdue and underdone documents describing Epigram 2. Check this blog for previous efforts. I’ll put the sources under darcs when there’s a mechanism to link the latest central version to the blog front page.

So far, it’s barely started. At all. What there is tends to concern itself rather more with how one writes sane rules etc, than with the rules themselves. I’ve only done the fragment with Π, to show the approach, which is highly algorithmic, yet (I hope) tolerably readable.

This document will have more authors than me. Ideally, we should be establishing a correspondence between the prescriptions made here and the implementation we generate and document in the EpiTome (the lhs2TeX source of the system). Being a realist, I expect a certain amount of feedback between the two. Indeed, you can tell this has already happened.

I thought I’d scribble a few things down while they’re fresh in my mind. First up, we’re shifting to Tuesday afternoons from next week, to give me time to get here from another country…

The eagle-eyed will have spotted a bit of darcs activity from myself and James C of late, so I painted some of the picture about the new proof state structure, replacing the OLEG-based system we had before.

It’s a bit slippery if you’re not used to it. Here’s the basic grammar:

• thing ::= decl  | defn
• decl ::= uid  : ↓term
• defn ::= uid [thing;*] => status  : ↓term
• status ::= # | ? | ↓term

OK, some explanation is in order. (more…)

James C and I are trying to make some progress on this hierarchical proof state lark. The new file EcceThump.lhs is our working file, but it will eventually get renamed, reorganised etc. Our new data structure seems a little cleaner than the previous one, which I find reassuring. I expect we’ll get quite a lot of this file by cut-paste-refactor from various versions of Ecce.lhs we have lying around. I’ve already ported the resolver from my previous abortive attempt at this. Correspondingly, I’ve been able to write something which claims to be a ‘loader’, inserting a new chunk of proof state (in concrete syntax) at the current cursor. It just trusts the supplier, rather than typechecking anything.

Next up, I’ll be porting the Christener and writing some sort of crude display mechanism, so we can see what we’re doing. Then it’ll be time to write some operations which actually do intros and claim/let in a typechecked manner. After that, we need to implement (anti-)refinement and update-propagation. I’ve already installed some dependency book-keeping, so we’ll see how that goes.

I’ve knocked off the easiest of the jobs below, Scoping now caches the list of things in scope at each node for future use, this is useful for a number of reasons.

I’ve also added a function with the following signature:


colourin :: (Scoper c f x,Traversable f) =>
  c -> x f CName -> x f (CName,NameKind)


what does this mean, well, if you have a p :: CProg (Either CShed) CName

and type

colourin () p

it should annotate the CNames with colours, I hope

No testing has been done so I’ll fix any bugs when I get back next week, there’s still plenty to do but it should help the UI guys show us some good stuff.

We sat in James’s garden, drank bad espresso, and enjoyed the nice weather. We also spent some time talking about the state Epigram was in.

* There appears to be a scoper. It works - i.e. compiles and delivers coloured IORefs.
* TODO Cache scope stack at each node. This should be trivial modification as we’re parametric in the labelling of recursive subnodes. We still need to write something to turn coloured IORefs into coloured Strings, which Joel can render.
* The hierarchical proof state is in pieces on pieces on Conor’s floor. Conor really wants to rethink things before working this out further.
* DONE Name resolution and christening works (more or less).
* TODO Navigation and update of hierarchical datastructure needs serious work.
* TODO Commit mechanism for updating meta variables
* Joel’s been messing about with Gtk2hs. He hopes to have something that at leasts renders concrete syntax by next week.
* How should we organise representation of terms to perform efficient updates?
We may want to design a drop-in replacement for terms in the proof state. We do not want to change values, just the terms. The replacement should support cheap update actions and convert easily between the actual terms. It’s a nice separable job for Wouter.

Once the proof state has been updated, we can work on the theorem prover layer.

Plan of action
James and Conor should work on proof state manipulations.
Peter should continue working on data types.
Edwin was here last meeting. He went away having some clue about the Term data
type. Compilation would be a good thing to have, but requires him having a fair amount of time.

The Epigram meeting went underground today due to the AUT strike. Despite a surprise picketter having taken up temporary residence on Conor’s downstairs sofa we weathered the shouts of “Scab!” and made it safely to Conor’s study.

Topics of discussion:

1. Further consideration of the advice provided to us by team gtk2hs on Friday.
2. Edwin is here and keen to build on his experiment of circumventing ghc’s typechecker to utilise the STG Machine for compiling Epigram programs. Expect further news on this later in the week.

Three things on the slate this week

• Datatypes for OTT: the current implementation loses canonicity if you use the notion of datatype from the pre-OTT days, so we need to bring this up to date. Peter Morris and I have a plan bearing a certain resemblance to what’s going on in the Indexed Containers paper; we also have a longer term plan, with an even stronger resemblance to the same, but that’s another story.
• Hierarchical proof state for Ecce: my Oleg theory of holes has the annoying problem that objects only have private subobjects (within so-called ‘guesses’); subobjects which need to be visible get λ-lifted and exported to the global context, resulting in a flattening of the elaboration tree, a loss of sharing, you name it. Just do a proof-state dump in Epigram 1 (META-RET, then look in *Epigram-bin*) if you don’t know what I’m talking about. So the plan is to do away with guesses in favour of hierarchically stored but fully λ-lifted holes and definitions. With a twist: we use a relative mode of naming, omitting the parameters held in common between reference and referent. So although these things are globally global, locally they look local. Oh, wait and see…
• Dummy elaborator for high-level source code. Joel has refactored the grammar and the parser; Peter has refactored the scoper; we just need to reassemble the pieces we had before and we have a basis to build a real UI. We might have the beginnings of a non-dummy elaborator soon enough too.

…is the new injunction which we shall doubtless take as seriously as we take anything. With that in mind, I have begun to exploit the page facility of this blog to produce some user documentation for Ecce, so that the intrepid might have fun and games of one sort or another. I, er, encourage my fellow developers to keep this stuff accurate, warts and all.

I’ve been thinking for a while that it ought to be possible to get Epigram to write out haskell code for ghc to compile, suitably annotated with unsafeCoerce# so as to get past the type checker. I finally got around to experimenting with this the other day; you can see some of the results here (generated from this).

This code is (mostly, apart from the Haskell interface glue at the top) generated by a tool I’m working on for a completely different reason from my usual noddy test functions: factorial, variadic adder and vector sum. I’ve tested it on some more complex code, but this example (factorial in particular) gives some idea of how fast it goes (about 1 second to compute 9! on my machine). Perhaps if I get a moment later this week I’ll try to make a more interesting program.

(more…)

Needed to do a bit of hacking at the weekend, so I just sorted out the naming mechanism to allow and generate the x^n notation. Try typechecking lam X : * => lam X : X => X and lam X : * => lam X : X => X^1.

Next mission, a very simple interactive editor for proof states, given by (Cursor (Key UId Reference)) for now, but we’ll go tree-structured later. In the first instance, this should just have holes and lets, with refinement and undo as the basic operations. This requires the ability to propagate an update. Before long, though, we’ll want to have parametrised things, and a hierarchical structure. We should be able to knock up a serviceable toy in fairly short order.

OK, I think I have a plan. I’m gonna

• hack in Bool and W directly, leaving ‘data’ alone for the moment
• add the relevant extra eliminators for equations (dom, cod, sym)
• make coe go into functions, pairs and trees
• add a constructor for extensionality

If that works out, it’s time to rethink data, then remove Bool and W. I’ll keep youse posted.

I’m following a plan to get us to stage 2 of the equality story: proof irrelevance. I’ll update this post as I go, but so far I’ve

• split Term into syntactic stuff (still Term) and semantic stuff (new file Value)
• lumped the contents of Equality into Value and removed Equality
• threaded a freshroot through eval and everything which calls it (no fun at all)
• added source and target to coe and coh
• made the computational behaviour of coe and coh compare source with target if the proof isn’t already refl
• made normal proofs of equations equal
• made spine comparison of coe just compare sources and targets, rather than (irrelevant) proofs
• did some very basic testing
• pushed the changes
• gone in search of a drink

I’m trying to keep Epitome sane as I go.

Meeting:

• Thorsten should type:
  1. darcs get http://sneezy.cs.nott.ac.uk/darcs/term
  2. cd term
  3. chmod +x Setup.hs
  4. ./Setup.hs configure --prefix=$HOME
  5. ./Setup.hs build
  6. ./Setup.hs install --user
  7. (and providing $HOME/bin is in your path:) epigram
• The next job in term is to build equality in these steps:
  1. Propositional equality
     
     coersions between equal types (and the proof that these are coherant)
     
     and the structural rule for application
     
  2. Proof-irrelevance for equality, to do this right we need to decide equality during evaluation (if we do not have a proof of an equation but it’s homogeneous, then we win anyway). The upshot is Equality.lhs and eval from Term.lhs need to be in the same file.
  3. Observational equavalence, at some point (sooner rather than later) we’ll include the structural rule for :
     
     Thorsten pointed out that is rule can be derived from substution of equals for equals plus the more primitive:
     
     Having this gives OTT a simpler core, but Conor prefers the first version because it is easier to program with.

I just had the following interaction with the version I just pushed:

*ParseEvalCheckRender> parseit synthit
input:
Nat => => data X : * where <z> : X ; <s> : all x : X => X
two => => <s <s <z>>> : Nat
plus => => lam m => lam n => m elim{Nat} (lam x => Nat)
% n
% (lam x => lam xh => <s xh>) :
% all m : Nat => all n : Nat => Nat
---
plus two two
STOP

<s <s <s <s <z>>>>>
data X : * where <z> : X ; <s> : all x : X => X


Some sort of progress, I think.

1. UI. Some interest from Nick Thomas. Joel is planning an experiment with gtk2hs.
2. Using darcs is working very well. Discussed structure our darcs repos.
3. Status of Epigram 2. We have been hacking the core recently. The afore mentioned ‘Up’ and ‘Down’ terms are in with the supporting parser, (not very) pretty printer,type checker equality checker. Peter has been implementing datatypes. Next is the equality type, and then on to wrapping it in a representation of holes.
4. Thorsten discussed injectivity of type constructors.
5. Move to the board to discuss 3 further. Specifically Conor proposes a short path to making something go. Two main areas: a) Finishing Core and moving on to theorem prover. b) Concrete syntax, comms protocol.

6. Division of work. Joel and Wouter to look at concrete syntax and comms. James and Peter to look at core and theorem proving.
7. The advantages of supporting observational type theory sooner rather than later will afford us simplifications in the implementation. (Thorsten to go into more detail about this on the blog).

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.