Hacker News new | past | comments | ask | show | jobs | submit login

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

So I rummaged around a bit more and found http://akgupta.ca/blog/2013/05/14/so-you-still-dont-understa... which explains the notation in much more readable English text. It's a pure win.

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.




Registration is open for Startup School 2019. Classes start July 22nd.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: