|
Reproduced from feedback that I gave pg on an earlier draft (omitting things he seems to have addressed): When you say, > But I also believe it will be possible to write efficient implementations based on Bel, by adding restrictions. I'm having trouble picturing what such restrictions would look like. The difficulty here is that, although you speak of axioms, this is not really an axiomatic specification; it's an operational one, and you've provided primitives that permit a great deal of introspection into
that operation. For example, you've defined closures as lists with a particular form, and from your definition of the basic operations on lists it follows that the programmer can introspect into them as such, even at runtime. You can't provide any implementation of closures more efficient than the one you've given without violating your spec, because doing so would change the result of calling car and cdr on closure objects. To change this would not be a mere matter of "adding restrictions";
it would be taking a sledgehammer to a substantial piece of your edifice and replacing it with something new. If closures were their own kind of object and had their own functions for introspection, then a restriction could be that those functions are unavailable at runtime and can be only be used from macros. But there's no sane way to restrict cdr. A true axiomatic specification would deliberately leave such internals undefined. Closures aren't necessarily lists, they're just values that can be applied to other values and behave the same as any other closure that's equivalent up to alpha, beta, and eta conversion. Natural numbers aren't necessarily lists, they're just values that obey the Peano axioms. The axioms are silent on what
happens if you try to take the cdr of one, so that's left to the implementation to pick something that can be implemented efficiently. Another benefit of specifying things in this style is that you get much greater concision than any executable specification can possible give you, without any loss of rigor. Suppose you want to include matrix operations in your standard library. Instead of having to put an implementation of matrix inversion into your spec, you could just write that for all x, (or
(not (is-square-matrix x))
(singular x)
(= (* x (inv x))
(id-matrix (dim x))))
Which presuming you've already specified the constituent functions is every bit as rigorous as giving an implementation. And although you can't automate turning this into something executable (you can straightforwardly specify a halting oracle this way), you can automate turning this into an executable fuzz test that generates
a bunch of random matrices and ensures that the specification holds.If you do stick with an operational spec, it would help to actually give a formal small-step semantics, because without a running implementation to try, some of the prose concerning the primitives and special forms leaves your intent unclear. I'm specifically puzzling over the `where` form, because you haven't explained what you mean by what pair a value comes from or why that pair or its location within it should be unique. What should (where '#1(#1 . #1))
evaluate to? Without understanding this I don't really understand the macro system. |
Representing code as linked lists of conses and symbols does not lead to the fastest compilation speed. More generally, why should the language specification dictate the internal representation to be used by the compiler? That's just crazy! When S-expressions were invented in the 1950s the idea of separating interface from implementation was not yet understood. The representation used by macros (and by anyone else who wants to bypass the surface syntax) should be defined as just an interface, and the implementation underlying it should be up to the compiler. The interface includes constructing expressions, extracting parts of expressions, and testing expressions against patterns. The challenge is to keep the interface as simple as the interface of S-expressions; I think that is doable, for example you could have backquote that looks exactly as in Common Lisp, but returns an <expression> rather than a <cons>. Once the interface is separated from the implementation, the interface and implementation both become extensible, which solves the problem of adding annotations.
This paragraph contributed a lot to my understanding of what "separating interface from implementation" means. Basically your comment is spot on. Instead of an executable spec, there should be a spec that defines as much as users need, and leaves undefined as much as implementors need.