12 ms·

Type inference

146 points by luord 8y ago

muglug 8y ago
This is awesome. Type inference is an endlessly fascinating road to venture down, and each programming language presents its own set of challenges. I've built a type inference system[0] for PHP and it's incredibly satisfying when it does what you expect. [0] https://getpsalm.org https://getpsalm.org
skybrian 8y ago
That's how it works, but I'll point out that just because you can leave out type declarations in a Hindley-Milner language doesn't mean you should. Compilers are good at deducing types from a function's implementation, but humans will find them easier to understand if they know what the function's inputs and outputs are supposed to be before attempting to figure out how the implementation does it. Error messages will be better, too.
- simcop2387 8y ago
  Along with that, the compiler is going to do less work too. That means faster compilation and better programmer experience with the language.
  - rileymat2 8y ago
    How is it less work for the compiler? It still needs to figure out the return type to make sure it matches.
    - lifthrasiir 8y ago
      Type inference algorithms generally have two operations, verification and inference. Verification is faster and more complete (i.e. never misses an existing suitable type) than inference because it works from the biggest assumption that is a (hopefully) suitable type for given expression. Hindley-Milner combined with Algorithm W is really brilliant because it makes inference as performant as verification as the constraint solver is integrated in the inference process, but it does not work for all type systems; inference continues to be inferior when H-M is not applicable as is.
- jfoutz 8y ago
  There is an experimental phase where you really don’t know. Hygiene indicates you should codify the types after you’ve sorted out the real constraints.
  - Waterluvian 8y ago
    Got me thinking. Are there tools out there that solidify "auto"s into their types? Type inference is fast but what if I want to eventually lock it down and prevent accidental changes in type by adding a decimal or whatnot.
    - skybrian 8y ago
      An IDE could do it, but the risk for local variables seems smaller compared to the confusion when someone accidentally changes the input or output of a function.
    - SatvikBeri 8y ago
      The Jetbrains IDEs let you do this pretty easily, at least for Python and Scala (and presumably for Java & Typescript.)
  - Smaug123 8y ago
    In my mind, this is a bit of an "experimentation smell". It means you're experimenting backwards because you are uncertain of the domain in which you are operating. It's something I've learned to notice as a symptom that I'm flailing around in confusion, and that I need to step back and understand the problem better. Clarify the domain so that you know the types of everything up front, and your work is more than halved.
    - adrianN 8y ago
      I find that writing some code is often the best way to clarify the domain and figure out the types.
    - gameswithgo 8y ago
      >Clarify the domain Could typing out code be a good way to clarify the domain for some people, and/or some of the time?
- lou1306 8y ago
  On the other hand, from my limited experience in F# (but I guess OCaml would be similar) I found that, when you let the type inference algorithm do its thing, it can help you realize that your function is more general than you thought. For instance, you write a function for lists of strings and in the end it can actually work on any list. Maybe it's trivial, but I found it helped me thinking about refactoring/reusing my code in contexts I didn't expect.
  - weberc2 8y ago
    You can still annotate the expression with the general type once you know what that type is. :)
  - hinkley 8y ago
    Is it that hard to figure out that your method is generic? And what is this “end” you speak of? You don’t know what next year’s requirements are. Don’t confuse the implementation with the contract. That’s a variant of duck typing. If you need to do stringy things to the data later don’t advertise genericity. People will start using your function and then you’ll have to make a new method because they own the contract now.
    - lou1306 8y ago
      > If you need to do stringy things to the data later don’t advertise genericity. [...] People will start using your function and then you’ll have to make a new method because they own the contract now. I agree that my point doesn't really apply to functions that are part of some kind of API. Still, type inference is not duck typing: the former happens at compile time, unlike the latter. > Is it that hard to figure out that your method is generic? Well, it is not if you decide it to be generic from the start. What I was saying is that sometimes you start with "concrete" implementation, but the type inference helps you thinking about refactoring it to maximize reuse. Something like "hmmm, right now this method has signature 'a -> int -> 'b... I wonder if I can turn it into 'a -> ('b -> 'c) -> 'c and remove this other method that looks pretty similar..."
