Lambda the Ultimate

I hate to be trite, but really, aliasing is the bane of imperative programming. There are a tremendous number of optimizations that simply aren't possible because of aliasing, and a good deal of static checks too. Perhaps you missed the significance of the given example: determining when a resource is being used properly. If two different pieces of code hold a reference to a file, and one of them closes it, the other doesn't know that the file is no longer valid to access without performing a check every time first. On the other hand, if it were statically impossible to access a file after it was closed, then a whole range of runtime checks and problems could simply be eliminated. I think that's *huge*.

Unfortunately, I think linear types look too bulky to become popular in practice, but this paper is a stepping stone towards a production-ready mechanism of encoding stateful information in types. In C++, the idiomatic way to handle this resource usage is to use something like a shared pointer with custom deleter, where the last pointer to the resource cleans up the resource (closes the file). The problem with this technique is that it requires all the space and time overhead of the shared pointer (which, fortunately, is not particularly exorbitant, but which would still be nice to eliminate).

The other thing you might be missing is the implication for storage management. Aliasing is the sole reason that memory management is hard. If there were never more than one reference to a given storage area, you would only need to track the lifetime of that one reference to determine when the storage can be reclaimed. It is the fact that multiple aliases with different lifetimes can access the storage that we must resort to techniques like reference counting and garbage collection. Reference counting is an explicit demonstration that aliasing is a computationally pervasive cost. And if you don't think that reference counting is popular, just look at COM.

Now, what if linear types gave us a way to *statically determine when storage can be reclaimed*?? Wow! Then you have another mechanism like region inferencing for performing compile-time memory management, thereby avoiding the cost in rc *or* gc! I hope that the magnitude of this possibility is not lost on you. GC today is "good" to "pretty good", but A) it still has a cost, no matter how you do it, and B) almost all GC is *conservative*. That is, there will be some storage regions that are semantically dead but held alive by a reference. If we could statically determine that more regions are semantically dead because those references are no longer used, then we would have even better storage reclamation.

To get back to the title of my post, the reason aliasing is so popular in many languages, despite the difficulties it can bring, is because it's also extremely useful. So aliasing itself isn't going to go away any time soon. The FP solution to aliasing is to make it a non-issue by preserving referential transparency. However, that has an associated cost as well.

Now, what if linear types gave us a way to *statically determine when storage can be reclaimed*??

The Clean compiler has such an optimisation (using uniqueness types which are related to linear types).

Now, as is often the case, this optimisation may interfere with other optimisations.
For example the technique described in
Haskell on a Shared-Memory Multiprocessor (Tim Harris, Simon Marlow, Simon Peyton Jones) is not immediately applicable because memory space for immutable objects may now be overwritten by other objects.

It was my understanding that uniqueness types and linear types was the same thing. Could you please expand on the diffrence, or give some pointers?

See the intro of Erik Barendsen and Sjaak Smetsers
Uniqueness typing for functional languages with graph rewriting semantics,

If you follow my post above more closely, you will see that there is a solution which allows aliases to exist, but also preserves the program's correctness, including state of storage.

Non-nullable pointers and linear types are special cases of the solution of the problem of state correctness, to which I think a solution exists.

Your "solution" is to enforce the runtime checks that already exist and must be written manually to deal with aliasing issues. My "solution" is to eliminate the need for checks at all. The difference is that annotations can only enforce local invariants and preserve local information. What annotation are you going to specify that says: "This file can only be opened if it is closed, and closed if it is open"? Consider the case of a database engine where several different query objects need access to a file and have different lifetimes.

On the other hand, types which allow you to perform inference over a whole program can, in some instances, allow you to eliminate entirely the runtime checks which appear in your annotated code. That is less code to write/generate, less code to execute, and less code to maintain. Where I come from, that is an unequivocal Good Thing(TM).

What annotation are you going to specify that says: "This file can only be opened if it is closed, and closed if it is open"?

Currently working on it and I have good reasons to believe that it's possible, with a good programming language.

A key to this would be, for instance, to have a different type for an opened file and a closed file.


file_open: closed_file -> open_file
file_open_rw: closed_file -> open_file_rw
open_rw_as_open: open_file_rw -> open_file
file_close: open_file -> closed_file

Etc.

On this topic, see also Microsoft Research's Vault or Naoki Kobayashi's TyPiCal & Resource Usage Analysis.

Is not hard to this with with phantom types, I posted one (ugly) way to do it on fa.caml last February. The posted the 'close' function does type if you eta-expand it). Its not really satisfactory though, because you have to jump through hoops to localize your effects.

