Why Infer Types? | Hacker News Reader

Why Infer Types?

npf.io

47 pointsingve29 comments

One pattern that I've seen in recently-designed programming languages is to make type declarations mandatory for function arguments and return values, but to make them optional for local variables. In other words, these languages do not attempt to perform program-wide inference.

One big advantage of this approach is that function types and return values are always documented in the source. But another advantage is that when type inference needs to look at many functions at once, then type errors are frequently misleading and they are reported far from the cause. By requiring parameter and return types to be declared, type inference will always report errors in the correct function.

It does also help to have a good IDE. rust-analyzer, for example, can show the inferred types of local variables, or even automatically insert the inferred type into the source code.

So basically PHP (except for the “requires” part)?

It does work quite well.

Yep, that's what Java (and Java IDEs) do.

> type inference will always report errors in the correct function.

Kinda! If you have a function calling another in apparent error, there are two functions that could be "the correct function" - maybe the call is wrong, or maybe the type signature on the called function is wrong (or potentially any of several called functions whose types interact in the calling function).

Now certainly you can report all of these locations, in which case the statement I quoted is true, but note that in principle you can also report all of the potentially involved locations when you have omitted some of the function type signatures.

You are very much correct that limiting the distance errors can drift is important in many contexts, and personally I strongly favor the "functions must have a signature" before a task in the code base is considered "done" (typically before merging to a shared repo), but I don't know that enforcing it in the language is the right call - deferring it during quick iteration until I've actually hit a potentially relevant type error is comfortable in Haskell, and in any case one has to be ready to add type signatures to better localize errors within a function.

Nitpick: the type of the returned value usually can be inferred from the 'return' statement.

Much of practice here can be summarised as: Code should read so that the intent of the programmer is clear.

Omit types where they arent relevant to understanding the code, include them where they are. Good code, then, only arises from good programmers who understand relevance and communication with code.

General prescriptions are no use. There is no correct whitespacing, no correct phrasing, no correct chunking, (and so on). There is only whether you have written code for the audience who will read it.

I suspect much of practice around software eng. here could be improved by peer challenges around program composition.

Here's my million dollar take:

The linter/typechecker should add in the inferred types explicitly. If you want to refactor, it's up to you to delete the types. Then a re-run of the linter/typechecker can re-check and add them back in.

For bonus credit, we should also automate the removal of unnecessary explicit types. A de-expliciter program should be able to go delete all explicit types which are inferable.

Personally I really like the spot readability of explicit types. I'd rather it be in the code, see the ripple out of changes to the codebase.

This idea of a separate phase modifying your input is really powerful, and I think more languages should design their syntax around that idea.

A nice example comes from AppleScript of all places. You can close a block with just `end`, or by referencing the opening like `end if`. When you save a file, the compiler rewrites all the `end`s to the second form.

Any other examples where the language is designed to be enriched by tooling?

I’ve been designing a new lightweight markup language for the past few months, and I have decided to take this approach for things like typographic punctuation: rather than the markup language engine embedding fallible heuristics (turning ' into ‘ or ’, based on the natural language’s usage) or annoying ligatures (e.g. TeX has -- → –, --- → —, ` → ‘ and ' → ’), I will provide a linter that provides flexible rules for such transformations and the ability to perform in-place replacement. This linter will also be able to perform source autoformatting of various kinds, e.g. visual alignment of list indentation and table columns, and it’ll be hooked into LSP so direct text editor integration is possible.

I'm building a language (https://flame.run) and trying a similar idea for imports. In my language there is no package manager. Files just import other files, locally or from URLs (like Deno). But, unlike Deno, I'd like to store the hashes of the imported files for security. I don't want to create a secondary file a la package.json, or even two files like go.mod/go.sum. So the idea I'm probably going with is that whenever you run/compile a program the tooling warns you and asks to insert the missing hashes of the imported files for you, inline.

Fun! that would be cool, but I wonder how this would work if a func just returns 4 and then the number type was added, and then I change it to return "wow". Do I have a type error or does my func type updates?

Good point. For this case, it's easy to imagine - such a construct would infer the function's new return type, and then any call-sites which have a mismatch would require updating. But you raise the real question of how the compiler could know when types were added by the inference-er versus the programmer

I think that if I were building a system that worked this way, automatically-inserted type declarations would be distinguished somehow (preferably in a way that in good text editors just appears as different formatting), and then when you change the function to return "wow" the compiler/linter/magic-type-annotator will see that the only things that need updating are ones it inserted itself, and just do it. If you edit any of those automatically-inserted type declarations, though, they're fixed and doing things that violates them becomes a type error rather than an auto-rewriting opportunity.

> If you want to refactor, it's up to you to delete the types.

The fact that

    f(g(x))

and

    { let y = g(x); f(y) }

