Archive for January, 2005

framework paranoia

Sunday, January 30th, 2005

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…

object files and datatypes

Saturday, January 29th, 2005

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…

Progress towards object files

Wednesday, January 26th, 2005

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…

Towards Object Files

Tuesday, January 25th, 2005

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…

Minute Man

Tuesday, January 25th, 2005

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!

Ivor Notion

Tuesday, January 25th, 2005

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

Test cases

Tuesday, January 25th, 2005

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.

src on web

Monday, January 24th, 2005

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.

A spot of tidying

Monday, January 24th, 2005

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…

CVS Structure

Saturday, January 22nd, 2005

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

The new style

Friday, January 21st, 2005

If it looks bad, press ‘Ctrl-F5′

Uploading Blog Content

Thursday, January 20th, 2005

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

Durham (11/01/04)

Thursday, January 20th, 2005

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

Durham Whiteboard Thumb
Click for a bigger version

Term.lhs

Thursday, January 20th, 2005

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

CVS Updates

Wednesday, January 19th, 2005

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

More garbage

Wednesday, January 19th, 2005

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

The name of this page

Wednesday, January 19th, 2005

I reckon we should call it Epilogue