(1) Hack until I've got something stable. Note: at the start of coding I typically don't quite know what the right abstractions are, so a lot of code (and associated types) are in constant flux.
(2) Once program is stable, wrap it in a module, let the compiler work out all types and put them in as module interface.
That gives me the best of all possible worlds: type annotations at abstraction boundaries but you don't have to type them out. Writing out explicit types inhibits fast change. I wish the languages I'm using at the moment (Scala, Rust, C++) allowed a flow like that. Alas, full type inference stops being possible with more expressive typing systems.
Because a program's types can serve as part of its documentation.
So many times I will accidentally return 42 or Result<Result<42>> when I mean to return Result<42>. With annotations, my error is instantly obvious. Otherwise I accidentally have a function that returns Result<Result<number>> and it may lead to a very weird error message when I use `foo().map(_ + 100)` somewhere else.
That's letting the computer doing more work, not less of it. Relying too much on inference can bow back into the human doing more of the work to figure out what the types actually are in a given spot.
The computer can only tell you what types your code _has_ (from inference), but not what type it _should_ have based on your intentions. Type inference can only complain when your code contradicts with itself (on a type level), but can't tell you when it contradicts with your intentions.
If you don't write out your intentions, you'd have to hover over everything to see if the inferred types differ from your expectations.
IDE hover types and collapsible type annotations (and alternatively also collapsible implementation) are still useful as a way to declutter your UI when reading code.
Right - that's not global type inference. It's intra-module type-inference.
Aside, when I decide to change where I put module boundaries, full program inference helps too: I just throw away the old module definitions, draw different boundaries and re-run inference.
I think their point is that they there were vanishingly few times where they were required to write explicit type annotations. As they say, mostly when dealing with data serialization. That doesn't say whether they wrote more, however.
0: There are plenty of places where not supplying a type annotation is more trouble than just writing it. Eg (Haskell since I'm not familiar with OCaml offhand):
data Foo = FooBar Int String
| FooBaz [Int]
It does make it easy. OCaml has a full matrix of types:
- Nominal product types (records)
- Nominal sum types (variants)
- Structural product types (objects)
- Structural sum types (polymorphic variants)
You could actually always use structural types and never have to actually define types. But OCaml people actually really like the nominal types because their typing rules are stricter and easier for people to understand. But the structural types can come in really handy, e.g. they give you a very convenient way to encode data between libraries that don't need to know about each other. E.g. there is an effort to add JSON-structured output to the OCaml compiler itself. This is using a polymorphic variant type to represent the JSON data type, to avoid having a dependency on any particular JSON library, but still being compatible with popular OCaml JSON libraries ( https://ocaml-community.github.io/yojson/yojson/Yojson/index... ).
If you wanted to, you could use
Either (Int, String) [Int]
Not in Haskell as far as I know, but (assuming MonomorphismRestriction) there's no technical reason why
data Qwe = Q a
qwe_eps :: Qwe
qwe_eps = Q ""
data Foo a b c = FooBar a b | FooBaz c
or
data Foo a b = FooBar a b | FooBaz [a]
But I agree that writing explicit type annotations is overall better practice.
quux :: a -> a
quux x = x
# quux takes any type genericly
frob y = y () ++ [()]
# frob takes some specific type, but we don't need to specify which (spoiler alert: it's () -> [()])
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?
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 neededIn 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).
My guess is that Rust's designers would reply that their compiler is slow enough without the complication you describe.
Just the opposite: type inference forces the type systems to remain simpler. Without type inference you could make them more complicated.
var a = 1;
slightly harder would be typing union / intersection types - e.g. this:
var a = some_test() ? "foo" : new Bar();
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;
let x = "foo" |> bar |> baz 5
Basically, there's two complications with type inference. One is type variables that you need to then "solve" - in my last example above, the type of parameter `x` would start as a type parameter α (usually denoted by Greek letters in type systems literature), then it would be "unified" with `int` when used "like" an int (i.e. passed to a function `+ : (int, int) -> int`).
This is what happens in a language with a "simple" type system like OCaml, with no subtyping. (OCaml is slightly more complicated, but still all equations that it needs to solve only involve equality (I think)). If your type system features subtyping, things get a bit more complidated.
(x) -> new List(x + 1, concat("test", x))
The other big issue type inference deals with, is generalization. If, at the end of inferring an expression's type, there are no equations involving a type variable (a bit of a simplification, but let's go with it), then it can be "generalized" - turned into polymorphic type.
(x) -> new List(x)
In your example, figuring the type of `x` is trivial compared to above - just take the return type of `baz`.
In eg Haskell, you often write the types first, even though in principle you seldom would have to write the types at all.
Do you genuinely rely on whole-program type inference? Writing fewer than ten explicit types in your whole career writing OCaml really surprises me. For example even the OCaml standard library is not written this way.
I find in practice most people explicitly type their top-level functions as if you don't this it can cause type errors at the point of use to 'poison' the function types and cause very confusing errors far away in the program. Do you not see this when you program without any explicit types?
We can see this in other projects for example Crystal which had to back-track on their goal of whole program inference, because it just doesn't really seem tractable in practice.