are equally robust to changes in g(x)'s type is an advantage of type inference. It doesn't seem reasonable to place an additional burden on the person who chose to assign a name to the subexpression value.

> Personally I really like the spot readability of explicit types.

You can use an IDE that displays inferred types as type inlays (for variables) and as sidebar info (for expressions). But I've often wanted a way to export such sideband data (including subexpression types and cross-reference links) so you could display it for code reviews, etc, without teaching those tools about your language specifically, so I'm sympathetic to the general goal.

Regarding explicitness and readability, I like Rust's idea of letting you partially specify types by using _ as a placeholder to say "infer this part". For example, you can specify that something is a Vec without specifying its item type:

    let v: Vec<_> = iter.collect();

Explicit types are a form of assertion. In the example

    { let y = g(x); f(y) }

I do not want to assert anything on the type of y but in

    {
        let y: Foo = g(x);
        // Do complex stuff with y
        f(y)
    }

I wrote the middle part with a specific mental model of what y is, and if that changes, I want to review that section to make sure that the semantics still match what I thought they were and does not just happen to be valid syntactically.

I do not want some automated tool to either strip assertions from my code, nor do I want it to synthesize assertions from a static analysis run of a particular version of the code. If I'm just gonna mindlessly remove all assertions and re-synthesize them on every refactor, they're useless.

> You can use an IDE that displays inferred types as type inlays

This isn't captured in the code & that is a huge weakness. Being able to see the code change over time is, in my view, a huge advantage.

Reliance on high-tech tools to discern meaning & do the inference for us feels far weaker than simply encoding the good information into the code. That just seems far better to me, far more robust. Some of this is that I'm a vim user and don't want to have to go lookup & configure a LSP daemon for each file I evaluate, but some of it just feels like base common sense, that the tradeoff of actually being explicit are overwhelming & clear.

I think I argued against this pretty resolutely the first time around. I don't think your post adds anything or changes my mind at all.

I don’t like type inference myself. Code is read more than written. You really should be optimizing for better intent understanding than for easy typing. Types can usually be auto completed if they can be inferred.

I especially love the Java case with Idea. You infer the types, than IDE puts them back in as type hints (taking exactly the same amount of space). You end up with the same amount of code.

Also the example in the post is pretty bad. Your functions have an interface. You create them with some specific input and output in mind. With inferred types they can fit in many unexpected places. And they will be used in cases you have not anticipated. This has ripple effect. You end up with very generic type inferred as input for your functions (because it worked) and then you’re blocked from changing internals of the function as you cannot narrow the type.

Type inference isn't about reading or writing code. It's about proving that the code is correct with respect to the language semantics: type inference and checking are relatively lightweight forms of code verification. If you have code that works and passes the type checker, and upon modification fails the type checker, that often reveals issues about how that code composes with code that calls it. That isn't "blocking" you from modifying the internals of a function: if those modifications cause the type checker to fail, you've likely got a problem with how that function is used. It isn't trying to make your life difficult - it's telling you that assumptions you may have made about your code in isolation are not valid assumptions when considering how that code you're working on interacts with other code that you aren't focused on.

Type inference isn't an IDE feature related to autocompletion. If that's how you perceive it, you might benefit from learning what type inference is about and what role it plays in the development process.

> Type inference isn't an IDE feature related to autocompletion.

Except... it sorta is? The benefits you describe are real, but they are derived from type checking. In principle you can get the same effect while making all the types explicit. Without basic type propagation this is horrifically verbose to the point that no language I'm aware of rolls that way. Without type inference, it's usually manageable. Type inference is a (very!) nice to have feature on top of that where the compiler is kind enough to fill in the details it can figure out, which doesn't happen to live in the IDE (usually? ever?) but is basically the same idea as IDE autocompletion except that the result is not typically visibly reified (... outside of an IDE or equivalent).

What I disagree with from the grandparent is the notion that the type annotations (that inference allows us to remove) always or overwhelmingly improve readability. I think the verbosity they add - particularly when they get repetitive - means they often obscure far more than they enlighten. And when they do pay their way - which is not rare - you are still free to include the annotation!

It is true that code is read more than written, and I agree that code should be optimized more for easy understandability than for minimal characters typed.

But in some cases leaving types to be inferred helps with understandability, because sometimes the details of the type are cumbersome and almost always irrelevant, and leaving them in costs you more in readability than it gains you in explicitness.

This happens particularly often in C++, for instance, because C++ has a lot of ugly cumbersome types.

Here's an example from Meyers's "Effective Modern C++". You're writing a templated function that takes an iterator range and does something with the things within that range. At some point it needs a variable to hold one of the values.

    template<typename It> void f(Int first, Int limit) {
        while (first != limit) {
            auto v = *first;
            // ...
        }
    }

