Epilogue

I think this separation of meta-level things with parameters {X.Y.f t1 … tn} and object-level things with arguments is going to drive me nuts. It’s cleaner in some ways: it makes the operational semantics a little cleaner. But it does involve a certain amount of duplicated technology, and it makes quoting data really quite painful. The framework {Fred.vcons X n x xs} is not what the programmer wants to see. I’m going to have a ponder about what gets harder if I collapse the levels…

This page gives the concrete syntax for the framework layer and hence for object files. I’ve now added objects corresponding to datatypes, but I’m not yet computing gadgets. I have implemented the forcing optimization, however. See Datatype.lhs for the code which searches for projections from index values equal to constructor arguments.

I loaded this lump:


*FrameParser> testFrame "Fred"
{A data
  {Nat in *}
  {zero in {Nat}}{suc (n : {Nat}) in {Nat}}}
{B (X : *)data
  {Vec (n : {A.Nat}) in *}
  {vnil in {Vec {A.zero}}}
  {vcons (n : {A.Nat})(x : X)(xs : {Vec n})
    in {Vec {A.suc n}}} }
STOP


The machine correctly figured out how to recover n for vcons and X for both.

Elimination gadgets are next on the hitlist…

More better documentation tomorrow, but I’ve hacked up the abstract syntax and operational semantics of a framework for definitions, holes and modules with parameters. I’ve implemented a parser from a textual format. The abstract syntax uses long names and is fully λ-lifted, whilst the concrete syntax is suitably localised. The code is a bit of a mess, but I’m too tired to tidy it now. I hasten to add that I haven’t got a checker for object files, just a somewhat trusting reader. Of course, in a lazy language, you can cache the semantics on loading the text as long as you promise not to use it until you’ve checked the corresponding syntax…

I’ve built a bit of concrete syntax for ‘object files’, being files packing up the results of elaboration, which live in some kind of framework. The syntax is quite simple

FrameObject := UId Frame

Frame :=

• {FrameObject}Frame
• (UId : Term)Frame
• FrameThing

FrameThing :=

• ⇒ Term : Term
• —
• …

FrameThing accounts for definitions and modules respectively, with holes, datatype bits and such to come in a while. Frame equips these things with parametrization and subobjects. The point is that the subobjects are local yet visible and that common parameters are shared. Note that, provided objects at each level have distinct names, a sequence of UId and a sequence of Term determine at most one thing.

An object file should contain a sequence of FrameObject. We can nest object files if we add a ‘File’ production to FrameThing.

What I need to do now is to implement the construction of the semantic objects from this syntax. With that done, several fronts open simultaneously…

The minutes of the local weekly Epigram meeting

Conor gave us a devloper-website-guided tour of the code as it exists today. Thorsten questioned the abstract style in which Conor programs and the merits of it were discussed. Looking at the code for the first time is a daunting experience as it is very terse and it is difficult to see what is going on. However it prevents the silly mistakes that are easily made in more concrete code where the plumbing is explicit. Conor pointed out that this code is the most recent of many iterations and that the way to understand it is to go through these iterations yourself.

Website and CVS feature requests:
Incorporating output from Programmatica on the blog and in the developer site.
Commit email notification.
ViewCVS/WebCVS or somesuch thing.

Tasks:
Peter - error handling
James - test harness, type-checking
Joel - test harness ← our local quickcheck expert!

Scribbles with vague relevance can be found here. New thinking about organization of holes, that sort of stuff.

What’s happening with these?

It would be nice to have a collection of samples in files, so we can all see the intended form of input, and do automatic testing later. Repeatedly typing in test cases isn’t good.

Can one of you arrange things so repository directory listings can be seen? Ie, it would be nice if http://sneezy.cs.nott.ac.uk/epigram/current/src/ showed a list of files - it makes it easier to wander around. Thanks.

In a fit of anal retentiveness, I’ve spent this morning tidying up yesterday’s developments. In particular, I’ve separated out DeBruijn.lhs as a more generic bunch of utilities. Correspondingly, Scope has become a functor (I’ve also added a constructor for vacuous scopes, as these give rise to optimized execution for λ and cute print forms for ∀ and ∃). For any idiom which counts how many binders you’re under, the operator ‘shiftyMap’ pushes functions inside scopes, doing the right thing. Yesterday’s nu operation has been slightly refactored to make it less value specific. You’ll also be delighted to find that I’ve added a few more comments…

Let’s not use the automatic CVS feed for a discussion about CVS. (If Paul isn’t yet registered to post, we should make this happen.) Meanwhile, I think it’s important to have enough structure to cope with serious forking. Maybe I don’t understand CVS properly, but I don’t think it’s necessarily just a question of the stable version being the last thing tagged ‘release’. I imagine that there may be a number of distinct versions of Epigram floating about, containing incompatible experiments, all of which are of the moment and should be spatially separated rather than temporally. There’s a pragmatic difference between a branch in the development of one thing and the development of two branches of a thing. The current structure allows for the possibility of the latter at the cost of a tiny number of keystrokes

If it looks bad, press ‘Ctrl-F5′

Best that people use the ‘webstuff’ folder newly added to cvs for Blog specific content and as ‘cvs commit’ automatically updates the website this should mean access is instant. Links to things in that folder will start:

http://sneezy.cs.nott.ac.uk/epigram/webstuff

As a reminder of what we are aiming for here is some bullstorming and some brainshitting which might help you understand the whiteboard:

Click for a bigger version

I’ve just created Term.lhs. I’ll be filling it up with glue very shortly.

Will appear as comments to this story, and subsequently in the Side Bar, unless they are uploads to the webstuff folder.

I thought I’d write a post with a URL in it. Epigram currently lives here.

I reckon we should call it Epilogue