Interpreter 7: Twelf!
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 (more on the problems that caused later.)
As I put at the top of my note to myself, I was using Twelf basically as Prolog-with-types. I didn't prove totality of anything, or prove any metatheorems, and I used at least one red cut (in the form of %deterministic) so there's really no way I could.
Given that, once I was abusing logic programming to write functional code, it was basically a pure functional language, it was most similar in style to Haskell or C++ templates. The fact that the patterns in Twelf have unification variables, which you can repeat to constrain the same value to appear in the input twice, made it superficially feel more like C++ templates, in fact.
Functional programming in a logic lanugage, OR: Negation as failure
Using logic programming to implement functional code has one major drawback: unwanted solutions. When you write a function by clauses in a functional language, EVEN if a particular value can match multiple different clauses in a pattern-match, only the first will ever be used. In logic programming, each such match is a valid solution; the first one is merely the first solution reported. You might naively expect that this would be fine; you just take the first solution and ignore the rest. You would be wrong. You might then revise your naive expectation as follows; as long as the input is _valid_, i.e. there exists a valid solution, take the first solution. You would _still_ be wrong. This problem turns out to be serious and hard to fix. As far as I can tell, the functional-programming idiom of using multiple overlappping cases, most-specific first, is never okay when logic programming, and can only be made okay by using the cut operator (or %deterministic in Twelf) as described below.
First problem: In SML/functional programming, if one of your pattern-match clauses is not total, and executing the clause fails, the program will fail. In Twelf/logic programming, by contrast, if one of your clauses initially matches but then fails later, you'll backtrack and move on to the next matching clause. When working in a functional style, you really just want to unify against the constants on the right-hand side of a rule; you don't want to backtrack past that unification if something fails later. Note that this problem can only happen on invalid input, for a non-total interpreter: the desired behavior is for the program to fail, producing no solutions. So this arguably isn't a very bad problem.
Second problem: If I use a logic programming function to find a value, and then check if that value is true, what I'm _actually_ doing, thanks to backtracking, is asking that function if there is _any way_ to make that value true. This will cause us to enter the undesired cases, if one of those can make the value true (where the desired value is false.) This problem is crippling, but it can be fixed using the cut operator, as implemented by %deterministic in Twelf. There are two steps: 1) Mark the relation with the overlapping cases as %deterministic. This means that, once we've unified with a case, we will never backtrack past that choice (for that invocation of the relation). So as long as we can ensure that we unify with the correct case, we're good. To ensure that, we have to be careful to unify in the correct order, which leads to: 2) when referring to the %deterministic relation, never mention anything in the output but a completely fresh and free unification variable. Otherwise, the output might constrain which case we pick, and we might therefore end up with the wrong one.
An example (imagine this is implementing an object-level eq function, so it better return an object-level boolean):
eq : integer -> integer -> bool -> type.
eq/eq : eq X X true.
eq/ne : eq X Y false.
%deterministic eq.
Now, here is something we must never do:
some_relation/some_case : some_relation X Y X
<- eq X Y false.
Oops! There's an instance for eq X Y false, for any X and Y, even if they are eq! But if we do the following:
is_false : bool -> type.
is_false/f : is_false false.
some_relation/some_case : some_relation X Y X
<- eq X Y Truth
<- is_false Truth.
Now we're good, because of the power of %deterministic. If X and Y are the same, when we unify 'eq X Y Truth' against the definition of eq, we pick the first clause, 'eq X X true'. When we then discover that there's no match for 'is_false true', %deterministic bars us from trying the other arm of eq; instead we backtrack out of some_case, as desired.
This whole issue is closely related to the difficult notion of negation in logic programming. It turns out to be very hard to say "If X does NOT hold, then I want to do Y." Without the cut/%deterministic operator, I don't know how to do it or whether it's possible. And in order to implement overlapping cases with take-the-first semantics, what we need to do under the covers is: if X, do one thing; if Y and NOT X, do another thing, etc.; so negation is necessary. The specific trick of using the cut operator to implement negation directly, which I'm essentially doing here -- since my overlapping cases are "X" and "_", which therefore means "not X" -- is called "negation as failure". It turns out that there's a page on this trick in the Twelf wiki, written by dklee in 2007 (with a promised update "later this evening"): http://twelf.org/wiki/Negation_as_failure.
The rest of it
So other than that, this was a pretty straightforward exercise. Although I wrote almost exclusively in a functional style, the one place I _did_ take advantage of backtracking -- when parsing lists -- was great, and it would be wonderful to be able to write mostly-functionally with a bit of free backtracking search thrown in. (Cue the Haskellers. Or the Racketeers I guess. Or anyone else whose favorite language has this facility. ;-)
A few general notes:
I have now used at least twice a "standard approach" for implementing first-class object-language primitives without first-class metalanguage functions, which is to represent them by stand-in tokens (Prim "foo"), which pass around in a first-class way, and then put special cases for them in the apply function. I suppose in retrospect this is the obvious approach -- in the same way that it's obvious to represent closures by pairs of function bodies and environments, without using metalanguage closures -- but it took me some thought to come up with.
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. (Insert joke about shooting hostages if my demands are not met.) [This demand is not related to working in Twelf; it is related to some other thing I was reading about the usefulness of structured logging.]
I had a good two more instances of "forgot a prime on a variable name" bugs. Whoops. I also had a few "this is hopeless and I don't understand what's going on so I will rewrite the whole thing" bugs, all while trying to do parsing in fancy ways, all of which were before I understood exactly what order the search happens in.
Overall: That was actually really fun. But it took too long... ;_;
Source code: here.
As I put at the top of my note to myself, I was using Twelf basically as Prolog-with-types. I didn't prove totality of anything, or prove any metatheorems, and I used at least one red cut (in the form of %deterministic) so there's really no way I could.
Given that, once I was abusing logic programming to write functional code, it was basically a pure functional language, it was most similar in style to Haskell or C++ templates. The fact that the patterns in Twelf have unification variables, which you can repeat to constrain the same value to appear in the input twice, made it superficially feel more like C++ templates, in fact.
Functional programming in a logic lanugage, OR: Negation as failure
Using logic programming to implement functional code has one major drawback: unwanted solutions. When you write a function by clauses in a functional language, EVEN if a particular value can match multiple different clauses in a pattern-match, only the first will ever be used. In logic programming, each such match is a valid solution; the first one is merely the first solution reported. You might naively expect that this would be fine; you just take the first solution and ignore the rest. You would be wrong. You might then revise your naive expectation as follows; as long as the input is _valid_, i.e. there exists a valid solution, take the first solution. You would _still_ be wrong. This problem turns out to be serious and hard to fix. As far as I can tell, the functional-programming idiom of using multiple overlappping cases, most-specific first, is never okay when logic programming, and can only be made okay by using the cut operator (or %deterministic in Twelf) as described below.
First problem: In SML/functional programming, if one of your pattern-match clauses is not total, and executing the clause fails, the program will fail. In Twelf/logic programming, by contrast, if one of your clauses initially matches but then fails later, you'll backtrack and move on to the next matching clause. When working in a functional style, you really just want to unify against the constants on the right-hand side of a rule; you don't want to backtrack past that unification if something fails later. Note that this problem can only happen on invalid input, for a non-total interpreter: the desired behavior is for the program to fail, producing no solutions. So this arguably isn't a very bad problem.
Second problem: If I use a logic programming function to find a value, and then check if that value is true, what I'm _actually_ doing, thanks to backtracking, is asking that function if there is _any way_ to make that value true. This will cause us to enter the undesired cases, if one of those can make the value true (where the desired value is false.) This problem is crippling, but it can be fixed using the cut operator, as implemented by %deterministic in Twelf. There are two steps: 1) Mark the relation with the overlapping cases as %deterministic. This means that, once we've unified with a case, we will never backtrack past that choice (for that invocation of the relation). So as long as we can ensure that we unify with the correct case, we're good. To ensure that, we have to be careful to unify in the correct order, which leads to: 2) when referring to the %deterministic relation, never mention anything in the output but a completely fresh and free unification variable. Otherwise, the output might constrain which case we pick, and we might therefore end up with the wrong one.
An example (imagine this is implementing an object-level eq function, so it better return an object-level boolean):
eq : integer -> integer -> bool -> type.
eq/eq : eq X X true.
eq/ne : eq X Y false.
%deterministic eq.
Now, here is something we must never do:
some_relation/some_case : some_relation X Y X
<- eq X Y false.
Oops! There's an instance for eq X Y false, for any X and Y, even if they are eq! But if we do the following:
is_false : bool -> type.
is_false/f : is_false false.
some_relation/some_case : some_relation X Y X
<- eq X Y Truth
<- is_false Truth.
Now we're good, because of the power of %deterministic. If X and Y are the same, when we unify 'eq X Y Truth' against the definition of eq, we pick the first clause, 'eq X X true'. When we then discover that there's no match for 'is_false true', %deterministic bars us from trying the other arm of eq; instead we backtrack out of some_case, as desired.
This whole issue is closely related to the difficult notion of negation in logic programming. It turns out to be very hard to say "If X does NOT hold, then I want to do Y." Without the cut/%deterministic operator, I don't know how to do it or whether it's possible. And in order to implement overlapping cases with take-the-first semantics, what we need to do under the covers is: if X, do one thing; if Y and NOT X, do another thing, etc.; so negation is necessary. The specific trick of using the cut operator to implement negation directly, which I'm essentially doing here -- since my overlapping cases are "X" and "_", which therefore means "not X" -- is called "negation as failure". It turns out that there's a page on this trick in the Twelf wiki, written by dklee in 2007 (with a promised update "later this evening"): http://twelf.org/wiki/Negation_as_failure.
The rest of it
So other than that, this was a pretty straightforward exercise. Although I wrote almost exclusively in a functional style, the one place I _did_ take advantage of backtracking -- when parsing lists -- was great, and it would be wonderful to be able to write mostly-functionally with a bit of free backtracking search thrown in. (Cue the Haskellers. Or the Racketeers I guess. Or anyone else whose favorite language has this facility. ;-)
A few general notes:
I have now used at least twice a "standard approach" for implementing first-class object-language primitives without first-class metalanguage functions, which is to represent them by stand-in tokens (Prim "foo"), which pass around in a first-class way, and then put special cases for them in the apply function. I suppose in retrospect this is the obvious approach -- in the same way that it's obvious to represent closures by pairs of function bodies and environments, without using metalanguage closures -- but it took me some thought to come up with.
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. (Insert joke about shooting hostages if my demands are not met.) [This demand is not related to working in Twelf; it is related to some other thing I was reading about the usefulness of structured logging.]
I had a good two more instances of "forgot a prime on a variable name" bugs. Whoops. I also had a few "this is hopeless and I don't understand what's going on so I will rewrite the whole thing" bugs, all while trying to do parsing in fancy ways, all of which were before I understood exactly what order the search happens in.
Overall: That was actually really fun. But it took too long... ;_;
Source code: here.