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…
I’ve experimented with a version where the object-level notion of spine is used at the meta-level. It makes several things a lot cleaner, but a few things a bit slippery. The object-level spines aren’t just applications, you see: they’re projections and explicitations and goodness knows what. So you need some extra information to turn a sequence of values into a spine. Fortunately, the technology for that is the same technology you need to decompress optimized data structures. Hmmm.
OK, we’re back where we were, only a lot of pointless code has been thrown out the window. I’ll update the page when I get a mo, but the changes to the syntax are fairly small. The parameters to meta-level objects are now discharged using the ordinary ∀, so you write their arguments to the right of the {X.Y.f} leaving only the long name. Har har, it turns out that for framework definitions, syntax is the best semantics: simply by abstracting the named parameters as deBruijn indices, you get the term to eval when enough environment has shown up; non-fully-applied framework definitions don’t reduce, although they’ll be eta-expanded where necessary for equality.
So we’re not far off the point where a file containing a module of splurged-out definitions can be reloaded without rechecking. I don’t think it would be so terribly tricky to splurge out Haskell programs which get compiled instead of TT terms which get interpreted…
The good news is that the framework data structure and mechanisms seem (almost suspiciously) simple. The next incarnation of Igor, lurching round the framework with his finite map of updated references, should not be too big a deal.
Just a couple of things about the page.
For the stuff in curly braces it isn’t very clear (well not to me anyway) whether there should be one or more, zero or more of anything and how many levels of bracketing there should be.
Also could you change the colour of the text ‘cos when I printed it out it my machine reverses the colours and comes up with a faded grey which is difficult to read.
Cheers.