Lambda the Ultimate

This is pretty obvious to anyone who has written code that may be accessed by multiple threads or code points unaware of each other.

This is hardly news :)

On the other hand, I'd like to note that it makes life easier quite often: for example the notorious singleton patter in essence is a shared global, but is often used to enable communication between various instances instead of passing references around.

Coming from his particular background, it's safe to assume Bracha means "static" in the Java sense: having a global lifetime. I agree it's an unfortunate choice of terminology, but it's been around at least since C (where at least it sort of made sense)...

You can still do things like Console.WriteLine(...) without statics. Using thread local storage and a stack for each "static" in each thread you can set up some part of the environment without having to pass it around in function calls. Cocoa's auto-release pools (which are chained) and graphics contexts (I'm not sure if they are chained) are examples.

Where's the difference to the current statics? In C# you can choose between per-app-domain statics and per-thread statics, which are stored in the TLS (there's a ThreadStaticAttribute).

None, except the initialization and release of the resource is explicit. There is also a defined way of temporarily overriding the environment. A silly example might be:

using (AutoDisposePool pool = new AutoDisposePool())
{
    AutoDisposePool.Add(new ImplementsDisposable());

    SomeFunctionThatUsesTheCurrentPool();
}

A very easy way to get access to your environment.

Unfortunately, it's also a very easy way for anyone else to get access to your environment. That means your code almost certainly won't play well with others, or even with multiple instantiations of itself. There are slightly more complicated ways of getting environmental access that have none of those problems, and are worth using in almost every circumstance.

Every time I've had to write code that interfaced with a hardware device, the first thing I wrote was a set of stubs emulating the device's interface, for testing purposes. That's exactly the sort of thing that statics make difficult to impossible.

Console.WriteLine is of course a static method rather than a static mutable variable, which is what Gilad is talking about. Still, even this looks somewhat unnecessary. It seems much neater, rather than having a static main method and a bunch of static objects, to instead have console applications implement a ConsoleApplication interface:

public interface ConsoleApplication {
    public void main(Console console, List<String> args);
}

The advantage of this is that as you application now doesn't rely on a particular static global Console object you could easily allow concurrent and distributed access to the application by simply creating several instances and then passing them Console objects wrapped around a network socket, essentially following the model of CGI but without much of the overhead. A similar approach could be taken for GUI applications, where each application is passed a Window object (which could in fact just be a sub-frame of some main application window). Likewise, a Runnable object could be passed a reference to the thread it is executing in rather than needing Thread.currentThread. Etc.

Actually I like this approach, but in my experience it tends to break down, because the hard part is not necessarily the mechanics of adding parameters to those things that used statics, it's deciding what is the _minimal_ interface of the new object that you are going to pass it.

There seems to be some tension here between the top-down and bottom-up styles of design. Designing the "mother-object" which is passed to an application that contains all the (previously static) functionality necessary (or contains references to other objects that have that functionality) is a top-down approach, while exposing static methods/fields one by one is a bottom-up approach.

The top down approach is better once a language and applications have evolved into something useful and the set of necessary functionality is well-covered, and the bottom-up approach is better when the language and its core libraries are evolving rapidly, since it results in fewer interface and application changes.

Unfortunately, refactoring these design points incrementally becomes impossible once a language is popular enough that there are a large number of programs that will break.

And this is how the pile o' steaming software known as Java became what it is. Yay.

There is another drawback to the static-free way of doing things, too. If objects are small and highly factored apart, then it can lead to many chained accessor calls like:

motherObject.getFatherObject().getFileSystem().newFile().exists()

etc.

When it gets to three or four levels of indirection, it becomes increasingly hard to remember exactly which object holds which functionality and how to get there in the minimum number of steps. That leads to a bunch of shortcuts like:

motherObject.newFile()

And soon all of the objects get feature envy and start implementing each other's functionality until it's all a nasty tangle:

motherObject.getFileSystem()

motherObject.getFatherObject().newFile()

and motherObject.getFatherObject().getMotherObject().existsFile()

Where every object loves and hates all the other objects! I've seen this happen over and over.

There are worse things than statics!

FileSystem fs = motherObject.getFatherObject().getFileSystem();
File f = fs.newFile();
if(f.exists()) ...;

When it gets to three or four levels of indirection, it becomes increasingly hard to remember exactly which object holds which functionality and how to get there in the minimum number of steps.

But it is of course trivial to remember that to read a line from the console you import java.io.BufferedReader or you import java.util.Scanner and of course a button is clearly javax.swing.Button (or is it... let me look it up... ah, JButton)

What is special about packages that makes the levels of indirection there easy to remember and somehow keeps us from making a bunch of shortcuts?

We remember simple classnames, and our IDEs manage the rest for us. If we don't remember the classnames, we try to remember some of us and then the IDE does a search. Occasionally, the IDE will ask us to disambiguate, if there is more than one class with a given name (java.util.List and java.awt.List), but that's pretty rare.

I've not typed an import in the last seven years coding Java, and rarely even see them.

You're right that IDEs do this exceedingly well these days. The other major difference is that (in the old days), one would just do an import package.* to get access to all the classes in an entire package with their short names added to the current file's scope. With import static, even static fields/methods can be referred to by their short name.

There isn't an equivalent shorthand for lots of chained method calls (certainly in Java--to the best of my knowledge in other languages).

Maybe being able to import chains of accessor method calls would reduce the problem?

And of course they can do the same thing for methods defined on objects. I agree that if we truly see a move away from static, languages ought to provide more flexible ways of working with such shortcuts (Scala's import from objects and Java's static method import are both examples of this, but neither is perfect). But surely IDEs could do for method names what they today do for imports. E.g., I could just type "getFatherObject" and the IDE could auto-complete the receiver of that method, requiring me to disambiguate when necessary. Whether this is practical or desirable is more a matter of style than of a technical difference between packages and classes.

There is state which only makes sense in a per-thread or per-process/per-app-domain or even per-machine manner

People are so used to solving this problem with the mechanism of statics that it is common to conflate the name for the solution and with that of the problem.

The problem is needing to share state among some family of local environments, but statics are not the only solution to this problem.

My preferred solution is to have that state passed in explicitly to those environments from some initializing environment. This makes it easier to trace data-flow, to substitute in variants for testing or changing requirements, etc.

Another is to have localized message passing between those local environments (and only those), which will be better for some variants of the problem.

Statics, in the sense that Gilad is using them, is really a term for solving the problem by enforcing, at a meta-level of the language, objects of long-lasting, global-access state.

As he states, this is a bad solution to this problem, however real and common the problem may be.

The comments following the article note that Scala's objects are somewhat like statics. It's true in the sense that they can be used in that manner.

Some of Scala's key innovations really revolve around clever uses of the type system to avoid needing statics at all; situations that would have traditionally required the use of static-like capabilities no longer do. Additional context and capabilities can be easily blended into components.

