Archive for January, 2007


Nothing will drive you insane like trying to spending over an hour trying to figure out a problem that turns out to be caused by α-equivalence being broken. Broken because some pattern match branches were in just the wrong order.

Still, I think the type inference code is properly handling a monotonically increasing subset of the InforML language. Tomorrow I'm going to try to get polymorphic generalization straightened out.


Pretty-printing lattices

After an hour or so of hacking this morning, things are looking quite good.

InforML with lattice pretty-printing

I just pipe my representation of the lattice to »dot« and then send the PostScript output back to TeXmacs.

Anyway, back to debugging.


Terminal emulation continued

Despite trying various versions of the Mozilla source tree, along with different versions of GCC, I couldn't get any of them to build a working version of »xmlterm«.

However, while attempting to consider my other options, I discovered something that is perhaps even better. When I searched for »terminals« on Freshmeat among the usual suspects, it suggested TeXmacs. TeXmacs is kind of a cross between emacs and a WYSIWYG LaTeX editor, but written in Scheme. And it has a very simple protocol for interacting with other programs. With a few minutes of experimentation I got it to at least start running InforML. It will take a little more work so that it InforML will spit out the appropriate escape codes. But this will be a significant improvement over monospace UTF-8 text.


First run of InforML in TeXmacs

Not bad. Don't mind the »printf« debugging garbage that was produced when inferring the function type. It can only get more beautiful from here!


The future of terminal »emulation«

Is anyone aware of there being a terminal emulator that supports something more expressive than ANSI graphics?

Specifically, it would be nice if there was a terminal that would interpret XHTML with CSS or some subset. I'm not entirely pleased with some of the output I get from the pretty printer I wrote for InforML (though originally for AspectML), and it seems kind overkill to start implementing my own code for flowing text and arranging things in a tabular fashion, when there exists perfectly good software for doing that kind of rendering.

There is something called »xmlterm« as part of the Mozilla source tree, and while Google still knows a few things about it, any trace of its actual development has disappeared from the web. I just tried building the latest Seamonkey with it enabled, but it didn't even seem to attempt to build it. I'm grabbing a significantly more ancient Mozilla release and will see if I can get that working.

This is definitely something I would like to work on when I have more free time, as there really isn't any reason for a more than twenty year-old text-only display protocol to be the state of the art when it comes to command-line interaction.


Mutually recursive functions

Type inference for mutually recursive functions is actually quite a bit more complicated than you would think. For example, while thinking through how to implement mutually recursive functions in InforML, I came across something that I was confused about and wondered how we had handled it in AspectML. I spent some time meditating on the AspectML source and found that it didn't really address the issue. In particular, you can naïvely write

  1. % fun f <a:*>(x : a) = 5
  2. > and g <b:*>(y : b) = f y;

which you would think would be two functions »f« and »g« that given anything return 5. However, these functions are not accepted by the type checker

  1. InferenceProcess Error: Error between [interactive]:0.2-[interactive]:1.22
  2. Error between frontend/to-source.sml:170.78-frontend/to-source.sml:170.85
  3. Non-unifiable type variables: b and a
  4. while trying to unify types b and a
  5. while checking that b is subsumed by a
  6. inside (f y)
  7. inside fun f <(a : *)>((x : a)) = 5 and g <(b : *)>((y : b)) = (f y)

The problem is that AspectML rightful decided that »f« could not be used recursively at a polymorphic type, because it didn't initially know the return type. However, this becomes a problem because the type variable a isn't actually in-scope inside of »g«, that is »f« has an invalid type in a sense that should be a »compiler« error, as is illustrated by this slightly more complex example

  1. % fun f <a>(x : a) = 5
  2. > and g <b>(f : b -> Int) : Int = 5
  3. > and h y = g f;
  4. fun f <(a : *)>((x : a)) : Int = 5
  5. and g <(b : *)>((f : ((-> b) Int))) : Int = 5
  6. and h <(b5933 : *)>(y) : Int = (g f)
  7. TranslateProcess Error: Error between [interactive]:1.1-[interactive]:3.13
  8. Error between frontend/to-source.sml:170.78-frontend/to-source.sml:170.85
  9. Error between frontend/to-source.sml:607.85-frontend/to-source.sml:607.92
  10. toTyp: Could not find type variable a. This should be impossible!
  11. %

Of course, diagnosing the problem is the easy part. The difficult part will be figuring out which of the many possible fixes makes the most sense for InforML.


Constraint solving over a complete lattice.

I'm quite pleased with the progress I've made today on the implementation of InforML. I finally put wrote the code to provide a lattice »model« for the little theorem prover over lattice constraints that is used by the type inference algorithm. Below is a sample session with InforML, making use of the #sublabel meta-declarations. It also shows off InforML's support for UTF-8. I could have also used UTF-8 versions of some of the notation in the input, but I was interacting with InforML via a terminal, rather than an emacs buffer, so it was easier to type the ASCII equivalents.

  1. InforML 0.7 $Id: informl.sml 1576$
  2. [Loading standard libraries]
  3. [Finished loading standard libraries]
  4. % #sublabel Bot, Top;
  5. ⊥ <: ⊤
  6. % #sublabel Top, Bot;
  7. ⊤ < / : ⊥
  8. % newlabel L;
  9. newlabel L
  10. % newlabel Foo where Foo <: (L || Top);
  11. newlabel Foo where Foo <: (L ⊔ ⊤)
  12. % #sublabel L, Foo;
  13. L < / : Foo
  14. % #sublabel Foo, L;
  15. Foo < / : L
  16. % #sublabel Foo, Top;
  17. Foo <: ⊤
  18. % #sublabel Foo, (L || Top);
  19. Foo <: (L ⊔ ⊤)
  20. % newlabel Testing where Testing <: Bot
  21. and Testing :> Top;
  22. Lattice model has become inconsistent!
  23. %

At this point I am quite optimistic about getting a rough version of type inference completed this week. Some of the stuff with regards to modules and signatures could prove tricky, but the rest of it is pretty much transliterating the inference rules I have typeset.