I am . . .

bonus (dfw) !

And as an added bonus, here is pretty good commencement speech by David Foster Wallace. Its no "Wear Sunscreen", in that I don't see it being put to music and put on VH1 anytime soon, but its probably bettter than "No Sex in the Champagne Room."

David Foster Wallace, in case you didn't know, is the author of Infinite Jest, a book which I'm still not sure whether was worth finishing (other than to be able to say at dinner, "I finished Infinite Jest.", which is a great test of the people you're talking to, because the right response to this statement really is "Why?").

He has other books as well ("Interviews with hideous men") but those didn't grab me (and drop me) in the same way that Infinite Jest did.

self and virtual types

I've been listening on discussions in the lab lately on handling self types. Sam mentioned something called virtual types. I know nothing about them.

However, I happened to run into an article by Remy and Vouillon arguing that virtual types (or at least common uses of virtual types) do not need special treatment in O'Caml, and gives some example code.

So I want to go back over the article later and really digest what is going on. I followed the argument as presented when I read it directly, but I'm feeling I may have missed the point when they were talking about camels at the end.

larceny unleashed

Last week, Will finally decided it was time to "release" Petit Larceny (as well as the latest build for Native Larceny).

I don't have much else to add to the subject. (other than its not really what anyone is willing to call a formal release; Will calls it a "Developer's Alpha", and I call it "Potentially Unembarressing")

However, it is nice that we've hit this stage.

Next items on my agenda:

• Finish term paper on "Computability and Complexity of Type Inference" (this mostly consists of poking Carl with progressively larger sticks).
• Finish getting NASM support working for Larceny on win32 platforms (so that we can release for windows as well as the current Mac OS X and Sparc).
• Merge the Common Larceny and Petit Larceny (aka release_2) source branches in the CVS repository.
• Start planning out how to implement the Garbage First collector in Larceny's runtime.

garbage collection in cylone

I just read a nice lil' paper that gives me hope for my own research.

It sounds like they put a region system to good use in developing a simple two-space garbage collector.

However, this blog entry indicates that they haven't figured out how to do a generational collector yet, and that they think it might require dependent types. Yowza. I've been thinking about the problem as well, but I never got to the point where it seemed like something that sophisticated would be required. . .

before you die, i'd like to. . .

Here is a page of links on PowerPC assembly programming.

Yeah, I've taken my sweet time getting around to learning ppc asm, so now one must wonder, "why bother?"

No answer.

apple, suicide, and analogies

This is a "fun" posting from 2001.

No, the analogy doesn't entirely stand up on its own. But its still worth considering.

The other issue that some people are talking about is DRM. Is that a driving issue? Its certainly not one that Steve Jobs was willing to mention on stage. Maybe its just paranoia.

"i for one welcome our new intel overlords"

. . . but not really.

Yep, Apple is going to be a Switcher. And I'm somewhat pissed about it.

I really had bought into the argument that RISC processors were the right solution for the long term, and that PowerPC was more scalable than Intel, etc etc. If nothing else, Intel processors meager register set really sucks.

Perhaps the worst thing is that it is going to be very hard to convince anyone to buy a new mac for the next year, at least. Sigh.

The power set axiom and the specification schema

Some people at the lab know that I occasionally (half-jokingly) question the existence of the real numbers and the (informal) validity of a set of axioms that imply that the reals exist.

Most recently I had pinned this down to the powerset axiom in Zermelo set theory. The powerset axiom is: "For any set z, there is a set whose members are just the subsets of z." [ forall z exists y forall x (x in y iff forall w ( w in x implies w in z )) ].

Let me be clear here: I have no problem with the powerset operator being applied to finite sets. I definitely see that for any finite set z, the powerset of z is easily constructed. The questionable part is: why should I believe that the powerset operator is applicable to infinite sets? Given the set of natural numbers N, if we allow the existance of its powerset, 2^N, then there are elements of 2^N that cannot be described by a finite piece of text. Why should we assume that such sets exist?

I recently picked up Boolos' book, "Logic, Logic, and Logic", again, and started looking there for answers to questions I've been having recently about Linear Logic. The first chapter presents "The Iterative Conception of Set", where Boolos describes a staged model for constructing the sets described by Zermelo's axioms (which include the powerset axiom above).

There are a lot of rules for building up these stages, but most of them are straightforward and believable. I skimmed them over, said "okay", and moved on to the next section, which argues that the axioms of Zermelo Set theory follow from the rules given for building the stages. This includes the Powerset axiom; so I was naturally interested in reading this more carefully.

The derivation of the Powerset axiom hinges on the truth of the "specification axioms" of the staged model. When I saw that, I said, "okay, I missed the details of the specification axioms, lets revisit it. . ." It is actually a schema describing an infinite set of formulas that we take as axioms. It is phrased as follows:

"forall s exists y forall x (x in y iff [X] and exists t (t earlierThan s and x formedAt t)))"
where [X] is a formula of in which no occurrence of "y" is free.

As Boolos puts it, "any such axiom will say that for any stage there is a set of just those sets to which [X] applies that are formed before that stage. Let us call these axioms specification axioms."

To derive the powerset axiom, one starts with the specification axiom:
"forall s exists y forall x (x in y iff (forall w (w in x implies w in z) and exists t (t earlierThan s and x formedAt t)))"
which is the same as the above with [X] := "forall w (w in x implies w in z)". This specification axiom says "for any stage, there is a set of all subsets of z formed at earlier stages." (the argument continues from there, but I don't want to relay the remainder of it at this point.)

z is free in the above specification axioms. So it seems that we're actually going to be employing an infinite number of the specification axioms to argue that the powerset axiom is true, since the powerset axiom is quantified over all z; is this okay? Plus, I'm no longer so sure that it is sensible to put no constraints on [X] other than that no occurrence of "y" be free in [X].

But these are pretty flimsy questions; and that's a good thing for me, because it means that I'm narrowing down my uneasiness about the powerset axiom into more bite-size chunks that I can process.

Linear Logic (with urls!)

Girard, 1987. Very hard to read. Found on
Girard's pubs page. Girard, 1995 has a significantly lower barrier to entry.

Lafont's collection. The only one I've skimmed is a Linear Abstract Machine, which isn't even downloadable there.

Another collection

Wadler's collection.

mailman, the return

As the subject indicates, I had a brief reencounter with a prior post today.

Short version of story (which is all I have time for today): when in doubt, check that the qrunner daemon has actually been started.

dlopen on win32 ?

I spent today getting Larceny to build on Cygwin. After I finished getting something that seemd to evaluate simple Scheme expressions, I tried dynamic loading. And it didn't work.

So at last I realized that I had been misinterpreting many of Lars' statements: dynamic loading doesn't work at all on Windows (even under Cygwin, which was the key bit I was missing).

Thus began a huge quest to figure out how dynamic loading works on Windows. Ha. Ha. Ha.

Here are some links I've found trying to explain it to Unix-heads like myself (or just looked interesting as I browsed over the Google output).

• ld and WIN32 (cygwin/mingw)
  
• Windows vs Unix linking dynamic module
  
• Dynamic Linking and Loading
  
• Re: Need internal help please (dynamic loading support)
  
• Enhanced Dynamic Linking for MS-Windows
  
• Dynamic Class Loading for C++ on Linux
  
• C++ dlopen mini HOWTO
  
• User defined main()
  
• RE: Dynamic loading on Cygwin - status
  

I think I need to pay special attention to the "Gimp" solution documented on the EDLL page; I don't mind writing a .def file that has all the millicode routines listed in it.

linear objects

This is just a note to myself to revisit the
following article by Henry Baker:
'Use-Once' Variables and Linear Objects

I really should start making a big list for Stevie and I to go through in preparation for our PL Jr talk.

See also:

• Linear Logic and Permutation Stacks--The Forth Shall Be First
  
• A 'Linear Logic' Quicksort
  
• The Boyer Benchmark Meets Linear Logic
  
• Sparse Polynomials and Linear Logic
  
• Lively Linear Lisp--'Look Ma, No Garbage!'
  

publication pressure

I have to say, I need to try to publish my work more often. (For other than
the obvious reason that I need to publish work, period.)

It really forces you to make everything concrete. To the max.

Almost as much as actually implementing it would.

System F and semi-unification

This is somewhat of a note to myself to revist the responses posted.

I'm not 100% percent sure the original author (Mike) really had a grasp on what he was saying. On the one hand, he wanted to get an intuition as to which programs would be problematic to infer types for. But then he started talking about reducing inference for those problems to semi-unification; that's not the right idea! The idea is that you take a bog-standard undecidable problem (e.g. the halting problem), reduce that to semi-unification, and then reduce the reduction to a sample term in System F.

Of course, this would probably yield a term so complex that it would boggle the mind, and not provide the intuition that he was hoping for.

If, on the other hand, he was just interested in the idea of using a (partial) semi-unifier to (partially) perform type inference for System F, then that's a different story. Hard to tell. But lots of interesting points and links in the responses.

subtextual response

I've been looking at Jonathan Edwards' experimental programming
environment/language, Subtextual

I am semi-underwhelmed. But there are some interesting connections with spreadsheet programming here.

I later read this post from the related Alarming Development blog, and there was one thing there that irk'ed me: the idea that we should embraced copy-and-paste programming.

cut-and-paste programming, I have learned to accept. That's when, if you are tempted to copy-and-paste a snippet of code, you instead cut it out entirely, and then turn it into a seperate subroutine/superclass/unit/module. Then you parameterize accordingly (and of course you are expected to add documentation about the mental model you have in your head about what this piece of code does).

But copy-and-paste is very dangerous. And in fact, in Subtextual, it seems like Edwards has embraced a sort of hybrid between cut and copy, because when you copy subtrees, you don't get a fresh copy immediately; instead you get a tree that is linked back to the original tree, and changes to either will propogate to both. You have a seperate operation, "introduce variant", to actually do the copying in place.

mailman, postfix, and pain

Was up late last night trying to set up a mailman-based mailing list to demonstrate such things to my cousin.

I made much use of this page to figure out how to get the whole thing going. But when I went to bed, the damn thing still wasn't working.

Eventually I figured out that I never actually started the mailman daemon that is in charge of processing information as it comes in. I just figured that apache and postfix would know that they needed to call out to these command line procedures when they got certain inputs (e.g. mail to a particular address). Silly me.

So I was dumped into the sewer of systems administration once again. But I've pulled myself out now; I'm so happy I'm a PL researcher.

Observing Finalizers and References on the JVM

As a followup to clarify my previous comment on this post (since Dave and I discussed this question personally):

Here is an experimental revision of the code that Dave posted; it is meant to demonstrate a number of things. The most important are:

• If you want to really observe a space leak, it is helpful to actually use objects which are large (new int[X] is your friend here).
  
• If you want to really observe a space leak, it (unfortunately) seems like you may have to employ the (non-standard) -Xms and -Xmx options to the JVM.
  
• There are more reliable/sensible alternatives for monitoring whether an object has been collected than attempting to maintain a hashtable of object identifiers. Namely, use of classes in java.lang.ref.*.
  
  
  
  • Having said this, I admit that I do not fully understand the semantics of weak references, because I was not able to naively replace all of Dave's uses of kill(int) with my killAlt(int) procedure.
    
  
  
• Finalizers really are run only once. However, that doesn't always mean that you can't collect an object just because the call to its finalizer makes it live again.
  

I had to backport the code to JDK 1.4 since that's all I have on my poor little Mac OS X box. Sorry. I tried to make the backport clean by using trampoline instantiation of the generic collections rather than cluttering up the code with casts everywhere.

Sample command line invocations of this class:

% java -Xmx1mb -Xms1mb Immortal -dummysize 100000 -num 10

% java -Xmx1mb -Xms1mb Immortal -dummysize 100000 -blowup 10

(Note that due to the braindead way I'm doing argument parsing, the order of the options above is VERY significant).

import java.util.Hashtable;
import java.util.Vector;
import java.lang.ref.Reference;
import java.lang.ref.WeakReference;
import java.lang.ref.ReferenceQueue;

public class Immortal {

    static class HashtableFromIntegerToInteger {
 Hashtable me = new Hashtable();
 public int get(int k) { return ((Integer)me.get(new Integer(k))).intValue(); }
 public void put(int k, int v) { me.put(new Integer(k), new Integer(v)); }
 public void remove(int k) { me.remove(new Integer(k)); }
    }

    static class HashtableFromIntegerToImmortal {
 Hashtable me = new Hashtable();
 public Immortal get(int k) { return ((Immortal)me.get(new Integer(k))); }
 public void put(int k, Immortal v) { me.put(new Integer(k), v); }
 public void remove(int k) { me.remove(new Integer(k)); }
    }

    static class HashtableFromIntegerToRef {
 Hashtable me = new Hashtable();
 public Reference get(int k) { return ((Reference)me.get(new Integer(k))); }
 public void put(int k, Reference v) { me.put(new Integer(k), v); }
 public void remove(int k) { me.remove(new Integer(k)); }
    }

    /** tracks the number of times each finalizer is run */
    // private static Hashtable finalizeCounts = new Hashtable();
    private static HashtableFromIntegerToInteger finalizeCounts = new HashtableFromIntegerToInteger();

    /** used to control object lifetimes */
    private static HashtableFromIntegerToImmortal pointers = new HashtableFromIntegerToImmortal();

    private static HashtableFromIntegerToRef  phantoms = new HashtableFromIntegerToRef();
    
    private static ReferenceQueue refqueue = new ReferenceQueue();

    private static boolean nomesg = false;

    private static void mesg(String s) {
 if (! nomesg) {
     System.out.println(s);
 }
    }

    /** used to generate unique identifier codes */
    private static int unique = 0;

    /** some "large" state so that we can observe blowup */
    public int[] dummydata;
    private static int dummysize = 100;

    public static void killAlt(int id) {
        int finalizeCount = finalizeCounts.get(id);
        pointers.remove(id);
        while ( ! phantoms.get(id).isEnqueued())
        {
            mesg("(alt) trying to kill " + id + "...");
            System.gc();
        }
    }

    /** deletes the object with the given id. */
    public static void kill(int id)
    {
        int finalizeCount = finalizeCounts.get(id);
        pointers.remove(id);
        while (finalizeCounts.get(id) == finalizeCount)
        {
            mesg("trying to kill " + id + "...");
            System.gc();
        }
    }

    // The code from these two methods can't be inlined, because
    // we rely on their stack frame disappearing to prevent the
    // link to the tracked object from persisting.

    public static int makeTemporaryObject()
    {
        Immortal temp = new Immortal();
        return temp.id;
    }

    public static void doSomethingWith(int id)
    {
        Immortal temp = pointers.get(id);
        temp.sayHello();
    }

    /** identifier code */
    private int id;

    private Immortal()
    {
        id = unique++;
        mesg("creating instance " + id);
        finalizeCounts.put(id, 0);
        pointers.put(id, this);
 phantoms.put(id, new WeakReference(this, refqueue));
 int last = dummysize;
 dummydata = new int[last + 1];
 dummydata[0] = 1;
 dummydata[last] = 1;
    }

    public void sayHello()
    {
        System.out.println("hi, I'm number " + id);
    }

    public void finalize()
    {
        mesg("finalizing " + id + "...");
        finalizeCounts.put(id, finalizeCounts.get(id) + 1);
        // clear! *khzh-thump*
        pointers.put(id, this);
    }

    public static void main(String[] args) {

 if (args.length == 0) {
     int id = Immortal.makeTemporaryObject();
     
     // This causes the finalizer to run (in the GC thread.)
     Immortal.kill(id);
     
     // And yet, the object is still alive!
     Immortal.doSomethingWith(id);
     
     // This will now loop infinitely, since the finalizer
     // will never be run a second time.
     Immortal.kill(id); 
 } else { 
     for(int i = 0; i < args.length; i++) {
  if (false) {
      // dummy case for uniform syntax
  } else if (args[i].equals("-nomesg")) {
      nomesg = true;
  } else if (args[i].equals("-dummysize")) {
      int num = Integer.parseInt(args[++i]);
      dummysize = num;
  } else if (args[i].equals("-num")) {
      int num = Integer.parseInt(args[++i]);
      
      for(int j = 0; j < num; j++) {
   int id = Immortal.makeTemporaryObject();
   
   // This causes the finalizer to run (in the GC thread.)
   Immortal.kill(id);
   
   // And yet, the object is still alive!
   Immortal.doSomethingWith(id);
   
   // FSK: alternative variant of kill which uses weak references
   Immortal.killAlt(id); 
      }
  } else if (args[i].equals("-blowup")) {
      int num = Integer.parseInt(args[++i]);
      
      for(int j = 0; j < num; j++) {
   int id = Immortal.makeTemporaryObject();
   
   // This causes the finalizer to run (in the GC thread.)
   Immortal.kill(id);
   
   // And yet, the object is still alive!
   Immortal.doSomethingWith(id);
   
      }
  }
     }
 }
    }
}

"Well-going programs can be typed"

Here is one of the stranger papers I've seen since the Forsythe one:

Well-going programs can be typed

The abstract:

Our idiomatically objectionable title is a pun on Milner's ``well-typed programs do not go wrong' --- because we provide a completeness result for type-checking rather than a soundness result.

We show that the well-behaved functions of untyped PCF are already expressible in typed PCF: any equivalence class of the partial logical equivalence generated from the flat natural numbers in the model given by PCF's operational semantics is inhabited by a well-typed term.

Its got Scott's $D_{\infty}$, PCF, Retractions, PERs, Logical Relations, . . .

And yet the paper itself is 50% tricks with Haskell type classes and GHC extensions.

I think the title is extremely misleading, at least based on my interpretation of the abstract. I thought the title meant: "if your untyped PCF program is well-behaved, then there is some way to add type annotations to yield a well-typed program (presumably with the same behavior)." But abstract semes to really be saying that if you have a well-behaved function, then there is some well-typed function with extensionally equivalent behavior; note the lack of constraint on the form of the typed program text and its relation to the untyped text.

test

My first post. Woot.

Catching up on West Wing. This one has Castro. Lots of Cuban-sounding music in the background. Its kind of like watching The Godfather Part II