- Drup 8y ago
  My experience is that people who think that never worked with a language where inference is principal and complete (aka, "good") and/or have poor editor support. In languages that are still reasonably close to HM and that have decent editor tooling, like OCaml, leaving the type out in the implementation is the common practice. You only write them down in the external API (along with the documentation).
- gameswithgo 8y ago
  An interesting middle ground here is when the editor can annotate the function signature's types for you, with code lens type features. Of course this only works for people who happen to be in such an editor. Another issue I ran into recently was you can add a new type to your program, and break existing code. Where the type inference was able to deduce the type, and your new type appears to also be compatible, and now things don't compile and it is very mysterious why not! There can be some interesting big wins by leaving types off when possible though, like super easy refactoring. Just start passing ints to a big chain of functions and you are done. No need to change the signature of a big chain of functions.
- CuriousSkeptic 8y ago
  Or put another way: Compilers are good att figuring out what a function _can_ do. But humans need to specify what it _should_ do. Types aren’t always the right tool for that though. It would be interesting to see what could be done by integrating testing and typing, letting one inform the other.
- SOLAR_FIELDS 8y ago
  I definitely agree with this. Too often while learning Scala I’ve found myself scratching my head at some piece of code and wondering how to modify it because the typing system is inferring something I don’t expect it to.
georgewfraser 8y ago
For anyone interested in this subject, there's a great minimalistic implementation in OCaml here: http://okmij.org/ftp/ML/generalization.html http://okmij.org/ftp/ML/generalization.html The author starts with a naive implementation similar to the one linked here, then implements a series of optimizations that make it more efficient.
legulere 8y ago
The problem with advanced type inference is that the exact algorithm needs to be part of the standard for compability reasons (not just between compilers but also between compiler versions). So for me it makes more sense to have everything that’s beyond basic in something like a lsp-language server/ide.
- gergoerdi 8y ago
  > The problem with advanced type inference is that the exact algorithm needs to be part of the standard for compability reasons I don't think that's true -- if you have principal types, you can just say in your language spec that the principal type is inferred.
  - lifthrasiir 8y ago
    It can be really tedious to list the cases where principal types do not exist. Haskell has a separate section for ambiguous overloading [1] for that reason, and more ad-hoc or advanced type systems will be harder to describe. [1] https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-790004.3.4 https://www.haskell.org/onlinereport/haskell2010/haskellch4....
renox 8y ago
I don't know much about this topic but I've heard that Hindley-Milner's type inference has also drawbacks as it doesn't work well with partial compilation and subtyping. So does the benefits outweight the drawbacks?
- Drup 8y ago
  HM type inference works perfectly fine with separate compilation and/or partial files (whichever you mean). See the OCaml tooling for a concrete demosntration. Subtyping is a fairly large domain, and it really depends what you mean. There are cases where it works fine (again, see OCaml) and other where it's more problematic (see Scala). In any case it's not really HM anymore, it needs to be more.
- chombier 8y ago
  As far as I know, subtyping with polymorphism looks much better since Stephen Dolan's thesis on Algebraic Subtyping http://lambda-the-ultimate.org/node/5393 http://lambda-the-ultimate.org/node/5393
