6 ms·

Local type inference can give you 90% of the benefit at a fraction of the cost of a global type inference system. Simply introducing local variable inference p

Local type inference can give you 90% of the benefit at a fraction of the cost of a global type inference system. Simply introducing local variable inference probably captures 50+% of that and it's the simplest programming trick I ever saw. When I first came across it in the gosu code base (https://gosu-lang.github.io https://gosu-lang.github.io) I said: "Wait. That's all you do? You just take the type from the right hand side and then put it on the left hand side?" "Yep." "That's type inference?" "Yep." It called into question many aspects of my computer science education.

cheerlessbog 6y ago
Would it help with this case? https://news.ycombinator.com/item?id=23777197 https://news.ycombinator.com/item?id=23777197
cultus 6y ago
I've been really enamored of bidirectional type systems [0] lately, which seem to really give the best of all worlds. They explicitly separate inference from type checking, with the type checker switching between both modes during checking/inference. It's also more syntax directed, which makes good error messages easy. A pure HM type-system is pretty restrictive, so most ML family languages don't have global type inference anyway. [0] https://arxiv.org/pdf/1908.05839.pdf https://arxiv.org/pdf/1908.05839.pdf
- shpongled 6y ago
  Yea bidirectional systems are nice - one of the big benefits is that you can also have polymorphic function arguments, something you can't do in standard HM. I recently implemented the bidirectional system in Rust from the paper you linked, it was fun (and a challenge!) [0] https://bit.ly/2W96K2r https://bit.ly/2W96K2r
  - cultus 6y ago
    Wow! Very cool!
dependenttypes 6y ago
What do you mean by local type inference? Things like let? If so even languages without HM like Agda allow that. HM type inference is specifically for finding the type of the arguments of functions.
- jhanschoo 6y ago
  > You just take the type from the right hand side and then put it on the left hand side? That's what they mean by local variable inference
  - dependenttypes 6y ago
    I do not really understand what this means. Something like given y : yt and let x = y we can infer that x : yt?
    - jhanschoo 6y ago
      Yeah.
kccqzy 6y ago
I agree. C++ has had some form of local type inference when it comes to inferring template types, but in C++11 the auto keyword makes a tremendous improvement. Even in Haskell where global type inference is supported, people end up putting type signatures on all top-level declarations because doing otherwise makes code less readable and makes type error messages way too confusing. Global type inference means a single type error in a single function can be propagated by the compiler to arbitrarily faraway at the call site, or even several layers deep in a call site. Solving such errors resulting from global type inference simply isn't worth the time.
- secondcoming 6y ago
  auto can be dangerous in that it can introduce unexpected copies, i.e. auto vs auto&. You could just use auto&& and be correct most of the time (unless you actually want to make a copy). Herb Sutter's Almost Always Auto advice was not good, in my opinion. I still find I actually need to find out the actual type so when I use it it's only typically when the RHS of the assigment mentions the type, static_cast, make_unqiue etc. I find it saves on typing but not so much for readability. There are different rules if you're writing an STL algorithm versus a final concrete program.
- gnulinux 6y ago
  I've never written Haskell but I'm a Agda programmer (a Haskell dialect with dependent types) and I almost always put all the types and don't rely on type inference. The obvious exception is if something quick like a = b otherwise I'd always do a : Some -> Type -> MoreType a = f b Readability is a reason why. Types are extremely pedagogic tools. I believe when I think about my code, I just think about types. I don't think about computation, just the topology of types. Can I go to Int from X. If not why? This is very different than when I write Python code. So seeing types in code helps me a lot understand what's going on. But the real reason is: errors. It's so much more easier to understand errors when types are explicit.
  - kccqzy 6y ago
    Agda doesn't have HM-style type inference. Furthermore many times the type is the main content of the program, not so much the value.
pornel 6y ago
This falls short with generics, e.g. let map = HashMap::new(); // <K,V> unknown map.insert("hello", 1);
- eru 6y ago
  I think that works in Rust, and they only do local inference (in the same function).
