Methods Methodical

The last couple of posts have been a bit off topic (where topic = Mix), so let's get back to it. These words are about methods in Mix, how they are implemented, and how the implementation choice corresponds closely to the language's semantics (which seems like a bad idea, but you'll see what I mean).

So, first let me note that, in the spirit of object orientationification, in Mix the goal is that every first class entity is an object. By this I mean that numbers and strings are objects, class instances are objects, instance methods are objects, and functions in general are objects. These are all first class entities, so they're objects; since classes are not first class (you can't go passing around classes, unfortunately, at least at this point) they aren't objects, and in fact they don't have any runtime representation.

It's easy to see how regular class instances are objects (it's by definition, right?), but perhaps slightly less clear what I mean when I state that, say, a function is really an object. All I mean is that a function is an instance of a class that has a method op(). This gets us into a bit of a loop; if methods are objects, then this method is an object as well. So, at the bottom we need to have some notion of a callable object; a "special" object with no methods at all. From the programmers perspective these can be ignored, because a callable object can always be treated as an object with an op() method that is callable.

So, methods are really just function objects; sounds great, very symmetric. Now, we have a question to answer: do these function objects take this as an argument, or do they contain a reference to this that is bound once and for all when the function object is instantiated? It turns out that this choice will dictate the semantics and correctness of certain kinds of statements, and so we should try to make a reasonable and (hopefully) reasoned choice.

Consider the following Mix code, which defines a class implementing ToString, and then derives from this a class that does not override ToString. Finally, it adds a ToString method to an instance of the derived class. Assume that print just takes a string and writes it to standard output.

class Base
{
  ToString(){ return "Base!"; }
}

class C : Base
{
  public var Name;
  new(n) { this.Name = n; }
}

Int main()
{
  var c = new C("Bob C.");
  var f = c.ToString;                  // (1)
  
  c.ToString = function(self)
    { return self.Name + " " + f(); }; // (2)
  c.ToString = function()
    { return c.Name + " " + f(); };    // (3)
  
  print(c.ToString());                 // (4)
  
  return 0;
}

