The value restriction in ML is so limited. If I have an auto-curried function

> fun foo (k : int -> 'a) (x : int) = ...;

it should be the case that partial application of foo is always non-expansive, right? It's really annoying that partial applications of auto-curried functions often can't be given general types.

> val raisek (x : int) = raise (Fail (Int.toString x));

> val fooRaise = foo raisek;

Warning: type vars not generalized because of value restriction...

I hate when the type system interferes with standard, semantics-preserving transformations.

## 1 comment:

A formalist would say that the expansive and non-expansive expressions are specified in the Definition of Standard ML (section 4.7) and, according to that definition, function applications are expansive (rather than non-expansive).

You might want to spend a moment to think about what it would take to make partial application of "auto-curried functions" non-expansive or, rather, generalizable.

What you need is to somehow change the type system. Concretely, an auto-curried function would get a different type from a non-auto curried function.

The earlier definition of SML had a notion of imperative type variables, which was one such type system. I have never programmed in an ML with imperative type variables, so I don't really know how well it worked in practice.

At any rate, while it is not too difficult to come up with such a type system, it is not necessarily all win. First of all there is the additional complexity that it brings. Programmers need to understand more complex types and the compiler writers need to implement a more complex type checking algorithm.

Another problem is that making such a distinction at the type level can interfere with modularity. Changing an implementation might change the type, which may be undesirable for many reasons. Or, if a signature specified a particular type, some implementations may become illegal.

MLton's wiki has a nice page on value restriction.

Post a Comment