Thinking about some things I came upon the following problem.

• Alice knows some set of facts F1.
• Bob knows some set of facts F2.
• Can Alice find out if Bob 's set of facts, F2, contains some fact X that is in her set of facts, F1, without leaking any information about X to Bob?
• Assume that F1 and F2 are sufficiently large that hashing X and then hashing each element of F2 and comparing is prohibitively expensive.
• Also assume that Bob learning that he does not know X counts as leaking information about X even existing.

I'm inclined to believe it is impossible, at least without further constraining the problem.

If there is some way of placing probabilities on whether Bob might know X based upon his knowledge of other facts, it might be possible to solve the problem by asking Bob whether he knows about those other facts. However, that may very well count as leaking information about X: If you ask Bob if he knows three things highly correlated to X, Bob could in turn conclude that you are thinking about X (if he knows it) or that there exists some fact highly correlated to those three things that he does not presently know.

If anyone has figured out a solution to this problem, it is probably the folks working on cryptographic protocols.

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.

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

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

Anyway, back to debugging.

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.

Update:

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!

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.

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

% fun f <a:*>(x : a) = 5
> 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

InferenceProcess Error: Error between [interactive]:0.2-[interactive]:1.22
Error between frontend/to-source.sml:170.78-frontend/to-source.sml:170.85
Non-unifiable type variables: b and a
while trying to unify types b and a
while checking that b is subsumed by a
inside (f y)
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

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

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.

I spent a little bit of time hacking on an InforML »mode« for SubEthaEdit. Partly because I started using it for a remote meeting with Stephanie last week. And the other nice thing is that SubEthaEdit has an option to »Copy as XHTML«, which means that instead of hacking on PHP to get WordPress to nicely display my programs, I can just load them up in SubEthaEdit and just copy and paste. Below is a small sample from the module for booleans (at least as it currently stands). SubEthaEdit's highlighting support is kind of poor however.

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.

InforML 0.7 $Id: informl.sml 1576$
[Loading standard libraries]
[Finished loading standard libraries]
% #sublabel Bot, Top;
⊥ <: ⊤
% #sublabel Top, Bot;
⊤ < / : ⊥
% newlabel L;
newlabel L
% newlabel Foo where Foo <: (L || Top);
newlabel Foo where Foo <: (L ⊔ ⊤)
% #sublabel L, Foo;
L < / : Foo
% #sublabel Foo, L;
Foo < / : L
% #sublabel Foo, Top;
Foo <: ⊤
% #sublabel Foo, (L || Top);
Foo <: (L ⊔ ⊤)
% newlabel Testing where Testing <: Bot
                              and Testing :> Top;
Lattice model has become inconsistent!
%

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.