Hacker News Reader

Comment by ezyang | Hacker News Reader

The thesis is about designing a type system that supports both type inference and subtyping. If you program Java but hate writing explicit type annotations all day, the thesis offers the tantalizing possibility of having a type system that supports all the subtyping you want, but at the same time has as convenient and predictable type inference as ML or Haskell. Conventional wisdom is that this is hard; in this respect, the thesis proves a very surprising result.

View on HN

That's not super interesting (to me personally, an acknowledged idiot) because working programmers are hardly ever confused about types. Intellij pretty much already does that thing.

I have this idea that this paper does something super interesting that I'm too stupid to understand.

Is there a correctness angle I'm totally missing where you can constrain subtypes and ... not sure?

EDIT: I watched a thing earlier today where people felt they could reasonably subtype zero away and therefore never think about NAN as in the range or domain of their mathematical functions.

I want to learn more. Probably my degree of ignorance is such that I'm unable to ask the right questions. Can you help? This is probably an unfortunately hilarious question.

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.

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.

It's a little difficult to explain why subtyping is so difficult. One answer is that Hindley-Milner inference is actually really simple; simple enough that I can ask my undergraduates to implement in a week long programming assignment. But how to add subtyping? Now there's a difficult question: one you could write papers about. Along the way, there are a number of desirable properties you want to achieve, like decidability, existence of principal types (for any expression you write, there is a "best" type you can give it), compactness of inferred types, support for records and functions... and it's been very difficult to get all of them. This thesis does it.

Assuming the thesis is "easily" implementable, will a from scratch ML need to be created, or can existing ML based languages all benefit? i.e. implement in the compiler, and voila, subtyping + inference for all MLers.

Unfortunately, it is never as easy as "just" putting in a new type system to a preexisting compiler. In the case of ML and Haskell in particular, we are kind of crazy about GADTs, and GADTs and subtyping are known to interact in complex ways. See for example http://gallium.inria.fr/~remy/gadts/Scherer-Remy:gadts-subty... (PDF)

That was my intuition.

The instant win scenario for ML based languages is quite appealing from this side of the fence (Scala) where it's not all roses wrt to type inference and subtyping.

Maybe even, gasp, SML can rise from the ashes and bring Rob Harper's dream to fruition (which seems to be that developers stop using Haskell); that or someone implements Rossberg's 1ML, or the theory backing this thesis.

All the MLs, including Haskell, have pretty significant tradeoffs, would be great if there was really 1 ML to rule them all.

Yeah 1ML is what really benefits from this: You really want subtyping for modules to handle library evolution, and 1ML means if you want it for modules ya better have it everywhere.

Yeah IIRC width subtyping for modules was the only thing they didn't have complete inference for if you didn't use large types, so this is a huge win. Though I'm nearing the end of the thesis and I'm afraid there may be some things about 1ML that don't jive with this (1ML elaborate to full Fω and gives you explicit access to existentials and higher kinds, which are possibly difficult to unify with the work here).

> That's not super interesting (to me personally, an acknowledged idiot) because working programmers are hardly ever confused about types. Intellij pretty much already does that thing.

One reason it's nice to have "toy models" and proofs is that we can gain confidence about how our "foundations" will/won't behave.

For example, Java's type system is well understood; it has some problems (e.g. https://dev.to/rosstate/java-is-unsound-the-industry-perspec... ), but we can think of them happening in 'contrived edge-cases', and we can make conservative claims about what is/isn't a 'contrived edge-case' (i.e. "that looks reasonable" vs "don't do that, even if it works").

Since we have a good understanding of Java's type system, we can do things like generating Java code automatically; this may be as simple as getters/setters in an IDE, or as complicated as a full API compatibility layer (e.g. swig, and many others). Automatically generated code can be very strange, but it's fine if we know that only "reasonable" code will be generated.

Let's compare this situation to IntelliJ's inference features. To make a more apples-to-apples comparison, let's turn IntelliJ's features into programming language features: we make a new language, which looks like Java but doesn't need as many type annotations. Our compiler takes the code it's given, fires up IntelliJ on a headless remote desktop, pastes in the code, clicks on some "infer types" button, copies out the result, kills the IntelliJ/desktop and feeds the generated code to javac.

The question is: what are the rules of our new language? Do we know what code looks "reasonable" and what looks like an "edge-case"? What properties can we be confident about? For example, can we make a claim like "return type annotations aren't required when calling a method"? How can we be sure? If our language does have such properties, do they work nicely together? For example, if we can do `a = b.c();` without annotating `a`, and we can do `a.b(c);` without annotating `c`, can we compose these together to do `a = b.c(d.e())` without annotating `a` `e`? Imagine how frustrating it would be if we couldn't be confident about what would/wouldn't work; all we could do is hit "compile" and cross our fingers, and if we did encounter a problem we wouldn't be sure about how to work around it. Third-party libraries which work perfectly well on their own might cause errors when used together; should we ask upstream to fix their (working) code? Should we abandon the libraries, or maintain in-house patches?

Now imagine that we're writing a code generator; e.g. a port of swig to our new language. What sort of code should we emit? How can we be sure that it'll work, regardless of whatever curveballs our users throw at us?

Even if we surmount all of these challenges, with a mountain of regression tests, what happens when IntelliJ push an update and a bunch of those tests break; do we start by rewriting our language's documentation?

This is why it's useful to have a small, self-contained system (like MLsub) which we can reason about semi-easily; which we can prove properties about. Even if we have to restrict things, like only proving something for a subset such that XYZ, at least we know what those limitations are.

Real systems can then be built on this foundation, with confidence about what can and can't be done.

>That's not super interesting (to me personally, an acknowledged idiot) because working programmers are hardly ever confused about types. Intellij pretty much already does that thing.

That's not true at all. For one, because programmers are not constrained to Java programmers. Try to infer the correct types in some C++ template code for example.

C++ templates are more a limited form of macros than generic types, though. Macros can make type inference more difficult because they usually don't provide any type bounds for the engine to work with and C++ templates can be especially complex.

This system doesn't seem to support type-based dispatch, so it's not directly suitable for Java.

That's not clear to me; unusual cases in Java are even used in some of their co/contravariance examples, and an example of how they can be encoded here are given (notably, without requiring existentials or bounded quantification). In particular, I'm not sure what about type-based dispatch in Java couldn't be replaced here by their "sum-of-products" notation (which allows you to directly reference fields if they are shared by every variant) combined with making { x : A } and { y : B } subtypes of { x : A | y : B }. I wouldn't be surprised if you can replicate a significant percentage of Java with nothing more than the machinery of this paper.

Reply on news.ycombinator.com