teajunky 8y ago
Every article on Eli Bendersky's website is just great. If he ever writes a book I would immediately buy one.
always_good 8y ago
The upside of type inference is that making small changes to types upstream doesn't necessary incur changes to code downstream. But the downside of type inference is that it makes reading code harder and you may depend on an IDE to know what your intermediate types are. Especially wrt generics and higher-order types where intermediate function calls don't have a concrete type in their signature. Nothing demonstrates this better than any time you've written code yourself only to immediately invoke the IDE tooling to inspect what the type is. If you didn't know, good luck to the person reading it in git diffs. I've had to git clone someone's Rust project recently just to follow the type transformation across a bunch of future/stream chains. This isn't an argument against static typing but rather an argument against inference excess. There's a nice middle ground where asserting the concrete type in critical places makes the code more readable but also checks your own assumptions. Like any time you received Maybe<Maybe<Int>> where you wanted Maybe<Int>.
- dllthomas 8y ago
  > This isn't an argument against static typing but rather an argument against excess. And also an argument for exposing better tooling when reading git diffs :D
- Klathmon 8y ago
  A general rule of thumb I follow is to explicitly type your interfaces, and infer private internals. (I mean "interfaces" not referring to any specific language feature, but to the concept in general).
  - steveklabnik 8y ago
    This is sorta where we landed with Rust; you have to type out type signatures of function signatures, but not inside function bodies. It's not based on public/private lines, but it's a similar idea.
    - deleted 8y ago
      [deleted]
    - 8y ago
abeppu 8y ago
I think he's using the term "bi-directional" in a potentially confusing and nonstandard way. As I understand it, in this area, that term typically describes a style of type checking and inference which arose later, and which involves both checking rules and synthesizing rules (the two directions), and which can be made to support some quite expressive type systems, but generally requires programs to have a sprinkling of explicit annotations. On that topic, I found these notes to be very helpful: https://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/15-bidirectional.pdf https://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/15-bid... But as I understand it, the concept started here: http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf
- vilhelm_s 8y ago
  Also, I think one should not call it Hindley-Milner. A key clever part of the HM algorithm is how it infers types for polymorphic functions, which this code doesn't do. For just the idea in this post, I suggest calling it something like "unification-based type inference", or "type inference using equational constraints".
piinbinary 8y ago
In case anyone finds it useful, I wrote an explanation of how type inference with let-polymorphism works: http://jeremymikkola.com/posts/2018_03_25_understanding_algorithm_w.html http://jeremymikkola.com/posts/2018_03_25_understanding_algo...

146 points by luord 8y ago

This is awesome. Type inference is an endlessly fascinating road to venture down, and each programming language presents its own set of challenges. I've built a type inference system[0] for PHP and it's incredibly satisfying when it does what you expect. [0] https://getpsalm.org https://getpsalm.org

skybrian 8y ago

That's how it works, but I'll point out that just because you can leave out type declarations in a Hindley-Milner language doesn't mean you should. Compilers are good at deducing types from a function's implementation, but humans will find them easier to understand if they know what the function's inputs and outputs are supposed to be before attempting to figure out how the implementation does it. Error messages will be better, too.

simcop2387 8y ago
Along with that, the compiler is going to do less work too. That means faster compilation and better programmer experience with the language.
- rileymat2 8y ago
  How is it less work for the compiler? It still needs to figure out the return type to make sure it matches.
  - lifthrasiir 8y ago
    Type inference algorithms generally have two operations, verification and inference. Verification is faster and more complete (i.e. never misses an existing suitable type) than inference because it works from the biggest assumption that is a (hopefully) suitable type for given expression. Hindley-Milner combined with Algorithm W is really brilliant because it makes inference as performant as verification as the constraint solver is integrated in the inference process, but it does not work for all type systems; inference continues to be inferior when H-M is not applicable as is.
jfoutz 8y ago
There is an experimental phase where you really don’t know. Hygiene indicates you should codify the types after you’ve sorted out the real constraints.
- Waterluvian 8y ago
  Got me thinking. Are there tools out there that solidify "auto"s into their types? Type inference is fast but what if I want to eventually lock it down and prevent accidental changes in type by adding a decimal or whatnot.
  - skybrian 8y ago
    An IDE could do it, but the risk for local variables seems smaller compared to the confusion when someone accidentally changes the input or output of a function.
  - SatvikBeri 8y ago
    The Jetbrains IDEs let you do this pretty easily, at least for Python and Scala (and presumably for Java & Typescript.)
