[benbataille]

No, this nonequivalence applies directly to the typing of the lambda-calculus which was the topic of the original papers by Hindley and proven by Damas.

On the contrary, the value restriction is a part of the extended rules used for the typing of ML. It was introduced because ML isn't pure, it supports references. The value restriction is there to prevent them having polymorphic type. The rule is simple : syntactic values are the only things receiving a polymorphic type. What is a syntactic value ? To quote Geoffrey Smith notes on SML97 "Basically, a syntactic value is an expression that can be evaluated without doing any computation".

All this iss done in order to ensure type safety. Actually, if references could have a polymorphic type, the type system would accept incorrect programs such as :

let r : 'a list ref = ref [] let r1 : int list ref = r let r2 : string list ref = r r2 := "a" let v : int = 1 + !r1

Which does not work because r, r1 and r2 are references to the same value.

Value restriction is a bit overkill. It rejects program which could be safely typed. Other solution to this problem exists. Actually, Standard ML used a different solution at the beginning (carrying information about the typed hold in a cell along) but it has other drawbacks. MLTon has a really good page about all that : http://mlton.org/ValueRestriction

Some research was done about relaxing value restriction. OCaml type system, for example, has less constraints than SML and MLTon (you can see this paper about that http://caml.inria.fr/pub/papers/garrigue-value_restriction-f...).

[Darmani]

You may be interested to know that the value restriction is not there to protect against unsafe programs. Rather, it is because polymorphic values get elaborated to functions after type inference, which produces some exceptionally unintuitive (but safe) behavior.

This is Karl Crary's explanation; here's the only online recording I've found: http://cstheory.stackexchange.com/questions/8892/type-infere...

[rntz]

You could elaborate polymorphic values to type functions; and if you were compiling ML to System F or System F-omega, that is certainly what you would do. But in practice this might produce performance problems (I shouldn't have to call a function every time I use the empty list just because it has polymorphic type!). I must admit I'm not sure what SML and Haskell compilers actually do.

So in some sense the value restriction is there to prevent us from having to make the ugly choice between unsafety on the one hand, and inefficiency and unintuitive behavior on the other.

[emillon]

In the presence of polymorphism and mutable cells, value restriction (or a restriction thereof) is necessary to establish type soundness (ie that typed programs are safe), so I'd argue that it achieves this goal.

As for this explanation, I'm not entirely convinced. In the first example, seeing x as two different cells depending on the type is interesting, but I have trouble seeing how it is possible to express its semantics without keeping runtime type information. Is System F compatible with type erasure?

[groovy2shoes]

I'm getting a few detailed responses :) Unfortunately, I'm getting conflicting answers. I'm having trouble wrapping my head around why App+Abs couldn't be equivalent to Let in the absence of the value restriction.

[benbataille]

It's because of the way the premises are written in regard to the type environment in the rules and how things are unified. It's directly linked to free and bound type variables and yes, it's complicated to understand.

If you look at the [Abs] rule, you will see in the premise "x : tau". Here, by definition, tau is non qualified. It represents a unique type. It's necessary monomorphic. Concretely, it means x will be bound to a type variable in the type environment and this type variable will uniquely be unified.

On the other hand, the premise for [Let] is e0 : sigma, x : sigma. Contrary to tau, sigma is qualified (polymorphic). So, it can be unified to a different type variable in different expressions.

I completely understand why it fails you. The way qualifier affects the unification process is quite complicated. I finally understood it only after having to write my own rules when I was implementing a type checker for my master thesis.

If you don't mind the formalism, read carefully the Wikipedia article paying particular attention to how tau and sigma are defined and to the paragraph about free and bound type variables. If you want something more practical, look at the Peyton Jones book I gave a link to in this thread. Part 9.5 is the important part but it's difficult to get without having read the whole chapter (eventually chapter 8 too). It 's still complex but far less abrupt than the Wikipedia article.

[groovy2shoes]

I understand the notation, but I don't understand the reasoning behind the Abs+App restriction (why does it have to be that way). I've been working on my own language and haven't gotten to the type inference yet, so maybe I'll finally understand once I go through it.

If the SPJ book is the one about implementing functional languages, then I've got a copy on my laptop I can peruse when I get home from work.

[gsg]

The difference between abstraction bindings and let bindings is that let variables are only ever bound to the value of a single expression, whereas the argument of a function may be bound to the value of any number of expressions.

This causes difficulties because the set of free type variables needs to be calculated in order for generalisation to produce safe type schemes, and that is tough to do for an unknown set of expressions.

[emillon]

I was not totally right in the my "uncle" comment. It has to do with the value restriction in the sense that it is where the distinction occurs (lambdas are never genezalized ; let-bindings are generalized for values), but the original HM system (without refs) indeed made this distinction.

I believe that if you don't do it and generalize everywhere, unification of types is harder or even impossible because everything has a type scheme.

This would look a lot like System F, for which type inference is undecidable, for example.