That's not so bad. But what if you want to make the type of v explicit? You need to write something like

    typename std::iterator_traits<It>::value_type v = *first;

instead. That isn't any more enlightening, it's extremely unlikely to make any bugs easier to track down, and it makes the code harder to read because there's this blob of useless type-nonsense getting in the way.

Another example from the same source; this time the issue isn't readability exactly but the fact that doing this stuff by hand is needlessly error-prone. (Again, specifically in C++ which is admittedly more error-prone than most languages.) You want to iterate over a std::unordered_map from string to int, like this:

    for (const auto & p : theMap) { ... }

On each iteration, p will be (a reference to) a pair whose first element is a string and whose second element is an int. But you want to make all your types explicit, so you write

    for (const std::pair<std::string,int> & p : theMap) { ... }

except that now you have a bug (which in this case only hurts performance) because actually what's in the map is pairs of const std::string and int, and that's a different type, so what your code will end up doing is copying every entry in the map into a temporary object before using it.

The tradeoffs probably favour explicit types more often in languages that are tidier than C++. But the tradeoffs are always there.

I honestly can't grasp this mentality. Very often types are so incredibly trivial that it makes no sense to include. Just like it would make no sense to write `1 + 1` as `((1: Int) (+: Int -> Int -> Int) (1: Int)): Int`. As if types add anything but clutter here. And many cases writing down types is just as unreadable as that.

Explicit types are important wherever you have an interface contract, because otherwise you may be basing your assumptions on a wrong understanding of what the actual contract is. Furthermore, explicit types serve to decouple interface from implementation. With (only) inferred types, you only have implementation, and client code is thus much more prone to relying on implementation details.

Arguably, every function or method can be regarded as having an interface contract, which is why it is useful to have explicit types there.

Personally, I also find it useful for local variables, because in a significant portion of code, the type of a variable is at least as important as its name, and guessing their type based on their name is worse than having the types be explicitly stated and visible at first sight. In particular in higher-level/domain logic code, variables are often the only ones with their specific type in the local scope. In many cases you therefore could in principle do without the name, the type would be enough.

I sometimes wonder if it could be practical to have a language allowing “anonymous” local variables, only identified by their type, as long as they’re (necessarily) the only one in their local scope with that specific type. That is, instead of writing `Foo foo = …` or `var foo = …`, have the ability to just write `Foo = …` in contexts where you only have one Foo. It would have the advantage that you know it’s a Foo (instead of guessing from the name as in `var foo`), and that the name can’t get out of sync with the type.

Scala’s implicits are something like that (though not for local variables). You can create a method signature like `listEntities(implicit connection: DBConnection)` and at call site if you have a DBConnection typed object in scope (and exactly one so it is obvious) it will be inserted automatically.

> Now if you want to change getFoo to return a Foo2, and doSomethingWithFoo to take a Foo2, you have to go change every place where these two functions are called and update the explicitly declared variable type.

This is wrong, and mixes up what side effects actually exist, and what questions you can ask the compiler.

getFoo is going to construct an object with some type that type must be assignable to its return type, and then that return type must be assignable to your declared variable type. declaring the type of your variable isn't just copying the type from the return signature, its a query to compiler about assignability (which is a query about ordering on the subclass relation).

You could imagine changing the type of the object, but not the return type of the function, or the return type of the function, but not the type declaration of the variable.

if you declared your variable to have a type and then try to assign that variable to the parameter (as the argument) of doSomething, you are again asking the compiler is my variable assignable to the parameter of this method.

if you are just "composing" 2 functions, then sure you might think of type declarations as boilerplate.

but if you think of variable assignments as queries to the compiler then you gain something by declaring types.

This doesn't even get into the ideas of variance and contravariance of the subclass relation over function types as well.

> if you think of variable assignments as queries to the compiler

Why should I?

I mean, I very much want to be able to make queries of the compiler and I think the notion of programming as productive conversation with the compiler (and other tooling) is a wonderful perspective. I should absolutely be able to ask questions of the compiler, and have it keep an eye on some things while I change other things. What I don't see is why I should be forced to make such a request just because I want to give some intermediate value a name. It seems to me that I should be able to do either, both, or neither of those as appropriate.

One interesting aspect is that if the language has any sort of implict type conversions/coercions, then type annotation can change program behavior in possibly surprising ways. For example https://blog.polybdenum.com/2022/04/25/when-type-annotations...

Somewhat unrelated to the article, but I always find the foo/bar style of code examples difficult to read. It's especially egregious here ; one of the points of the article is that types are often easy to guess from variable names, but it's very much not the case when the code is

  doSomethingWithFoo(foo)

I feel like simple but more realistic snippets are much better teaching tools.

Lol, Golang.

res, err = doSomething()

If there is an error how on earth does the res value make sense.

Just put getFoo inside doSomethingWithFoo.

Reply on news.ycombinator.com