Do you have some documentation about this ?

From Phantom Types:

We create a Parameterized type in which the parameter does not appear on the right hand side.

Thanks. Lucky for me I'm working on something more generic, otherwise I'd have been busted.

But I am happy I am not alone in this pursuit.

You said that:

"Your "solution" is to enforce the runtime checks that already exist and must be written manually to deal with aliasing issues

Not at all!

first of all, all the checks I am proposing are not done at run-time, but at compile-time.

Secondly, I do not propose to write them manually, but to have the compiler infer them from the code. The programmer would only have to write the logical requirements.

My "solution" is to eliminate the need for checks at all.

But your solution works in a very limited scope. My solution is general, and accounts for all logical problems. In fact, my solution is the "missing link" of programming: the declaration of requirements along with the implementation.

What annotation are you going to specify that says: "This file can only be opened if it is closed, and closed if it is open"?

Hey, it's very easy. Example in C-like syntax:

FILE CreateFile() -> {closed} {
    //bla bla create file object
    return file;
}
FILE OpenFile(FILE file -> {closed}) -> {open} {
    //bla bla open file
    return file;
}
FILE CloseFile(FILE file -> {open}) -> {closed} {
    //bla bla close file
    return file;
}
void ReadFile(FILE file -> {open}, byte[] buffer) {
    //bla bla read file
}

It's very easy to see from the above that:

• when a file is created, its state is closed.
• when a file is opened, its state is open.
• before a file is opened, it must be closed.
• before a file is closed, it must be open.
• before a file is read, it must be open.

The above can be checked mechanically by a compiler. If only APIs came together with their requirements, programs would be of much higher quality.

That is less code to write/generate, less code to execute, and less code to maintain. Where I come from, that is an unequivocal Good Thing(TM)

I couldn't agree more. That's one of the reasons I post here.

This sounds (to me, anyway) a lot like Design by Contract implemented as static analysis, which is what SPARK-Ada does. Having said that, I've never actually done any SPARK programming, so perhaps I'm off base here.

I thought through this possibility myself before spotting the problem. Without linearity, consider this code:

void write(FILE f)
{
    WriteFile(f, "Hello, world.");
}

void write_n_close(FILE f)
{
    WriteFile(f, "Goodbye, world!");
    CloseFile(f);
}

FILE file = OpenFile("foo.txt");
if (getchar() == 'x') write(file);
else write_n_close(file);
write_n_close(file);

Now, consider that you can't statically determine whether the second invocation of write_n_close() will fail or not. The conservative thing to do would be to forbid it, but that would also make most code unwritable. This is why I said that you must introduce runtime checks. There's a few problems. One is copying, naturally. The other is dataflow analysis. Trying to find all possible paths through the code statically to make sure the invariants are preserved is going to be exponentially hard (or worse) in many cases.

That's why the linear types were introduced. By controlling copying, you can limit leakage of control. That's really the only way to do this kind of thing and avoid the runtime checks.

As I understand it the whole point is that write and write_n_close has diffrent types, and if you want to enforce static checks on them you generally can't permit diffrent types in diffrent branches of a conditional.

I didn't spend much time trying to make a robust example, so here's a much better attempt:

FILE file1 = OpenFile("foo.txt");
FILE file2 = file1;  // problem
CloseFile(file1);
ReadFile(file2, buffer);  // Boom!

In order to solve the aliasing problem, all you have to do is to process variables and not names. Names can be attached to variables during the analysis in order to find out about which variable we are interested in any given point.

To put it differently, variable identifiers are only meaningful as names. If a variable has more than one name, then it is clear that it is the variable that we should be interested in and not the names that are attached to it.

The example you posted can be re-written in the following way which clearly demonstrates the solution:

FILE file1 = OpenFile("foo.txt"); //var1[file1]:{Open}
FILE file2 = file1;               //var1[file1, file2]:{Open}
CloseFile(file1);                 //var1[file1, file2]:{Close}
ReadFile(file2, buffer);          //var1[file1, file2]:{Close}; error.

The above means that openFile creates 'var1', and within the square brackets we can find the possible names of 'var1'. You can see that the problem of aliasing goes away when we process the actual variables and not assume that one name == one variable.

More conventionally (at least around here), one would talk about variables being bound to references to mutable storage cells that contain values. Which means all variables are bound to immutable values.

Now, consider that you can't statically determine whether the second invocation of write_n_close() will fail or not. The conservative thing to do would be to forbid it, but that would also make most code unwritable.

