Archive for February, 2006

This Week

Tuesday, February 21st, 2006

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.


Wednesday, February 15th, 2006

…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.

GHC back end?

Wednesday, February 8th, 2006

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.


Next stop, a wee theorem prover…

Monday, February 6th, 2006

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.