- Smaug123 8y ago
  In my mind, this is a bit of an "experimentation smell". It means you're experimenting backwards because you are uncertain of the domain in which you are operating. It's something I've learned to notice as a symptom that I'm flailing around in confusion, and that I need to step back and understand the problem better. Clarify the domain so that you know the types of everything up front, and your work is more than halved.
  - adrianN 8y ago
    I find that writing some code is often the best way to clarify the domain and figure out the types.
  - gameswithgo 8y ago
    >Clarify the domain Could typing out code be a good way to clarify the domain for some people, and/or some of the time?
lou1306 8y ago
On the other hand, from my limited experience in F# (but I guess OCaml would be similar) I found that, when you let the type inference algorithm do its thing, it can help you realize that your function is more general than you thought. For instance, you write a function for lists of strings and in the end it can actually work on any list. Maybe it's trivial, but I found it helped me thinking about refactoring/reusing my code in contexts I didn't expect.
- weberc2 8y ago
  You can still annotate the expression with the general type once you know what that type is. :)
- hinkley 8y ago
  Is it that hard to figure out that your method is generic? And what is this “end” you speak of? You don’t know what next year’s requirements are. Don’t confuse the implementation with the contract. That’s a variant of duck typing. If you need to do stringy things to the data later don’t advertise genericity. People will start using your function and then you’ll have to make a new method because they own the contract now.
  - lou1306 8y ago
    > If you need to do stringy things to the data later don’t advertise genericity. [...] People will start using your function and then you’ll have to make a new method because they own the contract now. I agree that my point doesn't really apply to functions that are part of some kind of API. Still, type inference is not duck typing: the former happens at compile time, unlike the latter. > Is it that hard to figure out that your method is generic? Well, it is not if you decide it to be generic from the start. What I was saying is that sometimes you start with "concrete" implementation, but the type inference helps you thinking about refactoring it to maximize reuse. Something like "hmmm, right now this method has signature 'a -> int -> 'b... I wonder if I can turn it into 'a -> ('b -> 'c) -> 'c and remove this other method that looks pretty similar..."
Drup 8y ago
My experience is that people who think that never worked with a language where inference is principal and complete (aka, "good") and/or have poor editor support. In languages that are still reasonably close to HM and that have decent editor tooling, like OCaml, leaving the type out in the implementation is the common practice. You only write them down in the external API (along with the documentation).
gameswithgo 8y ago
An interesting middle ground here is when the editor can annotate the function signature's types for you, with code lens type features. Of course this only works for people who happen to be in such an editor. Another issue I ran into recently was you can add a new type to your program, and break existing code. Where the type inference was able to deduce the type, and your new type appears to also be compatible, and now things don't compile and it is very mysterious why not! There can be some interesting big wins by leaving types off when possible though, like super easy refactoring. Just start passing ints to a big chain of functions and you are done. No need to change the signature of a big chain of functions.
CuriousSkeptic 8y ago
Or put another way: Compilers are good att figuring out what a function _can_ do. But humans need to specify what it _should_ do. Types aren’t always the right tool for that though. It would be interesting to see what could be done by integrating testing and typing, letting one inform the other.
SOLAR_FIELDS 8y ago
I definitely agree with this. Too often while learning Scala I’ve found myself scratching my head at some piece of code and wondering how to modify it because the typing system is inferring something I don’t expect it to.

georgewfraser 8y ago

For anyone interested in this subject, there's a great minimalistic implementation in OCaml here: http://okmij.org/ftp/ML/generalization.html http://okmij.org/ftp/ML/generalization.html The author starts with a naive implementation similar to the one linked here, then implements a series of optimizations that make it more efficient.

legulere 8y ago

The problem with advanced type inference is that the exact algorithm needs to be part of the standard for compability reasons (not just between compilers but also between compiler versions). So for me it makes more sense to have everything that’s beyond basic in something like a lsp-language server/ide.

