True, but it is also true that the best papers would be even better if they were written in less terse and cryptic style so that the same information could be obtained more easily.
I’m not sure about that. For example, the first time I read them, each of these statements in the declarative specification of Hindley–Milner type inference took me a long time to unpack.
x : σ ∈ Γ
--------- [Var]
Γ ⊢ x : σ
Γ ⊢ e₀ : τ → τ′ Γ ⊢ e₁ : τ
--------------------------- [App]
Γ ⊢ e₀ e₁ : τ′
Γ, x : τ ⊢ e : τ′
------------------ [Abs]
Γ ⊢ λx. e : τ → τ′
Γ ⊢ e₀ : σ Γ, x : σ ⊢ e₁ : τ
----------------------------- [Let]
Γ ⊢ let x = e₀ in e₁ : τ
Γ ⊢ e : σ′ σ′ ⊑ σ
------------------ [Inst]
Γ ⊢ e : σ
Γ ⊢ e : σ α ∉ free(Γ)
---------------------- [Gen]
Γ ⊢ e : ∀α. σ
Each one takes a sentence or two of relatively dense English text to explain:
[Var]: If the context indicates that it has a particular type, a variable is inferred to have that type.
[App]: If a function is inferred to have some type, and a value is inferred to have the same type as the parameter of that function, then the application of that function to that argument value is inferred to have the type of the result of the function.
[Abs]: If the body of a function is inferred to have some type, given an arbitrary type for its parameter, then the type of such a function is a function type from that parameter type to the type inferred for the body.
[Let]: If an expression is inferred to have some polymorphic type, and another expression would be inferred to have some monomorphic type given that a particular name were bound to that polymorphic type, then a let-expression binding that name to the former expression within the latter expression would have the same type as inferred for the latter.
[Inst]: If an expression has a polymorphic type, and that type is an instance of some more polymorphic type, then the expression can be said to have the more polymorphic type.
[Gen]: The type of an expression can be generalised over its free variables into a polymorphic type.
But having learned this notation, I can now read and write specifications of type systems with ease, and do so much more quickly and compactly than I could in a more approachable notation. To me, that’s a win.
Of course, I’m the sort of person who finds Java programs hard to read because they seem to take so long to say anything. So opinions are going to vary on this!
Ah, serendipity! As it happens I'm working on a variant of HM type inference right now, so my first step was to look up the explanation on Wikipedia and have my eyes glaze over. (As the saying goes, 'Which part of [above equations] do you not understand?' Answer: all of it! And it's not even the first time I've looked at it, though I don't remember anything much from the previous time.)
Yes, I find typical Java style too verbose for optimal readability; but I find typical Perl style too terse for optimal readability. The sweet spot is somewhere in the middle.
There is an editorial problem with that (which nowadays, with electronic publishing should not be an issue): space is (used to be) a scant resource. Hence density of content was more important than clarity of exposition.
Nowadays I guess everything boils down to a custom of which we (yes, I am part of the problem) have not been weaned. It looks more scientific to write things densely and more or less cryptically.
Also, we scientists are a bit afraid of publicly (I mean, to the general public) explaining our way of understanding things, because we know it is somewhat blurry, informal, possibly even comical to a lot of people. And we tend to be introverts.
I guess things like arxiv.org etc. are going to create a new way of explaining scientific discoveries much more interesting and enlightening.
