4 ms·

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 w

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.

xyzzy123 10y ago
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.
- awestroke 10y ago
  Not the same thing at all
  - deleted 10y ago
    [deleted]
  - xyzzy123 10y ago
    Thanks, enlightening as always.
- taejo 10y ago
  > 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.
  - deleted 10y ago
    [deleted]
- chombier 10y ago
  From the Kotlin spec: http://jetbrains.github.io/kotlin-spec/#_type_inference 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.
  - xyzzy123 10y ago
    Excellent, so now this will help us write programs better. Thanks. I upvoted you. Looking forward to the blog post.

xyzzy123 10y ago

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.

awestroke 10y ago
Not the same thing at all
- deleted 10y ago
  [deleted]
- xyzzy123 10y ago
  Thanks, enlightening as always.
taejo 10y ago
> 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.
- deleted 10y ago
  [deleted]
chombier 10y ago
From the Kotlin spec: http://jetbrains.github.io/kotlin-spec/#_type_inference 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.
- xyzzy123 10y ago
  Excellent, so now this will help us write programs better. Thanks. I upvoted you. Looking forward to the blog post.