Interpreter 7: Twelf!

[nalintmo]

I am pretty excited about my Twelf Lisp interpreter. It slices, dices and even parses! I decided to do a parser because it seemed like it would be easy with logic programming (free backtracking!) I am taking slight advantage of the logic-programming features for the list case of the parser, but mostly I ended up just writing in a functional style (

Comments

[wjl]

I look forward to reading this report more closely tomorrow -- it sounds like you had some good times :D

For now though:

implementing first-class object-language primitives without first-class metalanguage functions

I think you made biscuits defunctionalization.

(NB: i think you'd actually get a kick out of that Reynolds paper!)

[gwillen]

How interesting. I seem to have sort-of-done this. I only defunctionalized the primitive functions; user-defined functions were still implemented as closures, and the closures themselves were first-class. For primitive functions this wasn't possible in the absence of first-class metalanguage functions, so indeed defunctionalization sounds precisely like what I did to them.

[zahariel]

I'm suspicious of your implementation of not-env-has. Does this usage actually constrain K1 to be different from K? If not, not-env-has is (trivially) provable for all env and K. I'm not sufficiently familiar with twelf, and none of your test cases are complicated enough to encounter a problem here, if in fact it is broken. Also it really looks as though ctx-lookup is trying to look in the global environment before the local one, mitigated by not-env-has not actually working.

[gwillen]

Not-env-has is indeed broken. Dklee noted this on twitter, but I guess not here. I wrote it before I figured out negation-as-failure, and forgot to go back for it. The order of lookups is definitely also backwards, whoops.

[wjl]

Extending my demand from the other day that languages should have built-in prettyprinting and built-in logging: I extend it to demand built-in serialization and deserialization of positive types, and built-in structured logging built on that.

I don't know about logging, but O'Caml with Jane St's sexp syntax extension lets you do something like:

type exp = IntExp of int
| AddExp of exp * exp
| MultExp of exp * exp
with sexp
and get, for free, a variety of functions like sexp_of_exp : exp -> Sexp.t and exp_of_sexp : Sexp.t -> exp, and sexp's are the usual LISPy dealies that have various parsers, pretty-printers, and serializers inside the Sexp module.

Programming with this facility is really a joy for debugging, and i imagine it would be great for logging, too.

[gwillen]

Nice! That's exactly the kind of facility I'm talking about.

[wjl]

Yeah, I wish such things were more universally available, or perhaps more universally recognized as necessary. I guess Haskell has "deriving Show", which is probably roughly as good as "with sexp". Well, being structured is also pretty important -- "with sexp" serves an interesting in-between use case, offering a view that's more structured than flat strings but less structured than the original datatype itself.