I haven't seen a notation that is easier to read than inference rules. Writing them as functional programs can be problematic, as the rules do not always fully specify an algorithm. One judgement may have different derivations. If one writes down algorithms, such as HM type inference, then one does in fact often use notation in the style of functional programming.
Incedentally, rather than abolishing the inference rule notation, there are actually tendencies to introduce them into programming: https://en.wikipedia.org/wiki/Epigram_%28programming_languag... (though it remains to be seen if this is a good idea)
In the current example, there is just no need to write Hindley-Milner in this notation. Using pattern matching and sets will do just fine.
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)
...
(although I did once threaten my co-workers that I would tell the theoretical mathematician on the team about Unicode identifiers in Java. He used to write LaTeX in the Javadoc comments [which Doxygen handles rather nicely])
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?
If you're using a tool which forces you to use a map to find glyphs, you're simply doing it wrong. Really, there is no excuse in this day and age not to support Unicode well!
I think this will be demise of Haskell by the way. As good as it is, the notation is still full of '||', '!!', '++', ':' ... So I think there would be another iteration in the functional world. Haskell will die, just like ML/Ocaml/etc had died, because Haskell with slightly better syntactic sugar had captured that segment of developers.
But these are not so much syntactic issues. It always seemed to me that people are actually drawn to Haskell's syntax.
Where you have a different + for doubles and ints...
It's probably difficult to strike the right balance between too little and too much overloading. Maybe OCaml does not allow enough overloading. For my taste typical Haskell code uses too much. But that's a matter of taste, I suppose.
How do type classes make that harder? You either need to understand what "foo" does, or you need to understand what "fooForThisType" does. What's hard about the former?
Are there alternative approaches I am not aware of? All I can see is encode the type in the name of the function (fmapList, fmapMaybe, fMapVector, etc), or forcing the functions to all be in separate namespaces and have to qualify them (List.fmap, Maybe.fmap, etc). Both seem much worse than typeclasses.
Totally anecdotal, but this is really not the case for me. I have only dabbled in Haskell, and never really used it for a project from end-to-end, but have used Standard ML quite a bit in the last few months to write a lexical analyzer generator [0] and just recently spent a weekend and a half using OCaml.
There are a number of Haskell features and general design that I think are better than the MLs. While modules and functors are quite cool, I think typeclasses end up being more practical. Standard ML gets a lot of little things right that I think OCaml gets flat out wrong (mutable strings, throwing exceptions instead of returning 'a option), but Haskell seems to take it further, with a standard library that I can only describe as very tasteful. This is just my impression after reading half of Real World Haskell and doing a lot of dabbling but not a lot of real work, so I'm sure it's incomplete.
Haskell's syntax IS nicer than Standard ML's and OCaml's, but that is the least important thing IMHO. If there were an ML (strict, impure) with typeclasses and with as taseful design as Haskell at the edges, I would probably use that over Haskell, even if the syntax was ugly(ier). As it stands, I'm inclined to eventually switch to using Haskell, and just figure out how to deal with the other bits of it (laziness, purity), just so I can use typeclasses and the well-designed bits.
[0] In case you doubt how much ML I've written, the repo is on GitHub
To be completely honest, I'm a little skeptical given that the first page in the "Mythryl for SML programmers" highlights adding special-cases to the front-end to support printf: http://www.mythryl.org/my-Mythryl_printf.html I don't really miss printf in SML, although if I wanted it I think I would rather reach for this kind of type hackery instead: http://mlton.org/Printf
You think haskell is going to die because it has operators? Seriously?
Admittedly, it's an ASCII bastardization of the notation, but it's the same idea.
A
B
----
C
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.