“What part of Milner-Hindley do you not understand?”

(Operationally speaking, the two forms (let and abs+app) are always equivalent, though).

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...).

Admittedly, it's an ASCII bastardization of the notation, but it's the same idea.

Although I am not working in that area any more, when I used interactive theorem provers the one I used mostly would present the proofs in Sequent calculus. It showcased a nice connection between the logical framework and a small step operational semantics reading of te formulas.

In my view, it is important to understand the reasons for different fields choices of notation; it typically reveals interesting things about the fields in question. When starting out learning a new field, it often seems strange and un-intuitive, but after a while one starts to recognize that there are many valid reasons for why a certain style of notation is used. Of course, sometimes it is just an accident of history, and bad choices stick around :)

I've hopped around quite a bit in my studies (semantics, formal methods, operations research, theoretical computer science, pure algebra, logic), and I always feel overwhelmed with new notations and concepts. Nowadays I tend to expect it when trying to learn something new.

Of course, all this is a matter of taste and for particular applications like HM it doesn't make any difference at all which notation to use. I don't want to defend the rule notation too much; it takes up a lot of space in papers and if you have something better then fine. But maybe that explains why people prefer this notation.

The horizontal bar notation is not ideal however. In my opinion Prolog notation is clearer, because it reads the right way around, and it makes it clear what relation we are defining. In Prolog notation you'd define a typeof(context, term, type) relation:

    typeof(C,var(X),T) |- X:T in C
    typeof(C,app(X,Y),B) |- typeof(C,X,A -> B), typeof(C,Y,A)
    ...

http://en.wikipedia.org/wiki/Fortress_(programming_language)

Or even mix-fix operators like Maude. Maude lets you define operators with variable arity and arbitrary stuff before, between and after, like

       let _ = _ in _ 
       _::_(_)
       _,_ |- _
       You _, but I _

...thus reducing his productivity to zero while he hunts through the Unicode maps to find the glyph he wants?

But these are not so much syntactic issues. It always seemed to me that people are actually drawn to Haskell's syntax.

You think haskell is going to die because it has operators? Seriously?