gergoerdi 8y ago
> The problem with advanced type inference is that the exact algorithm needs to be part of the standard for compability reasons I don't think that's true -- if you have principal types, you can just say in your language spec that the principal type is inferred.
- lifthrasiir 8y ago
  It can be really tedious to list the cases where principal types do not exist. Haskell has a separate section for ambiguous overloading [1] for that reason, and more ad-hoc or advanced type systems will be harder to describe. [1] https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-790004.3.4 https://www.haskell.org/onlinereport/haskell2010/haskellch4....

renox 8y ago

I don't know much about this topic but I've heard that Hindley-Milner's type inference has also drawbacks as it doesn't work well with partial compilation and subtyping. So does the benefits outweight the drawbacks?

Drup 8y ago
HM type inference works perfectly fine with separate compilation and/or partial files (whichever you mean). See the OCaml tooling for a concrete demosntration. Subtyping is a fairly large domain, and it really depends what you mean. There are cases where it works fine (again, see OCaml) and other where it's more problematic (see Scala). In any case it's not really HM anymore, it needs to be more.
chombier 8y ago
As far as I know, subtyping with polymorphism looks much better since Stephen Dolan's thesis on Algebraic Subtyping http://lambda-the-ultimate.org/node/5393 http://lambda-the-ultimate.org/node/5393

teajunky 8y ago

Every article on Eli Bendersky's website is just great. If he ever writes a book I would immediately buy one.

always_good 8y ago

The upside of type inference is that making small changes to types upstream doesn't necessary incur changes to code downstream. But the downside of type inference is that it makes reading code harder and you may depend on an IDE to know what your intermediate types are. Especially wrt generics and higher-order types where intermediate function calls don't have a concrete type in their signature. Nothing demonstrates this better than any time you've written code yourself only to immediately invoke the IDE tooling to inspect what the type is. If you didn't know, good luck to the person reading it in git diffs. I've had to git clone someone's Rust project recently just to follow the type transformation across a bunch of future/stream chains. This isn't an argument against static typing but rather an argument against inference excess. There's a nice middle ground where asserting the concrete type in critical places makes the code more readable but also checks your own assumptions. Like any time you received Maybe<Maybe<Int>> where you wanted Maybe<Int>.

dllthomas 8y ago
> This isn't an argument against static typing but rather an argument against excess. And also an argument for exposing better tooling when reading git diffs :D
Klathmon 8y ago
A general rule of thumb I follow is to explicitly type your interfaces, and infer private internals. (I mean "interfaces" not referring to any specific language feature, but to the concept in general).
- steveklabnik 8y ago
  This is sorta where we landed with Rust; you have to type out type signatures of function signatures, but not inside function bodies. It's not based on public/private lines, but it's a similar idea.
  - deleted 8y ago
    [deleted]
  - 8y ago

abeppu 8y ago

I think he's using the term "bi-directional" in a potentially confusing and nonstandard way. As I understand it, in this area, that term typically describes a style of type checking and inference which arose later, and which involves both checking rules and synthesizing rules (the two directions), and which can be made to support some quite expressive type systems, but generally requires programs to have a sprinkling of explicit annotations. On that topic, I found these notes to be very helpful: https://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/15-bidirectional.pdf https://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/15-bid... But as I understand it, the concept started here: http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf

vilhelm_s 8y ago
Also, I think one should not call it Hindley-Milner. A key clever part of the HM algorithm is how it infers types for polymorphic functions, which this code doesn't do. For just the idea in this post, I suggest calling it something like "unification-based type inference", or "type inference using equational constraints".

piinbinary 8y ago

In case anyone finds it useful, I wrote an explanation of how type inference with let-polymorphism works: http://jeremymikkola.com/posts/2018_03_25_understanding_algorithm_w.html http://jeremymikkola.com/posts/2018_03_25_understanding_algo...