In this code there are a few issues. First, at point 1 we store a reference to the original value of c.ToString (which is more or less B's implementation of ToString). I think it is clear that we want f to contain a function object that takes 0 arguments (so that later we can write f() and get the same result as if we wrote c.ToString()); this implies that the function object implementing c.ToString has c (or this) bound as a member variable, and does not take it as an argument.

Then, at point 4, we use the new method in the same way as we used the original one; we aren't obligated to pass c to the new ToString method.

Next, check out points 2 and 3, which highlight the difference between the two treatments. In the first case we get explicit access to this (though without some syntactic sugar we can't name it the keyword this, and so give it a different name). In the second we only have access to this (actually c) because it is contained in an outer scope. While at first glance they seem equivalent, they aren't quite the same.

To see the difference, consider this function that, given a function object (which should correspond to a ToString method), returns a new method that annotates the output of the given method with the operated-on object's Name field:

function annotate(f)
{
  return function(self)
    { return self.Name + "(" + f() + ")"; };
}
o.ToString = annotate(o.ToString);

While this works under the interpretation higlighted by point 2 above, it would not work under the interpretation shown in point 3:

function annotate(f)
{
  return function() { return X.Name + "(" + f() + ")"; };
}

The question is, "What is X?" One answer is that we can work around the issue by passing this (or at least, the object that correspond to it) to the scope enclosing the new method's definition:

function annotate(o, f)
{
  return function() { return o.Name + "(" + f() + ")"; };
}
o.ToString = annotate(o, o.ToString);

So we don't gain expressivity going the second route, though we do perhaps lose code clarity. And in fact, this seems to be exactly how it works in Python:

class Foo:
  __init__(self, i):
    self.I = i
  
  Get(self):
    return self.i
    
f = Foo(7)
f.Get()  # = 7

g = g.Get
f.Get = lambda: g() + 1
f.Get()  # = 8

f.Get = lambda self: self.i
f.Get()  # Error!

Anyways, if they are kind of the same, but kind of not, then where does the real difference reside?

One important point is that the first route allows us to use a single function object instance as a method on many instances regardless of whether the function object needs to access this, while the second option only lets us reuse a function object if the object does not access this. That is, under the first interpretation many instances could share a single function object as a method.

However, a caveat: the "workaround" described for the second situation has a small "strangeness", in that because the variable holding the equivalent of this is captured it could be updated, but only in by the directly enclosing scope.

All of this leads me to a decision.

• Since at the outset a new function object instance is created whenever the containing class is instantiated, it seems more symmetric to use the second route (which would in general encourage always creating a new function object instance when setting an object's methods).
• Since method use doesn't require this to be passed explicitly, and since method definition within a class also doesn't require it, then method definition from outside of a class should not as well.

There is also a second, simpler issue here as well. In point 2 notice that we really do have access to this; does this mean that under the first interpretation we should at this point have access to the private members of this, and therefore the private members of c? I am inclined to believe that we should not: private should have a lexical meaning, which is that only code lexically within the class, or lexically within a derived class, whould have access to said members. What's, more, this is in keeping with the choice made above (that is, as we've picked the second interpretation, we don't even face such an issue).

Furthermore, it would produce a asymmetry between function objects intended to become methods, and those intended to be simple function objects, which could only be solved with more syntax. Namely, it would allow a function object's body to access the private members of an argument only when the function object was intended to become a method; we would need to require that in such cases the argument be made explicitly this. Anyway, lot's of special casing for an idiom that could lead to some seriously obfuscated code.

Time

Time has passed quickly, and my posts have been infrequent of late. That's because I have been busy with a couple of things. Apologies all around.

First, I've been working on a method of implementing the dependently typed lambda calculus via compilation. Specifically, I've been looking at how to compile (or translate, if you like) Logical Framework specifications to lambdaProlog, a higher order logic programming language with at least one efficient compiled implementation (Teyjus, which I have worked on during my undergraduate and graduate studies; there are probably more).

Programming with LF is usually achieved by encoding judgments as dependent types and then searching for inhabitants of particular instances of these type families; I won't go into detail, but instead point you towards the excellent LF implementation Twelf, which does many things, including allow you to program in this way. My implementation is organized around compiling an LF specification to a lambdaProlog module, and then querying that module to find inhabitants of particular types.

Second, my friend and colleague David Baelde has recently begun a year long post-doc at the University of Minnesota (which is where I am), so we've been finding him a place to stay and what not, as well as working away (on, amongst other things, a proof that the translation I mention above is correct).

But, now things are settling a bit, and I should have time to write more about Mix -- I'll have to if I want to write a thesis proposal on the ideas I've been describing.

Thank _____ for Static Analysis

Once I talked about why I think static typing (and more generally static analysis) can be really useful, even if I didn't say much. Today I was working on some code and was reminded yet again that, in some cases, without static typing all would be lost, and I would fall into a dark insanity, never to be lucid again.

The code is that of the Tac system, a "framework for implementing and interacting with interactive theorem provers". Originally it was conceived of as a generic tool with which you could develop first an interactive prover for a linear logic, then one for a classical, then another for an intuitionistic logic, all as easy as something relatively... un-difficult. As it stands we have fully developed one such prover, based on the logic µLJ, a first-order logic with (mutually recursive) definitions, induction and coinduction, and generic quantification.

Like Coq, Tac is a tactics and tacticals based prover, in which you manipulate logical sequents by applying tactics (possibly tactics composed of tacticals and tactics) to them. These tactics can be very low-level (a tactic for right conjunction elimination, say), or more complex (a rule for applying some hypotheses to a lemma). In addition, there's a tactic implementing automatic proof search based on focusing which can finds proofs that require nested inductions and coinductions by automatically generating invariants.

To give you an idea of how working with the system might work, here's a proof script showing the process of first defining the natural numbers, defining the even numbers, and then proving that 0 is even (yes, a silly proof) by first unfolding the definition of even, then picking the left branch, and finally recognizing that 0 does in fact equal 0.

#define "nat x := x = 0; sigma y\ x = s y, nat y".
#define "even x := x = 0; sigma y\ x = s s y, even y".

#theorem even_0 "even 0".
mu_r.
left.
eq.

We've also spent a lot of time working on implementing automatic proof search via focusing. Here's a slightly more interesting proof using automation, showing that if x is a natural number then either it is even or its successor is even:

#theorem even_nat "pi x\ nat x => (even x; even (s x))".
prove.

Not an interesting script though.

Anyway, one standard way of implementing such a system is through higher order functions and success and failure continuations (that paper, by Elliott and Pfenning, describes it in the context of logic programming search, but as it is powerful way of implementing backtracking search, it's what we want). The idea is that a tactic is just a function that takes a sequent, a success continuation, and a failure continuation. If application of the tactic on the sequent succeeds, the success continuation is called with the results of the application (more sequents). Otherwise, the failure continuation is called. Tacticals are functions taking possibly several tactics (a list of them, even) and returning a single tactic. Sometimes we have tacticals taking tacticals returning tacticals, and on and on. Lots of useful composable tacticals for doing all kinds of stuff -- the automatic proof search tactical is (more or less) just composed out of simpler tactics.

The point is, after all is said and done, we end up with some fairly complex code. Some of the types defined in the source are third and fouth order, to say nothing of those of the various helper functions whose types are inferred. Working with such complicated code can be pretty hairy, but with O'Caml's type system we've found it relatively easy to work with.

Now, you might say "you're doing it wrong" (I mean come on, fourth order functions?) But let me motivate the design of the system as it stands. First, the tactics and tacticals method of interactive theorem proving has demonstrated its merit in several other systems, so we'll not find a serious case of "doing it wrong" here. Second, the success and failure continuation based approach is, as mentioned, a powerful and elegant way of implementing backtracking search; it's efficient, because all calls are tailcalls, once you wrap your head around the technique it's easy to write new tacticals to compose various tactics correctly, and it cuts the crust off your toast.

Anyway, the point is that while I don't bother about types when writing Python scripts for a MUD I wrote, and I don't even use them to great effect in some of my other projects, sometimes they really are a ____-send.

Postscript 1: fill in the blanks as you see fit.

Postscript 2: Here's an example of the kind of proof that Tac can find; this one is of the fact that "less than or equal to" is transitive. The proof is presented in outlined form, where asynchronous phases are compressed. Click it for a better view.

Clarity

So, last time I said "the invocation n.Foo() will raise a null pointer exception", which it will of course, but in the more complete example involving Length no such exception could ever be raised: the body of the while loop was guarded by a test to determine whether current was null. Duh.

The point is, it seems that some simple form of nullness analysis would completely eliminate the problems with null that I talked about previously. But, I also said that such an analysis has its own problems. The thing is, this kind of analysis isn't simple after all. Consider:

test(n)
{
  if(n is null)
    return 42;
  else
    return 17;
}

main()
{
  var n = null;
  
  if(test().IsPrime())
    n.Blah();
}

This is a relatively simple (though convoluted) example, but it should illustrate the idea: to get "perfect" nullness analysis in we would need to actually run the program (to determine whether the number is prime using the definition of IsPrime). This is something we really don't want to do (there goes any hope of a termination proof, for one thing). What if the code needs to ask the internet whether the number is prime? All kinds of chaos.

Perhaps a better idea is a very naive nullness analysis, one that only recognizes explicit guards of the form if(something is not null) { ... } or similar. Under such a system, if something had an empty typeset (indicating that it is always null), then the body of the if statement would not be examined. Then, unguarded method invocations on objects with empty typesets could raise a warning.

This would yield more accurate types during inference, and would limit the number of spurious warnings. The latter aspect should be obvious, but the former might not be as clear. Consider:

main()
{
  var n = null;
  var g = 42;

  if(n is not null)
  {
    n.Bleck();
    g = new Foo();
  }
  return g + 7;
}

Let's assume that Foo does not implement operator+. With the simple form of nullness analysis described above, this code typechecks correctly: g is never assigned to an instance of Foo, so its typeset contains only Int[] (which does implement operator+). Without nullness analysis, the invocation n.Bleck() would generate a warning, and the expression g + 7 would generate an error. Here nullness analysis (or nullness inference, as the Nice people call their version of it) is acting as a kind of poor-man's dataflow analysis.

We still need to analyze such a technique for correctness. For now I'll handwave it away; I've got work to do.