5 ms·

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

by ezyang 10y ago

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.

xyzzy123 10y ago
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.
- ocharles 10y ago
  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.
- ezyang 10y ago
  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.
  - deleted 10y ago
    [deleted]
  - deleted 10y ago
    [deleted]
  - virtualwhys 10y ago
    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.
    - ezyang 10y ago
      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-subtyping@inria2012.pdf http://gallium.inria.fr/~remy/gadts/Scherer-Remy:gadts-subty... (PDF)
      - virtualwhys 10y ago
        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.
- chriswarbo 10y ago
  > 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-perspective 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.
- coldtea 10y ago
  >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.
  - akiselev 10y ago
    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.
Veedrac 10y ago
This system doesn't seem to support type-based dispatch, so it's not directly suitable for Java.
- Jweb_Guru 10y ago
  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.

by ezyang 10y ago

xyzzy123 10y ago

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.

ocharles 10y ago
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.
ezyang 10y ago
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.
- deleted 10y ago
  [deleted]
- deleted 10y ago
  [deleted]
- virtualwhys 10y ago
  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.
  - ezyang 10y ago
    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-subtyping@inria2012.pdf http://gallium.inria.fr/~remy/gadts/Scherer-Remy:gadts-subty... (PDF)
    - virtualwhys 10y ago
      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.
chriswarbo 10y ago
> 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-perspective 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.
coldtea 10y ago
>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.
- akiselev 10y ago
  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.

Veedrac 10y ago

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

Jweb_Guru 10y ago
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.