The scala compiler itself is a case in point. The early versions of the compiler made pretty extensive use of statics to model the symbol tables, name tables, and a variety of other tangly data structures with complex interdependencies. With the second version of the compiler (fully written in Scala) Martin used many of the "scalable component" features of the language to eliminate the need for statics.

nsc (new scala compiler) elegantly shows how to blend multiple component contexts together into a seamless whole application. Scala provides very detailed control over partial component abstraction, giving the coder the freedom, but also the necessary type discipline, to compose complexity in a scalable way.

The short version: Scala's need for statics is dramatically reduced by its type system.

I agree with you about Scala, but I also agree with Bracha that it doesn't go far enough, apparently out of compromise with Java, but also I think for other reasons.

But this also raises another question. Much of what Scala uses "statics" for is actually object construction patterns (case classes, factories, and so on). It seems to me, as well as to fans of dependency injection, that constructors are best regarded as a form of static access (or ambient authority, although DI people would not use that phrase), and should be eliminated from use where possible. It doesn't appear that Bracha wants to eliminate direct access to constructors, and I'm curious how he feels about it.

Finally, I also agree that this is best thought of in terms of context. In general, I'm very interested in the idea of context-sensitivity in programming, both in traditional ways (binding, scope) and less traditional (configuration files and so on). Of course, I'm not the only one...

Getting rid of static state is more likely related to understanding your design upfront rather than much to do with the type system! Taking NSC as an example, features that have been in there for a while do not depend on static state while new features (e.g., recent changes to case classes), for now, do depend on static state. Static state is extremely convenient for getting things implemented, but in the long term should be re-factored out.

The avoidance of static state in NSC is a perfect example of why static state is bad: without so much static state, I've been able to hack in an incremental presentation compiler that memoizes parse and type information. The most gruesome parts of the presentation compiler deal with what static state remains, which is thankfully minimal when compared to other compilers.

The general idea of being able to have a continuous range of language semantics, from dynamically to statically (with inference), from static state to no static state, etc., seems really attractive - and to have the tools to make it possibly to easily move around in that range. So you could start with a very quick & dirty thing and progressively refactor and refine towards something more, well, anal. Dyalizer seems cool, gradual typing seems cool.

(I guess one could vaguely get it by e.g. first writing in Bean Shell then later re-writing in Java or something, but obviously that requires entirely too much actual finger typing.)

If one is starting with something loosely typed, then a key tool in the bag would be auto test generation so you can refactor more safely and easily.

What would it be like if such a gestalt ide / tool-chain existed? Would it really be something new and useful?

My preferred solution is to have that state passed in explicitly to those environments from some initializing environment. This makes it easier to trace data-flow, to substitute in variants for testing or changing requirements, etc.

Let's also be clear that this is the basic idea of dependency injection frameworks. To all the "but we need statics" people, perhaps what you really need is Spring...

This is also a place where dynamically scoped variables might be useful. We all know that dynamically scoped variables are bad when used for normal function argument binding, but when passing around shared state like this, which is inherited from the caller, it can be very useful. Dynamic scoping here has the same advantages as you listed for explicitly passing values around, but without the cost of changing the signature of several functions after they are written, if more information from the caller is later determined to be needed.

What about unrestricted imports? Without imports we would be forced to have (SML like) functors for modules with external dependencies, which would make statics just another parameter. Calling Console.WriteLine() is only a static method because Console is a global shared class, not a instance explicitly given to a module.

Strike the root: ban global namespaces and unrestricted imports! Only authority through explicit introduction! (in a revolutionary tone ;)

Imagine you're debugging "the old way", i.e. have console-output nearly everywhere in your code. Isn't it cumbersome to pass an instance of Console to every method/instance you need access to it. To speek more generally, isn't it cumbersome to have such a fine-grained environment which is passed around all the time?

That depends completely on what mechanism is available for "passing" such an environment... If it's too cumbersome, we need new mechanisms for managing context. We shouldn't just punt and make it global.

Exactly. I've run into several situations in the past where (a) global data is used to avoid passing context information as semi-automatic extra parameters to function calls, and (b) this comes back to haunt the developers some time later when concurrency becomes an issue.

There are at least two distinct concerns here: expressive power and run-time performance. In the former case, where the design of the program logically calls for some context information to be available, it seems to me that this could be achieved using some sort of dynamic scoping, so that necessary context is passed implicitly in all functions calls. It is only because most mainstream programming languages don't support any kind of dynamic scoping that we have traditionally resorted to global data as the alternative.

Actually, if we only want simple context information, I don't see why this couldn't be done statically but implicitly given sufficiently clever semantics. It's not much different from implicitly passing the object reference on a method call in many OO languages: as long as the type system recognises that functions requiring implicit context can only be called from elsewhere in the same context, it's all the same idea.

For bonus points, I'd like to see a robust framework that goes beyond simple dynamic scoping to share context information across a specific group of threads, since this is sometimes a fair reflection of the model being implemented. This would allow us, for example, to generalise the practically useful concept of thread-local storage to support shared state or common resources in a thread pool without resorting to fully static data and the global namespace. Combined with higher-level thread synchronisation to access the common data safely, perhaps some sort of transaction system, this would allow potentially parallelisable algorithms to be implemented using multi-threaded techniques with each group of threads operating in the same context, but with no inadvertent name clashes should the same algorithms be called simultaneously from multiple other threads, and of course with no need for global anything.

The performance implications if such an approach were implemented naively are probably quite unpleasant, but of course history is full of times when naysayers criticised a useful idea for performance failings that disappeared as implementations got smarter.

Scala example?

This is what "Inversion of Control" and "Dependency Injection" is all about.

As I said in my post we need to give parameters to modules/packages, so we have more lexical scoping. In pseudo-java:

package foo(java.io io, System s) {
   class Foo {
      public void bar(int x, int y) {
         s.out.println(x + "," + y);
         //do stuff
      }
   }
}

So everything inside the package has access to the package parameters. The parameters can be other packages or even objects. This could replace configuration files (your package can receive a configuration parameter and then your caller builds the object with the necessary information), makes easier to adapt classes when used inside certain packages (e.g. in package a we give them an instrumented version of package java.net). Even dependency injection frameworks would become obsolete, we can easily expose the dependency to the DataSource as a package parameter, so each layer is in a different package and the main package that drives the application initialize the layer packages with the necessary dependencies (so we can say new db.Foo() and the db package was initialized with the layer dependencies).