- deleted 6y ago
  [deleted]
lmm 6y ago
That's "type inference" according to some people's definitions but not others. In any case it's pretty trivial; it only gives you 90% of the benefit if you're starting from a really low baseline.

cheerlessbog 6y ago

Would it help with this case? https://news.ycombinator.com/item?id=23777197 https://news.ycombinator.com/item?id=23777197

cultus 6y ago

I've been really enamored of bidirectional type systems [0] lately, which seem to really give the best of all worlds. They explicitly separate inference from type checking, with the type checker switching between both modes during checking/inference. It's also more syntax directed, which makes good error messages easy. A pure HM type-system is pretty restrictive, so most ML family languages don't have global type inference anyway. [0] https://arxiv.org/pdf/1908.05839.pdf https://arxiv.org/pdf/1908.05839.pdf

shpongled 6y ago
Yea bidirectional systems are nice - one of the big benefits is that you can also have polymorphic function arguments, something you can't do in standard HM. I recently implemented the bidirectional system in Rust from the paper you linked, it was fun (and a challenge!) [0] https://bit.ly/2W96K2r https://bit.ly/2W96K2r
- cultus 6y ago
  Wow! Very cool!

dependenttypes 6y ago

What do you mean by local type inference? Things like let? If so even languages without HM like Agda allow that. HM type inference is specifically for finding the type of the arguments of functions.

jhanschoo 6y ago
> You just take the type from the right hand side and then put it on the left hand side? That's what they mean by local variable inference
- dependenttypes 6y ago
  I do not really understand what this means. Something like given y : yt and let x = y we can infer that x : yt?
  - jhanschoo 6y ago
    Yeah.

kccqzy 6y ago

I agree. C++ has had some form of local type inference when it comes to inferring template types, but in C++11 the auto keyword makes a tremendous improvement. Even in Haskell where global type inference is supported, people end up putting type signatures on all top-level declarations because doing otherwise makes code less readable and makes type error messages way too confusing. Global type inference means a single type error in a single function can be propagated by the compiler to arbitrarily faraway at the call site, or even several layers deep in a call site. Solving such errors resulting from global type inference simply isn't worth the time.

secondcoming 6y ago
auto can be dangerous in that it can introduce unexpected copies, i.e. auto vs auto&. You could just use auto&& and be correct most of the time (unless you actually want to make a copy). Herb Sutter's Almost Always Auto advice was not good, in my opinion. I still find I actually need to find out the actual type so when I use it it's only typically when the RHS of the assigment mentions the type, static_cast, make_unqiue etc. I find it saves on typing but not so much for readability. There are different rules if you're writing an STL algorithm versus a final concrete program.
gnulinux 6y ago
I've never written Haskell but I'm a Agda programmer (a Haskell dialect with dependent types) and I almost always put all the types and don't rely on type inference. The obvious exception is if something quick like a = b otherwise I'd always do a : Some -> Type -> MoreType a = f b Readability is a reason why. Types are extremely pedagogic tools. I believe when I think about my code, I just think about types. I don't think about computation, just the topology of types. Can I go to Int from X. If not why? This is very different than when I write Python code. So seeing types in code helps me a lot understand what's going on. But the real reason is: errors. It's so much more easier to understand errors when types are explicit.
- kccqzy 6y ago
  Agda doesn't have HM-style type inference. Furthermore many times the type is the main content of the program, not so much the value.

pornel 6y ago

This falls short with generics, e.g. let map = HashMap::new(); // <K,V> unknown map.insert("hello", 1);

eru 6y ago
I think that works in Rust, and they only do local inference (in the same function).
deleted 6y ago
[deleted]

lmm 6y ago

That's "type inference" according to some people's definitions but not others. In any case it's pretty trivial; it only gives you 90% of the benefit if you're starting from a really low baseline.