Hacker News Reader

Comment by ocharles | Hacker News Reader

The point is that you don't need to write the types down anymore. The program is still typed, but the compiler can figure out what the type of variables (in a well typed program) needs to be. As said, this has previously been a hard problem. If you're familiar with the `auto` keyword, think of that - but everywhere.

View on HN

That's nice but basically kotlin already implemented that thing before an academic paper showed us it was possible.

We all knew that and no one cared.

My thinking was that we now need very high resolution thinking about what types mean, for example, "do they come from functions which have these constraints as output", but that's just as ... well, it's unrealistic. How do you annotate the world?

If your output range was obvious to the compiler, that was never a problem to anyone.

Not the same thing at all

Thanks, enlightening as always.

> That's nice but basically kotlin already implemented that thing before an academic paper showed us it was possible.

According to Wikipedia, Kotlin first appeared in 2011. Algorithm W for inferring types in the Hindley-Milner type system was published in 1982.

From the Kotlin spec: http://jetbrains.github.io/kotlin-spec/#_type_inference

"Type inference is conservative — it may fail to find suitable assignment of type-arguments to the type-parameters despite that one exist, and the function invocation could be successfully typechecked if the programmer explicitly provided suitable type-arguments."

My guess is that what the thesis presents is complete type inference in presence of subtyping that is decidable, efficient, and that yields types with all the nice properties one could hope for (principality, compactness, ...).

Which is hard.

Excellent, so now this will help us write programs better. Thanks. I upvoted you. Looking forward to the blog post.

Reply on news.ycombinator.com