4 ms·

How much simpler would OCaml or Standard ML be if there were no type inference? I'm perfectly happy to never use type inference (maybe only for local variables)

How much simpler would OCaml or Standard ML be if there were no type inference? I'm perfectly happy to never use type inference (maybe only for local variables). It feels like people get distracted by H-M inference and forget that there's a pretty nice high level language in SML or OCaml anyway (although I'd rather have modular implicits). Am I wrong in thinking implementation would be much simpler without type inference?

shpongled 6y ago
Implementation would be simpler, but only by a small degree. To be honest, HM is relatively straightforward to actually implement.
miloignis 6y ago
I think it depends on the algorithm & implementation, but in at least some cases type inference adds very little code over type checking. (To some degree, both are propagating and unifying types through the program and throwing an error when trying to unify two things that aren't the same. And depending on the language, you've got to have some non-trivial machinery for handling function overloads, which can require inference-y reasoning anyway (like calling an overloaded function immediately with the result of another overloaded function).) On the other hand, non-local inference can make things more complicated in some situations, depending on how hard you try. For instance, Rust gives up if you don't know the type of a variable and you try to accesses a member of it, where I once wrote a more complicated iterative solver that would see if it could infer the type of the variable from later context and return to the member access later. For example, consider the following Rust code where the compiler could figure out the types with some additional complexity but doesn't bother: fn main() { let a = (1..10).collect(); println!("{:?}", a.len()); let b: Vec<i32> = a; } error[E0282]: type annotations needed
- IggleSniggle 6y ago
  Your comment has me feeling quite bullish on TypeScript type inference
- chriswarbo 6y ago
  > To some degree, both are propagating and unifying types through the program and throwing an error when trying to unify two things that aren't the same In fact they're so similar that they can be combined to give 'bidirectional typing'. This is mostly useful for systems that are more expressive than Hindley Milner. For example, dependently-typed languages like Agda and Idris require type annotations for top-level definitions (local definitions can sometimes be inferred). Bidirectional typing is a neater approach to such hit-or-miss inference approaches, and also allows values to be inferred (your function-overloading example is a case of value inference: using the types to figure out which particular function to call).
- frank2 6y ago
  >Rust gives up if you don't know the type of a variable and you try to accesses a member of it, where I once wrote a more complicated iterative solver that would see if it could infer the type of the variable from later context My guess is that Rust's designers would reply that their compiler is slow enough without the complication you describe.
aspaceman 6y ago
There's some really cool programming language theory that makes things like type inference easier than you think. It's still hard but there's rules and math and stuff for all of it.
throwaway894345 6y ago
Local variables seems to be the sweet-spot for me, especially when I'm working on a project with others.
gnulinux 6y ago
HM is pretty easy implement actually. You just need a unification function, the rest is just a laundry list of rules available everywhere, like Wikipedia. Source: I implemented a typed python dialect as a college project that used HM.
eru 6y ago
> How much simpler would OCaml or Standard ML be if there were no type inference? I'm perfectly happy to never use type inference (maybe only for local variables). Just the opposite: type inference forces the type systems to remain simpler. Without type inference you could make them more complicated.
yawaramin 6y ago
You can't actually have a statically-typed language without type inference. Otherwise if you tell the compiler `(5 + 2) : String`, how would it report a type error?
- tomp 6y ago
  That’s not type inference, just type propagation - tons simpler.
  - yawaramin 6y ago
    Sorry but what's the difference? Inference is a way to infer the type of any given expression. How does type propagation contrast?
    - tomp 6y ago
      Propagation is way easier, and basically just requires tracking types of values & parameters. To infer the type of `a` in var a = 1; I just need to figure out the type of `1`, then realize that the type of `a` is the same. slightly harder would be typing union / intersection types - e.g. this: var a = some_test() ? "foo" : new Bar(); Java would "infer" (kind-of) the type of `a` to be something like `Serializable & Comparable<? extends Serializable & Comparable<...>>` as both `Serializable` and `Comparable` are supertypes of both `String` and `Bar` (well, depends on `Bar` of course). This starts to show how much trickier things can get. Now, imagine knowing nothing about what can be stored in the variable, and only seeing how it's used - this is the case for function parameters. (x) -> x + 1; Is `x` a `float`? An `int`? A `long`? Maybe a vector? Basically, imagine the most complex type you can write in a given language, and then consider, the compiler would need to be able to prove that this is the only (or at least the most specific) type you could use.
      - yawaramin 6y ago
        Hmm, all of your examples can be inferred by Hindley-Milner. Of course, for the second one it would be a type error assuming that `Bar` is not a subtype of `String`. I'm not seeing how type propagation of a complex expression could be any simpler or easier than full-fledged type inference of that expression. For example, let x = "foo" |> bar |> baz 5 What's the type of `x`? You might say that we can figure it out by propagation, but how's that different from inference?

shpongled 6y ago

Implementation would be simpler, but only by a small degree. To be honest, HM is relatively straightforward to actually implement.

miloignis 6y ago

I think it depends on the algorithm & implementation, but in at least some cases type inference adds very little code over type checking. (To some degree, both are propagating and unifying types through the program and throwing an error when trying to unify two things that aren't the same. And depending on the language, you've got to have some non-trivial machinery for handling function overloads, which can require inference-y reasoning anyway (like calling an overloaded function immediately with the result of another overloaded function).) On the other hand, non-local inference can make things more complicated in some situations, depending on how hard you try. For instance, Rust gives up if you don't know the type of a variable and you try to accesses a member of it, where I once wrote a more complicated iterative solver that would see if it could infer the type of the variable from later context and return to the member access later. For example, consider the following Rust code where the compiler could figure out the types with some additional complexity but doesn't bother: fn main() { let a = (1..10).collect(); println!("{:?}", a.len()); let b: Vec<i32> = a; } error[E0282]: type annotations needed

IggleSniggle 6y ago
Your comment has me feeling quite bullish on TypeScript type inference
chriswarbo 6y ago
> To some degree, both are propagating and unifying types through the program and throwing an error when trying to unify two things that aren't the same In fact they're so similar that they can be combined to give 'bidirectional typing'. This is mostly useful for systems that are more expressive than Hindley Milner. For example, dependently-typed languages like Agda and Idris require type annotations for top-level definitions (local definitions can sometimes be inferred). Bidirectional typing is a neater approach to such hit-or-miss inference approaches, and also allows values to be inferred (your function-overloading example is a case of value inference: using the types to figure out which particular function to call).
frank2 6y ago
>Rust gives up if you don't know the type of a variable and you try to accesses a member of it, where I once wrote a more complicated iterative solver that would see if it could infer the type of the variable from later context My guess is that Rust's designers would reply that their compiler is slow enough without the complication you describe.

aspaceman 6y ago

There's some really cool programming language theory that makes things like type inference easier than you think. It's still hard but there's rules and math and stuff for all of it.

throwaway894345 6y ago

Local variables seems to be the sweet-spot for me, especially when I'm working on a project with others.

gnulinux 6y ago

HM is pretty easy implement actually. You just need a unification function, the rest is just a laundry list of rules available everywhere, like Wikipedia. Source: I implemented a typed python dialect as a college project that used HM.

eru 6y ago

> How much simpler would OCaml or Standard ML be if there were no type inference? I'm perfectly happy to never use type inference (maybe only for local variables). Just the opposite: type inference forces the type systems to remain simpler. Without type inference you could make them more complicated.

yawaramin 6y ago

You can't actually have a statically-typed language without type inference. Otherwise if you tell the compiler `(5 + 2) : String`, how would it report a type error?

tomp 6y ago
That’s not type inference, just type propagation - tons simpler.
- yawaramin 6y ago
  Sorry but what's the difference? Inference is a way to infer the type of any given expression. How does type propagation contrast?
  - tomp 6y ago
    Propagation is way easier, and basically just requires tracking types of values & parameters. To infer the type of `a` in var a = 1; I just need to figure out the type of `1`, then realize that the type of `a` is the same. slightly harder would be typing union / intersection types - e.g. this: var a = some_test() ? "foo" : new Bar(); Java would "infer" (kind-of) the type of `a` to be something like `Serializable & Comparable<? extends Serializable & Comparable<...>>` as both `Serializable` and `Comparable` are supertypes of both `String` and `Bar` (well, depends on `Bar` of course). This starts to show how much trickier things can get. Now, imagine knowing nothing about what can be stored in the variable, and only seeing how it's used - this is the case for function parameters. (x) -> x + 1; Is `x` a `float`? An `int`? A `long`? Maybe a vector? Basically, imagine the most complex type you can write in a given language, and then consider, the compiler would need to be able to prove that this is the only (or at least the most specific) type you could use.
    - yawaramin 6y ago
      Hmm, all of your examples can be inferred by Hindley-Milner. Of course, for the second one it would be a type error assuming that `Bar` is not a subtype of `String`. I'm not seeing how type propagation of a complex expression could be any simpler or easier than full-fledged type inference of that expression. For example, let x = "foo" |> bar |> baz 5 What's the type of `x`? You might say that we can figure it out by propagation, but how's that different from inference?