The theory behind this is really solid (it's almost a clone of SML's module system) and is much safer (there's no ambient authority). It also paves way to solve some issues that are impossible today (e.g. factories are necessary because classes are accessed by global name instead of being passed by reference, if they were parameters I could easily give a package a different implementation of a class and they could write new Foo() and get a SubFoo instance).

This is basically what's known as the "Cake" pattern in Scala, also known under the general rubric of "Scalable Components" or "Objects as Modules". There are obvious relations to dependency injection frameworks, although the pattern is both more powerful than them (allowing for simply gorgeous aggregation of component assemblies into components), and less powerful (no easy way to add support for component lifecycle, session-scoping, auto-wiring, AOP).

Ada packages can have parameters (resulting in what is called "generic packages" in Ada-speak). They can indeed be used for dependency-inversion as well as a host of other things...

Does this approach really solve the problem? Now everything in the package foo has access to io and s. You'd need very fine-grained packages to control the scopes. Of course, there are a lot of advantages regarding IoC but I think we need something else.

Again, it's a different programming style. Today in mainstream languages every class in every package has access to every other package and every static thing (modulo public/private issues), so this scheme is no worse than current practice. Actually it's better, because it makes you declare your dependencies (benefit #1), exposes those dependencies as parameters (so you can adapt and modify them if needed, benefit #2), don't require globals (benefit #3), enforce package initialization order (benefit #4) and let you instantiate packages with different parameters (benefit #5).

Not having higher-order modules (or even first order ones) becomes a problem when we need to have a component model (that's why there's so many different container solutions out there), want to reuse code but adapting it first (many problems solved by AOP are just adapting all the classes in a package to do something more, which can be done with a higher-order module), initialization order needs to be enforced (today things are quite messy and we never know if the initialization order of our packages is thread-safe. This happens in Haskell too, lookup for top-level IORef issues).

As a side note I think that we lost so much time because mainstream OOP languages choose to make classes solve everything, from code reuse to type hierarchies to access control of methods. Most problems solved by DI, factories, frameworks, etc., are simply issues of classes and not essential problems of computing. I've been studying PLT for seven years now and the only sure thing I got from it is that every non-first class thing in a language is going to cause problems sooner or later.

every non-first class thing in a language is going to cause problems sooner or later

I know next to nothing about PLT but that pragmatically rings true, to my ears. Presumably it is hard to make all things first class and still have a solid theory behind it, if you want things to be clean and well-fitting?

The best way to not have second class things is to have fewer different parts. Solid theory breaks apart if we add things that aren't well understood (e.g. mixing arbitrary effects and type systems). In languages like Forth or Self (i.e. the core of those) almost everything is first class. OTOH in languages with static type systems there's a tendency of making the phase distinction bigger than it need to be, so there's separate languages to describe types and values, functions and modules, usually with types and modules (which fall on the compile-time side) being less expressive than the values and functions world (which fall on the runtime side). It's still an active research topic to make these things work together, there are many good ideas floating around but no obvious solutions yet.

Actually I would say that it's easier to have a solid theory when everything is first class than otherwise. If every language element composes with every other the resulting algebra is more uniform and has fewer exceptions.

Actually I would say that it's easier to have a solid theory when everything is first class than otherwise. If every language element composes with every other the resulting algebra is more uniform and has fewer exceptions.

I would tend to agree. I don't think the problem with these systems is complexity of theory, but rather intractability of general analysis. Some of the most expressive, most consistent calculi have some of the simplest theoretical descriptions.

What languages 'equate' with such calculi? What problems are there with those languages that we aren't all just using those and nothing else? Are they statically typed, do they have debuggers, are they amenable to macros, etc? Seems interesting to me if there were a clean yet really usable language.

What are the sorts of limits we see in languages due to the 'intractability of general analysis'?

Daniel's post below covers the bases pretty thoroughly. As far as I know, languages based most closely on the most expressive calculi are mostly in the realm of theorem provers (that's a lot of "mosts"). The calculi I have in mind are things like Martin-Löf Type Theory, Logical Frameworks, the Calculus of Constructions, etc.

I would say there is not yet a "clean yet really usable" language. This is still an active area of research. As for the limits we see in such languages, it may still be too early to say, in some sense. But the limits we might worry about, at least, are things like undecidable compilation or the complete loss of the phase distinction.

(I wonder where Paul Snively is? This thread seems to have moved in his direction, too...)

I agree, but these theories are really simple (in breadth) and PLs tend to incorporate much mure stuff that don't compose well. There's a bit of distance between lambda calculus and Haskell (with GHC extensions).

I'm interpreting that to mean statically typed languages are limited in what they can successfully let be first class, whereas more loosely or dynamically typed languages aren't so much?

It's not really a issue of static vs. dynamic type systems, but a kind of uniformness of features. The problem of static typing is that it introduces too much in the name of phase distinction, but Epigram, Agda and Coq (to name a few) do wonders with them. Higher-order modules are missing in most languages and the only ones with it are statically typed ones (AFAIK). IME it's more due to lack of theory (sometimes it didn't even exist then), a desire to make the language "more expressive" and keep up with the joneses (i.e. mainstream languages), so people end up adding things to a language without seeing how it mixes with the current theory. Good examples of this are Perl 6, Java's generics and closures, pretty much everything in Haskell after the standard, C++, R6RS, Erlang records, to name a few.

The primary reason (ignoring optimization) that one would prefer static to dynamic typing, is that it lets us establish invariants about a program which hold for all running instances of that program. As the number of possible running instances of any nontrivial program is infinite, it therefore holds that the static typing guarantees are established before some instance of the program is run.

"Before execution" and "during execution" are two phases with differing semantics. So it seems to me, that static typing does imply a phase distinction of some sort.

Naturally, with more modern runtime environments, it's certainly possible to defer some forms of typechecking until runtime. If you have a language with dependent types (depending on terms computed at runtime), some typechecking might not be able to occur until a term with a given dependent type is instantiated. OTOH, that doesn't necessarily require fully-deferred ("dynamic") typechecking.

Here's an interesting thought:

Static-typing and dynamic-typing are fundamentally the same thing; with static typing encompassing eager evaluation of the typechecker (all terms are checked greedily, before the program runs) and dynamic checking is the case of running a typechecker in a lazy fashion (laziness here being so pervasive that type judgments per say aren't done--just queries as to specific attributes of terms. In other words, the question "is this a duck" isn't asked; just "can this quack?").

With that in mind, one can note the following:

* For some programs, eager evaluation of typechecking will diverge, but lazy evaluation will terminate. In other words, some sufficiently-complex types are essentially co-data. The flip side of that coin is of course that failure is detected sooner.

* As dynmamic typing is lazy typechecking--use of memoization might help. OTOH, certain memoization schemes which have been tried in practice, such as polymorphic inline caches, haven't had the desired impact on performance. (As an added note, many dynamically-typed languages, other than things like Oz and Erlang, promiscuously encourage side effects, complicating any memoization scheme. Some, like CL and Smalltalk, make things even tougher by permitting type migration). As a result, most dynamically-typed languages don't memoize the results of type inquiries.

Enough rambling for now...

that eager vs. lazy perspective helps me more easily understand that dynamically typed things could succeed in some case where a statically typed one wouldn't.

type judgments per say aren't done--just queries as to specific attributes of terms

And that would be the reason why static typing and dynamic typing aren't "the same thing", but just under eager and lazy evaluation, respectively. As you say, they don't compute the same result. If they were the same, but would only differ in the reduction strategy, then, according to the Church-Rosser theorem, they would still compute the same result.

First of all, I should preface this by noting that my earlier post was not intended as a rigorous claim, but as a thought exercise. So I apologize if I'm being sloppy--I surely am. :)

That said, there are many cases where the following holds:

* Some result f(x) is desired.
* Some code to compute f(x) is "buried" in a computation to a larger function, G(x); computation of which is expensive.
* Given the result of G(x), the result of f(x) can be trivially discovered by applying some other function (such as a projection) to the result of G(X).

In many cases of this, lazy evaluation can buy you a lot, if all you really want to know is f(x), and G(x) is only computed as a byproduct. A pervasively lazy solution can "drill down" to get f(x) without computing lots of other stuff, while a pervasively (or naively) eager solution will compute all of G(x), then apply the projection function to extract the desired subset of the result.

A canonical example occurs in matrix math. Assume A and B are matrices of appropriate size (so their product is defined), and assume that you want the third row and forth column of said product, and type:

(A * B)[3,4]

in your pseudocode of choice. The dumb, eager solution will compute the product of the matrix--an expensive operation--and then apply the projection function to get the desired cell. The pervasively lazy solution will attempt to retrieve the desired cell of the not-yet-computed result, and then perform just that subset needed to get the element in question.

The C++ library Blitz++ does this sort of cleverness (at compile-time, using template hackery) to achieve a blinding-fast matrix library--one that has a simple and consistent API, but doesn't do dumb things like multiply two matrices just so you can look at one element.

Of course--what, if rather than desiring only a given element of the matrix, you want to compute the whole product (so you can print it out)? The eager solution will be faster, as no thunking goes on. At which point, looking up a particular element is trivial.

It's kinda like that with the "is it a duck" vs "does it quack" question. If you know that it's a duck, then you know it quacks, but figuring out that a term is a duck may be undecideable in a sufficiently powerful type system; determining if something can quack, however, is frequently easy.

Often times, with static typechecking--what you (or your compiler) really wants to know is not whether some X is a duck. It wants to know the conjunction of "can X fly?", "can X swim?", "does X have feathers?", "does X taste good when roasted in hoison sauce"?, and numerous other predicates on X which are all easily inferred by the collective judgement "is X a duck?" If you want to know all of this about a term X all at once, the "high-level" type judgement is the easiest way to go.

Of course, with purely structural typing/subtyping (think C++ templates, at least until the C++ standard gets revised when nominative features get added), you still are doing a whole lot of proving of individual attributes of a term, rather than proving that a given term is of a given elaborated type.

Again, I apologize if I'm engaging in gratiuituous hand-waving here...but I'm certain there's a point buried in the above somewhere. :)

The dumb, eager solution will compute the product of the matrix--an expensive operation--and then apply the projection function to get the desired cell. The pervasively lazy solution will attempt to retrieve the desired cell of the not-yet-computed result, and then perform just that subset needed to get the element in question.

Note that call-by-need is not intelligent either. By itself it does not guarantee that a minimal amount of work is done to compute a particular result. To take advantage of laziness, you still have to design the algorithm carefully.

A typical example used to pitch the beauty and elegance of lazy evaluation is the Sieve of Eratosthenes. Of course, the fact is that the example, as usually presented, does not implement The Genuine Sieve of Eratosthenes, and is significantly slower than the real thing.

Another typical example used for the same purposes is the quicksort algorithm on lists, see here, which also "gives an efficient algorithm for finding the k smallest elements out of n". The reason why this happens is that the quicksort algorithm has a particular divide-and-conquer pattern for performing the sort. A mergesort on lists, for example, does not have the same property. Of course, for finding the smallest k elements out of n, the quickselect algorithm is even faster, because it does not bother to sort the elements, like a naive lazy quicksort does. Yet, it seems to be often implied that the lazy version of quicksort specializes to quickselect, which is not true.

First of all, I should preface this by noting that my earlier post was not intended as a rigorous claim, but as a thought exercise.

That much was obvious, but the analogy still does not work. The type system of a typical modern "statically" typed language and the dynamic checking of a typical "dynamically typed" language simply do not compute the same result. A typical type system attempts to assign types to expressions. No such thing is done by dynamic checking. No matter how many times you run a program with dynamic checking, you don't get out an assignment of types to expressions.

Dynamic checking typically assigns types to values instead of expressions or terms. Given a combination of a lambda calculus and an evaluation strategy, values are generally a specific subset of terms. So this isn't quite as broken as you're suggesting.

Dynamic checking typically assigns types to values instead of expressions or terms. Given a combination of a lambda calculus and an evaluation strategy, values are generally a specific subset of terms.

That is not necessarily true. Values, or semantic objects, are not necessarily a subset of terms or expressions. In the Definition of Standard ML, for example, semantic objects (values) are specified separately from terms and the two are disjoint (AFAICT). Values aren't necessarily a subset of terms even when they are expressed using a similar grammar. Some semantic styles (e.g. denotational semantics) make the distinction clearer than others (e.g. operational semantics). The distinction becomes clearer in a language that has semantic objects with identity, such as mutable references. In Types and Programming Languages, for example, which uses operational semantics, chapter 13, References, says:

Since all values are also terms, this means that the set of terms should include locations. [...] Of course, making this extension to the syntax of terms does not mean that we intend programmers to write terms involving explicit, concrete locations: such terms will arise only as intermediate results of evaluation. In effect, the term language in this chapter should be thought of as formalizing an intermediate language, some of whose features are not made available to the programmer directly.

IOW, the terms of the (object) language are first translated to the terms of an intermediate language. Values, then, are a subset of the terms of the intermediate language --- not of the (object) language.

In comment-40305, Scott Johnson wrote:

... there are many cases where the following holds:

• Some result f(x) is desired.
• Some code to compute f(x) is "buried" in a computation to a larger function, G(x); computation of which is expensive.
• Given the result of G(x), the result of f(x) can be trivially discovered by applying some other function (such as a projection) to the result of G(X).

In many cases of this, lazy evaluation can buy you a lot, if all you really want to know is f(x), and G(x) is only computed as a byproduct. A pervasively lazy solution can "drill down" to get f(x) without computing lots of other stuff, while a pervasively (or naively) eager solution will compute all of G(x), then apply the projection function to extract the desired subset of the result.

In other cases, lazy evaluation creates a lot more work than an eager solution would. Consider the following program in an eager language.

(define (foldl op init lst)
  (if (null? lst)
      init
      (foldl op (op (car lst) init) (cdr lst))))

(define (generate acc seed next done?)
  (if (done? seed)
      acc
      (generate (cons seed acc) (next seed) next done?)))

(define (from-to lo hi)
  (generate '()
            hi
            (lambda (x) (- x 1))
            (lambda (x) (< x lo))))

Here's what we get in Guile 1.8:

$ guile
guile> (load "foldl.scm")
guile> (foldl + 0 (from-to 1 10000))
50005000
guile> (foldl + 0 (from-to 1 100000))
5000050000
guile> (foldl + 0 (from-to 1 1000000))
500000500000

The last expression takes a few seconds to compute on my ancient hardware, but it does return a result. Compare this to Hugs:

$ hugs
__   __ __  __  ____   ___      _________________________________________
||   || ||  || ||  || ||__      Hugs 98: Based on the Haskell 98 standard
||___|| ||__|| ||__||  __||     Copyright (c) 1994-2005
||---||         ___||           World Wide Web: http://haskell.org/hugs
||   ||                         Bugs: http://hackage.haskell.org/trac/hugs
||   || Version: September 2006 _________________________________________

Haskell 98 mode: Restart with command line option -98 to enable extensions

Type :? for help
Hugs> foldl (+) 0 [1..10000]
50005000
Hugs> foldl (+) 0 [1..100000]

ERROR - Control stack overflow

Let's try GHC:

$ cat foldl.hs
module Main where
main = putStrLn (show (foldl (+) 0 [1..1000000]))
$ ghc -o foldl foldl.hs
$ ./foldl
Stack space overflow: current size 8388608 bytes.
Use `+RTS -Ksize' to increase it.

This is indeed the case, but it surprises me. Where is the stack consumption coming from? I would have expected it for foldr, but foldl only needs to consume a single list cell at a time from the lazy stream of integers it's given. It seems to me that should be possible to do, lazily, in constant space.

Stack overflow

In comment-41071, mental wrote:

This is indeed the case, but it surprises me.

It surprised me too. But then I recognized it for what it was -- a leaky abstraction. That's just the way things work. Abstractions always leak. Annoyingly so.

Haskell has seq, Prolog has cut — there is always a fly in the ointment.

Anyhow... In addition to the page Derek mentioned, see also this and this.

I'm not so sure it creates *a lot* more work. I'm not even convinced it creates more work at all:


GHCi, version 6.8.2: http://www.haskell.org/ghc/ :? for help
Loading package base ... linking ... done.
Prelude> :m Data.List
Prelude Data.List> foldl' (+) 0 [1..100000000]
5000000050000000


Sure it'd be more difficult to identify in a less contrived example, but I guess I'd have to evaluate the difference in effort between spotting the stack overflow and adding the apostrophe (or strictness annotation), or coding a lazy solution to the 'projection' situation mentioned above.

I've also found that the relational approach pops up more often than I anticipated. It's nice to write IO code that 'runs' across the whole filesystem, then filter it to only operate on interesting files/directories higher up in the call stack. I think it's easier for me to build straightforward, composable and reusable code this way.

Church-Rosser only says that reductions don't alter a term's normal form. This isn't much help if your reduction strategy isn't normalising on the term in question, because you'd have to change strategy to find the normal form if one existed.

While they don't compute the same result type as-is, it's possible to envisage a result which static typing computes completely and dynamic typing computes just enough of - one of the first results you get from this is that given a dynamic language whose notion of types looks like that of the simply-typed lambda calculus, the static type system required to encompass all that's actually happening is rather more complex and powerful (and very probably has typechecking that's no more decidable than the dynamic language's evaluation!).

If a static variable is accessed without any sort of interface, then it is indeed bad for security. But the real problem here is not that the variable is static, it is that there is no security mechanism around it.

I think what Gilad means is that the global accessibility of the state and methods in question makes them accessible by default as opposed to requiring the API designer to create mechanisms by which they can be accessed, and thereby be forced to think about access control. In fact, it's worse, because it is extremely hard to retrofit an API with a security mechanism that existed without one when there is a lot of static state. I am not a security expert, but I can tell you that access by default is one of the worst possible ideas from a security standpoint.

Static variables are bad for distribution. Static state needs to either be replicated and sync’ed across all nodes of a distributed system, or kept on a central node accessible by all others, or some compromise between the former and the latter. This is all difficult/expensive/unreliable.

I don't buy it. Non-static variables needs to be replicated and sync'ed as well.

Yes, but when they are objects, more instances of those objects are easily created, whereas you cannot easily replicate the static state of classes in (e.g.) Java.

Static variables are bad for re-entrancy. Code that accesses such state is not re-entrant. It is all too easy to produce such code. Case in point: javac.

The problem is not static variables, but the design of the software around static state. Javac had much static state where it could have been done without it.

Well obviously the design of software around static state hinges on the fact that static state exists. So by definition, if it did not exist, you could not design software around it.

Static variables are bad for memory management. This state has to be handed specially by implementations, complicating garbage collection. The woeful tale of class unloading in Java revolves around this problem.

What does memory management have to do with class unloading? nothing. A static class' data memory segment is nothing more than another root area added or removed from a collector, dynamically. It's trivial! I really don't see it as a problem.

I would caution you against making such categorical statements. The issues surrounding class unloading in Java are anything BUT trivial.

Static variables are bad for for startup time. They encourage excess initialization up front.

What does initialization have to do with static variables? static pointers to singleton objects, for example, are null, and the objects are created at first chance. It's lazy initialization.

Lazy initialization is actually a coping strategy for the problem, not a solution to the problem; a clear admission that startup time CAN be a problem.

Furthermore, In this day and age, it's not really expensive to have a few 100s of objects initialize themselves at program startup. Even in such an extreme case, startup time would be below half a second.

Bogus argument. Half a second is an eon to someone who wants to run many JVMs, use the JVM as a scripting platform, automate processes that are each standalone Java programs, etc.

Not to mention the complexities that static initialization engenders: it can deadlock

Deadlocking has nothing to do with static variables. Anything can deadlock.

I assume he meant that there can be cycles in initialization which need to be broken somehow. It leads to some nasty problems.

applications can see uninitialized state

Not if the compiler ensures the initialization order.

You aren't familiar with Java's class loading semantics. The initialization order is *not* determined by the compiler. In fact, the specification of the initialization order (and its implementation in any JVM) is a complexity nightmare.

and unless you have a really smart runtime, you find it hard to compile efficiently (because you need to test if things are initialized on every use)

You don't have to do that. You first do the static initializations, then the dynamic initializations, then you run any code.

Not when you have dynamically loaded code, e.g. in Java and pretty much any other language runtime system nowadays.

Static variables are bad for for concurrency. Of course, any shared state is bad for concurrency, but static state is one more subtle time bomb that can catch you by surprise.

The fact that a memory location is labelled with 'static', to show that only one instance of the variable will exist in memory has nothing to do with concurrency. Any memory location accessed by more then one threads is bound to have concurrency problems.

You miss the point. You cannot easily replicate this shared location in memory by creating a new instance of its class. It's global and always will be. Making it non-shared, replicated, or synchronized all require significant rearchitecting of the system after the fact, whereas instance fields of classes can more easily replicated.

As a conclusion, this is another case of blaming the tool for not using it correctly. Just like 'destructive update' is blamed for all of the world's problems by functional purity advocates, here we have another case of 'I can't deal with X, it's X's fault'...

This argument is completely bogus, since it could be used to dismiss *any* criticism of *any* tool. And then what point would there be developing any new tool or refining old ones? You do a disservice to yourself when you fail to recognize that your choice of tools has a profound effect on the quality, understandibility, flexibility, and ultimate robustness of your solution. Your tools can't rescue you, but they sure can make life hell.

And Gilad's arguments just point out vast and wide the pit is that so many fall into, and suggests that perhaps we should do something about these gaping holes in the ground that tend to lure programmers with their seductiveness and then send them to the pits of unmaintable hell, described in lively color in his post.

I think what Gilad means is that the global accessibility of the state and methods in question makes them accessible by default as opposed to requiring the API designer to create mechanisms by which they can be accessed, and thereby be forced to think about access control. In fact, it's worse, because it is extremely hard to retrofit an API with a security mechanism that existed without one when there is a lot of static state. I am not a security expert, but I can tell you that access by default is one of the worst possible ideas from a security standpoint.

Access by default has nothing to do with static. I can make a C++/Java program without any static variables with all the fields of all classes public. So please let's not confuse the issues.

Yes, but when they are objects, more instances of those objects are easily created, whereas you cannot easily replicate the static state of classes in (e.g.) Java.

That has nothing to do with static, as well. What do you mean you can not easily replicate the static state of classes in Java? if classes were regular objects, they could be easily replicated. That Java chose to make classes special objects and hence make replication difficult is Java's fault, something that other languages (e.g. Smalltalk) don't have. So, again, static is blamed wrongly here.

Well obviously the design of software around static state hinges on the fact that static state exists. So by definition, if it did not exist, you could not design software around it.

If static state did not exist, many things would be much harder to do. There is a reason that static state exists. If people abuse it, it's not the fault of static state, just like anything else that can be abused: for example, APIs that are over-engineered and therefore difficult to use are due to their developers' wrong approach to problem solving rather than object-oriented programming itself.

I would caution you against making such categorical statements. The issues surrounding class unloading in Java are anything BUT trivial.

It's Java's fault, not static state's fault.

Lazy initialization is actually a coping strategy for the problem, not a solution to the problem; a clear admission that startup time CAN be a problem.

Well, if, for example, you try to calculate PI's millionth digit before starting the actual program, then it is definitely a problem. But then it's not a problem of static state: the same calculations could be done locally using stack variables...the program would delay the same amount of time as in using static variables. Again, not a problem of static state.

Bogus argument. Half a second is an eon to someone who wants to run many JVMs, use the JVM as a scripting platform, automate processes that are each standalone Java programs, etc.

If you want a program inside the JVM to start instantaneously, then why did you put all these computations before starting the program? actually the problem is design, not static state.

I assume he meant that there can be cycles in initialization which need to be broken somehow. It leads to some nasty problems.

So can calling the same function over and over, i.e. infinite recursion. Again, a design issue, nothing to do with static state.

You aren't familiar with Java's class loading semantics. The initialization order is *not* determined by the compiler. In fact, the specification of the initialization order (and its implementation in any JVM) is a complexity nightmare.

So why is static state blamed? blame Java's designers, not static state.

Not when you have dynamically loaded code, e.g. in Java and pretty much any other language runtime system nowadays.

I don't see any issue with dynamically loaded code. Fundamentally, it's no different than loading a C DLL at run-time, which is, in turn, no different than actually creating a new process in an operating system. So if the new module contains static context, initialize it, then run any code that depends on it. It's simple, and O/Ses are doing it for many years now.

You miss the point. You cannot easily replicate this shared location in memory by creating a new instance of its class. It's global and always will be. Making it non-shared, replicated, or synchronized all require significant rearchitecting of the system after the fact, whereas instance fields of classes can more easily replicated.

I disagree. Why you can not easily replicate this shared location in memory? obviously, the replicated instance will belong in another process, running possibly in other machine. I see no problem in duplicating it.

I don't see why instance fields can be replicated more easily. If there is a bunch of data in memory, there is no difference if these data are the result of declaring them with 'static' or allocating them dynamically with 'new'. Once an object exists in memory, its replication has the same issues independent of where the object is.

This argument is completely bogus, since it could be used to dismiss *any* criticism of *any* tool. And then what point would there be developing any new tool or refining old ones? You do a disservice to yourself when you fail to recognize that your choice of tools has a profound effect on the quality, understandibility, flexibility, and ultimate robustness of your solution. Your tools can't rescue you, but they sure can make life hell.

The only bogus thing in this case is the programmers who don't think before choosing their tools.

A tool can make life hell only if it gets in the way. Static state does not get in the way at all, it's optional. Don't use it, if it does not suit your needs. Just like you don't use C when you don't need its capabilities.

And Gilad's arguments just point out vast and wide the pit is that so many fall into, and suggests that perhaps we should do something about these gaping holes in the ground that tend to lure programmers with their seductiveness and then send them to the pits of unmaintable hell, described in lively color in his post.

The only thing Bracha's argument say is that software is not like selling shoes, and only trained people should do it. Just like in other engineering disciplines, software must be created by people who are trained professionals, i.e. they have been trained to know when to use static state or not static state, they have been trained to use pattern X or pattern Y according to needs. Putting an untrained person in front of an IDE does not create a software product.

I actually agree with some of your points, and think some of what's been blamed on static state here is really just static state as implemented in Java. Other places I disagree (Access by default is about having references to state, not public/private. Static doesn't play well with replication because it breaks the model of there being a single global state. etc.)

In my view, static is a bad idea simply because it solves too specialized of a problem. The general problem is context management, and a single global context per process only covers a few of the usage patterns you might want. Furthermore, as requirements change you'll often find yourself needing to switch from one usage pattern to another.

For example, you may expose a file system as a singleton object and then realize later you need to sometimes use two of them. If you've just used 'static' for the file system, then you're going to have to go change all of the code that now can possibly use two file-systems and modify it to take a parameter instead, and then change all uses of the file system to make use of those parameters, and then add code to hook up all the parameters everywhere. This is a major change in code for a minor change in requirements, which is bad.

If you took Java and just deleted the idea of statics, then you'd force people to write code in such a way that all access was passed explicitly. This would improve robustness of code to changes like this, but would also make Java even more verbose (which the masochistic Java guys may see as win-win). The key is, IMO, to not just eliminate static, but to replace it with a more general solution to context management. Scala may have a good solution here - I haven't looked at it closely enough yet (I'm one of the diluded who thinks pure functional is a good idea).

i'll ask this hoping somebody can make it less nebulous and more grounded e.g. by pointing to work Bray Meyers does or something like that (maybe not "Kurzweil says we'll have AIs next year so don't worry").

if software is so complex, and a lot of programmers aren't so hot, and we need more of the, how can we either ameliorate the difficulty, or do some stunning end-run around it all?

maybe you could have a company where you use the layered approach of CTM where most people only get to use declarative code, and then authorized people get to use state? :-}

Without static (or global) variables you would have to change your program so this list is available at every call of integer_factorization(i, v)

No, you simply wrap the object performing these computations in a generic memoizer exposing the same operations. Your application is properly factored into modular components right? ;-)

As this example demonstrates, there is still no proper use for mutable static state.

I think there is a tradeoff and it should be addressed more explicitly. Especially it is easy to modify existing programs using static variables.

But this is Lambda the Ultimate, after all! If this is true in today's languages, we should ask: can it be made easier in tomorrow's languages? In fact, a huge part of the history of programming can be construed as answering this question in the affirmative.

Anyway, the point here is not to quit using static state in existing languages (although some would make that argument); the point is designing a new language where one is not so tempted.

I think Gilad Bracha is right with his statement for many existing more or less "modern" languages and probably even more for tomorrow's languages.

Incroducing a "clean" memoizer in C would mean to add a module, i.e. a new source and header file. IMHO static variables make sense here from a pragmatic point of view, if only for testing purposes. If a language has closures or classes, I think static variables are indeed useless.

Note that the issues with ambient naming also apply to free functions as well as variables. (Also note that many things can safely be ambiently-exposed).

Yes, security is primarily concerned with controlling effects, so if those functions don't themselves have access to mutable static state or other ambient authority, they can't have side-effects. Global functions aren't ambient authorities, mutable static state is.

Really, capability security and referential transparency are closely linked, and I'm tempted to say that the latter subsumes the former. The one thing I haven't seen addressed in referentially transparent languages are ambient authorities. Haskell exposes an openFile function for instance; this violates capability security, but doesn't seem to violate referential transparency, even though I sort of suspect that it should in some way (it accesses and updates hidden state -- the file system).

Longevity issues. Here, the argument concerns a global lifetime

True, static state is just bad for long-running applications that must undergo live upgrade for instance.

...and openFile and its siblings provide unfettered access (modulo the OS) to it, so your suspicions are more than warranted.

OTOH, your beef is probably not with Haskell, but with the OS. One issue with all modern OS's is that entities in the filesystem must be named--an unnamed file is considered semantic garbage by the filesystem and is gleefully stomped on by fsck or similar utilities. And such names are generally discoverable.

Unix permits hidden directories, which cannot be searched by a user without given permission (this differs from directories with no read access). A more general facility that might be useful are files which are only accessible with an unforgeable name--and that files are created this way by default. (Named files, in such a scheme, could simply be files for whom the reference has been stored in a table which provides a searcheable key). I'm certain this musing is unoriginal.

OTOH, your beef is probably not with Haskell, but with the OS.

Yes, but languages are far more flexible than OSes, and I would expect that a language will thus allow me far greater control over my subsystems written in the language. For a file system API, I would expect that I could chroot a module in my program, for instance. The way to do this is simple in any language: don't allow traversing upwards in a directory, ie. no GetParent() method/function on the current directory. All I/O effects are thus necessarily isolated to the provided directory, or any other directories to which the module may have a handle.

[Edit: I should note that omitting GetParent() is only the easiest way to get a chroot, and I'm not sure I would actually go that way as my other post suggests.]

GHC at least offers you that flexibility - rewrite the libs and get on with it!

I plan to, just not with Haskell. ;-)

Your beef might only be with unsafePerformIO...

In Haskell without unsafePerformIO, IO actions like openFile can only be meaningful when composed into a distinguished IO action "main". The definition of main can delegate authority to other functions in a couple of ways:

• a function may be allowed to create an IO action, by having a type like a -> IO b (perhaps for some very specific b)
• a function may be allowed to transform or depend on IO actions, by having a type like C (IO a) -> IO b (again, perhaps for very specific C, a and b)

One might object that too much authority is bundled into the single type constructor IO, but this is a matter of design, not of insufficient mechanism.

This perhaps points to another approach to capability security, but I'm not very familiar with the literature, so I have no idea how this approach relates to existing work. A quick search returns this blog post, which I have not read. And of course there is Kiselyov and Shan's Lightweight Static Capabilities, which I have shamefully also not read (but I believe you have). I don't know how or whether those ideas are related.

In Haskell without unsafePerformIO, IO actions like openFile can only be meaningful when composed into a distinguished IO action "main". The definition of main can delegate authority to other functions in a couple of ways

You do raise a good point, and I sometimes forget that monadic actions are so carefully controlled, but the coarseness of the primitives (like IO) is still a gaping hole from a security standpoint. Further, even if IO was refined into more specific actions (DelDir, FileRead, etc.), openFile still exposes an underlying global namespace, which is undesirable. For instance, isolating a subsystem to work within a specific directory (a chroot) would still be impossible, and I don't think you could refine monadic actions sufficiently to enforce that in the type system. At best, you can enforce that the subsystem could not traverse a directory upwards (action: DirParent), but even that is unnecessarily restrictive I think. Any other thoughts?

Thanks for the pointer to the blog post. Looks interesting. This discussion is definitely focusing my understanding of the connections between referential transparency, monads, and capability security.

For instance, isolating a subsystem to work within a specific directory (a chroot) would still be impossible, and I don't think you could refine monadic actions sufficiently to enforce that in the type system. At best, you can enforce that the subsystem could not traverse a directory upwards (action: DirParent), but even that is unnecessarily restrictive I think. Any other thoughts?

If each file is associated with a phantom type with capability-like properties then you can have a File c type, where c is the type of capabilities you have. So you can have operations read :: File Read -> IO String and parent :: File (Parent (File a))-> IO (File a) that only work with the file with given capabilities. Actually you need some encoding to express multiple capabilities, probably writing such library is in the order of 50 milliolegs.

That's a nice example. Certainly if one adopted capability security as a design goal, one could do much better than the existing Haskell library. I think it would be an interesting direction for research, because it's not totally obvious to me whether existing mechanisms would be enough. We might run into in-principle difficulties, or we might find that the resulting library is just too cumbersome. Either way we may discover some new language mechanisms in the process.

But as I said above, I don't know much about this area in general, so I'm not sure how interesting or novel this would be.

I've given this some thought, and the biggest stumbling block to my mind is that the phantom types can't be composed at sufficiently fine grains. For instance, Read, Write, Execute are individual operations on a File type, but how do you express the composition of File (Read & Write & Execute), File (Read & Write), File (Read & Execute), File (Write), File (Execute), File (Write), and File (Read). I think one would need some form intersection types to express the above compositions, and we'd need subtyping to be able to use the wider types whenever a narrower one will do. Given current type systems, I think one would have to write each composition manually.

I think this gets a little unwieldy though, and my gut instinct is to avoid type proxies to convey information that is probably more clearly conveyed by an algebraic type (psuedo-Haskell/ML):

type FileOp = Readable of Handle | Writable of Handle | Executable
type FileSystem = File of String * FileOp list | Directory Dir of String * File list

openReader: File -> Maybe IO Handle
openWriter: File -> Maybe IO Handle
execute: File -> Maybe Bool
...

I don't really like that structure either, but it's very clear and obvious how to implement it. I'd like to see if you can come up with a way to statically verify all the various combinations.

Reflecting the capability to getParent() as a type proxy raises interesting possibilities though. I'll have to think on that some more.

After reading the Arrows blog post linked to above, it occurred to me that r/w/x can be individual labels, and so File could be encoded with a phantom type for each one:

type R = Read | None
type W = Write | None
type X = Execute | None

type File r w x = string * ...

openReader: File Read W X -> IO Handle
openWriter: File R Write X -> IO Handle
...

I believe File would have to be defined as GADT in order to type these functions, and I'm not clear how that File declaration would fit in the declaration of FileSystem, but I now think some of these properties are expressible.

type R = Read | None

Instead of an algebraic datatype, to use phantom types, you should define a (distinct) type for each variant:

type readable
type nonreadable

However, as shown in my earlier post, if you have structural record types (like in Standard ML), you can get readable types just by having two general purpose phantom types yes and no. You could even put them into a library.

I believe File would have to be defined as GADT in order to type these functions

Doesn't seem like that to me. There are lots of things people throw GADTs at that can be reasonably implemented without them. For example, I recently implemented a small combinator library for expressing higher-order contracts in SML. All I used was functions having types of the form 'a -> 'a. After implementing my version, I noticed that those crazy Haskell academics (-; had used GADTs to implement a similar combinator library. I'm sure there are some places where GADTs offer value, but quite a few examples using GADTs can be easily encoded using simpler mechanisms.

For instance, Read, Write, Execute are individual operations on a File type, but how do you express the composition of File (Read & Write & Execute), File (Read & Write), File (Read & Execute), File (Write), File (Execute), File (Write), and File (Read).

Unless I misunderstand you, then it is easy to achieve. Just use a phantom record of phantom booleans. In SML syntax, you'd have types like:

{read : yes, write : yes, exec : yes} File
{read : yes, write : yes, exec :  no} File
{read : yes, write :  no, exec : yes} File
{read :  no, write : yes, exec :  no} File
(* ... *)

And you'd use type variables when you don't care, e.g.

{read : 'read, write : yes, exec : 'exec} File

Using a structural record type over pseudo "bool kind" is dual to using a structural variant type. For example, with OCaml's polymorphic variants you could use the following types:

openReader : string -> [`R] file
openWriter : string -> [`W] file
openReaderWriter : string -> [`R | `W] file
...
read : [> `R] file -> string
write : [> `W] file -> string -> unit

The nice thing here is that (a) the types are very concise, (b) you don't need any auxiliary type declarations, and (c) thanks to row polymorphism, types of individual operations are independent of unrelated capabilities, making them robust to extension.

(Edit: added ReaderWriter.)

With the record of booleans, one can require absence of capability (no rather than 'dontCare):

{read: no, write: yes, exec: 'dontCare} File

AFAICT, the structural variant type scheme (at least in the form presented) cannot express the above constraint (whether or not it is useful).

Edit: Oops, you actually can. You can say something like [> `R of no | `W] file.

Also, as you probably know, one can encode the structural variant type scheme with a type level list (or set). Without type level computations one would have to manually pick capabilities using combinators, but the burden could be a reasonable trade-off for safety under some circumstances. Basically, you'd have something like this:

type nil and ('h, 't) cons

val openR : string -> ({r:yes}, nil) cons file
val openW : string -> ({w:yes}, nil) cons file
val openRW : string -> ({r:yes}, ({w:yes}, nil) cons) cons file

val read : ({r:yes}, 't) cons file -> string
val write : ({w:yes}, 't) cons file -> string -> unit

I leave it as an interesting exercise to the reader to develop a scheme and a set of combinators to make it possible (and preferably reasonably convenient) to call write with a file opened using openRW (I do have a solution in mind).

Edit: Added missing arguments to open functions.

Edit: Edited the types in the encoding sketch to suggest that it could also be used to encode the absence of capabilities (but then you would need carefully defined conversion combinators).

With the record of booleans, one can require absence of capability (no rather than 'dontCare):

{read: no, write: yes, exec: 'dontCare} File

AFAICT, the structural variant type scheme (at least in the form presented) cannot express the above constraint (whether or not it is useful).

Actually, you can. That would correspond to the polymorphic type

[< `W | `X > `W ] file

I'm not sure you can achieve it without enumerating all allowed capabilities in this case, though. But that's no worse than with a record. (It's just a restriction of OCaml's surface syntax anyway, AFAIK the underlying type system is able to express absence of individual fields directly.)

I'm not sure you can achieve it without enumerating all allowed capabilities in this case, though.

It seems that you can (by using an incompatible tag with the same name). See the type in my previous post (I edited it at the same time you posted).

One lingering issue is what to do of an object that embeds a capability, that may change the semantics of the program if safe code receives the object and uses that capability.

I don't see a problem with this. A program has a statically known semantics, and a dynamically known semantics. Sometimes the stream embedded in the object will be the console, but sometimes I may want to provide a file stream instead. Or perhaps I wish to output to a socket. As Daniel Yokomizo said, you want to be able to specify the types of effects your program depends on, and the effects your program is parametric on. The dependencies should be known statically, and the parametricity is resolved dynamically during program execution.

My problem is that the compiler may not be aware that the object is holding a capability, since polymorphism can hide that fact to the receiver. One option would be to make the new type incompatible (in regards to polymorphism) but that reduces expressiveness.

To illustrate the issue, let us say that function f takes a Price defined as:

class Price:
   float value
   link Currency currency
.

Now for debugging purposes I decore Price with a qualifier that sends its value over the network each time it is accessed:

qualify Price is SendingMeInfo(writeSocketToMyServer)

If my program uses f 1,000 times with a decorated Price, the result is likely to be different than the undecorated version (execution time, dependence on network, resource usage...)

But as you said, the calculation result may remain unchanged. It does not have to. Instead of writing to a socket I could read dynamically the price from it...

My problem is that the compiler may not be aware that the object is holding a capability, since polymorphism can hide that fact to the receiver

I don't see why this is a problem. Encapsulation is a good thing. It enables local reasoning of information/security flow.