Not really. The correct thing would be to forbid it, because a possible path might lead to closing a closed file.

Trying to find all possible paths through the code statically to make sure the invariants are preserved is going to be exponentially hard (or worse) in many cases.

Actually you do not have to check all the possible paths. You only have to check the edges of blocks using sets of values. For example:

void mighty_function_which_may_close_the_file(FILE f)
{
    ...8,000 lines of very complex code, which in some place
    CloseFile is invoked.
}

FILE file = OpenFile("foo.txt");
if (getchar() == 'x') write(file); else mighty_function_which_may_close_the_file(file);
CloseFile(file);

In the above example, we do not care about following all the paths in the function "mighty_function_which_may_close_the_file"...all we care about is that it is possible for the file to close. Once we compile this function, we keep the information that the passed file may be closed after the function returns.

To explain more rigorously:

the input set of the function 'mighty_function_which_may_close_the_file' is:

{Open}.

The output set is:

{Open, Close}.

The input set of the function 'closeFile' is:

{Open}.

The sequence

mighty_function_which_may_close_the_file(file) => closeFile(file)

creates the following set relationships (output of a subroutine becomes an input of another subroutine):

{Open} => {Open, Close} => {Open}

Since {Open, Close} is a superset of {Open}, we can safely declare an error: the input set of CloseFile(file) may be {Open, Close}, but only {Open} is allowed.

The set information can be kept along the function and checked where the function is used.

And what we actually get is a phantom type. Or perhaps not, because we probably want to be able to branch on the actual state if we don't know it statically (oh look, GADT!). The sets are perhaps best handled as (disjoint) unions with subtyping.

What do you mean when you write "FP makes aliasing a non-issue"? That the storage-management benefits are irrelevant?
I'm actually interested in linear types because of FP, since they seem to be the only efficient & truly-FP solution for things like aggregate update.

On another note, aren't "referential transparency" and "pure"-FP somewhat idealized, since function calls can easily change the layout of memory used by the app? That is, the return value may contain newly-allocated memory.. (and then there is the stack, the PC, &cetera). I'm sure someone has pointed this out; I just haven't seen it.

So in an unusual sense, the reuse of storage via linear types could actually make functions more pure, if said functions just transform memory (vs. alloc/free it).

On another note, aren't "referential transparency" and "pure"-FP somewhat idealized, since function calls can easily change the layout of memory used by the app? That is, the return value may contain newly-allocated memory.. (and then there is the stack, the PC, &cetera). I'm sure someone has pointed this out; I just haven't seen it.

They're not idealized because the elements you mention are not part of the abstract machine used to specify the semantics.

I believe this article (Broadway: A Compiler for Exploiting the Domain-Specific Semantics of Software Libraries) uses annotations for compiler optimization and this one (Error Checking with Client-Driven Pointer Analysis) uses it for pointer analysis. Both are generally within the domain of libraries in C.

Personally I do not see a problem with aliasing. Maybe I am too optimistic, but I think if a block of code is viewed as a black box with annotations on its input and output, then the problem of checking aliases becomes a problem of reviewing annotations at the start and end of block.

In a sense, linear types are annotations that tell the compiler "you can't alias this value". They just happen to have extensive research done about them.

... where a more general solution exists?

Why have regular expressions when a more general solution exists?

If you have mutable data, then that data forms a new channel of communication between different parts of the program. You can use this power for good, when you use aliasing to design algorithms that communicate through shared memory to save time and space, but more commonly it just leads to bugs.

The reason that the obvious kind of annotations don't work is because you need to specify no-aliasing conditions in your preconditions and postconditions. Suppose your function has six different variables all of type Foo (call them x,y,z,u,v,w). Now, if two of those variables point to the same Foo object, then an update on one must update the other one too. If they hold different Foo objects, then an update to one should not change the other one.

Why is this hard? If you've got distinct objects (and you usually do), then the number of no-aliasing clauses in your specification will rise quadratically with the number of variables in the routine. For example, to specify that the variables in the previous example don't alias, you'd need to write:

x != y & x != z & x != u & x != v & x != w &
y != z & y != u & y != v & y != w &
z != u & z != v & z != w &
u != v & u != w &
v != w

Things get even worse with arrays, because you have to give a no-aliasing condition for each element in an array. This is basically why Hoare logic never lived up to the high hopes people had for it back in the 70s; you couldn't scale it up to real programs because every spec had a ton of unenlightening no-aliasing conditions for ever ounce of real meaning.