Hacker News Reader

Comment by recursivedoubts | Hacker News Reader

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) 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.

View on HN

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.

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.

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.

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.

This is true, I should have mentioned it, although my point still applies to HM style type inference as well.

To a point at least, HM type inference is decidable, but type inference in haskell with certain extensions or in agda (at least with certain pragmas) is not.

The possibility of a diverging type-level function would require the type inference algorithm to solve the halting problem.

(As I understand it at least, been a while since I got into the details)

Python has optional typing though.

Python has optional type hinting for optional static analysis tools (e.g. mypy). Types aren't checked at runtime.

The terminology I used was correct. Python has optional typing. What you are thinking of is gradual typing which Python lacks. See "Is Sound Gradual Typing Dead?" for a description on what the differences are.

If you pass a string-typed var to a func with an int-typed parameter, it will not fail at runtime. `python the_file.py` will not even emit a warning, much less a failure, because there's absolutely no runtime difference between "has types" and "does not".

That's not optional typing. It's just a standardized magic comment (which the reference implementation ignores). It's far from useless, but it's not adding typing to the language.

Yes, that is "optional typing." Read the article I referenced.

That appears to be a doc about Racket, which it implies does have run-time checks, from the third sentence here:

>In particular, Typed Racket’s run-time system remains largely untyped. As a result, even the completely typed configurations of our benchmarks usually import constants, functions, and classes from an untyped module in the run-time system. When these values cross this boundary at run-time, the contract system performs checks, and that imposes additional costs.

But I haven't read the whole thing. It doesn't appear to be very related - it seems to be about gradual typing in a language that does run-time checks (with ways to disable them for performance purposes).

Typed python has no additional checks than untyped. So it's still untyped. You wouldn't claim my "// int" comments add optional typing to JavaScript, would you?

---

edit: here, take it from the source instead: https://docs.python.org/3/library/typing.html Note the title is "support for type hints" and this prominent note is right at the top:

>Note: The Python runtime does not enforce function and variable type annotations. They can be used by third party tools such as type checkers, IDEs, linters, etc.

It's not a doc about Racket, it's a conference paper. Had you read it you would have found "Optional typing can be traced as far back as MACLISP, which allowed users to declare (unchecked) type specifications [15, §14.2] in an otherwise untyped language." and "Contemporary optional type systems have been developed for Clojure [8], Lua [14], Python, [10]," where the footnote references MyPy. Type hinting is the mechanism through which optional typing is implemented.

MACLISP I can't really comment on as I don't know it and Wikipedia makes no mention of this, but yeah - MyPy is definitely an optionally-typed python code checker. It fits that category for both comment-based and in-language type hints, because it performs checks based on that info.

For Python itself though: if you have a syntactic element which does not change behavior in literally any way, whether present or absent and regardless of what it contains: sounds like a comment to me.

so, I'm curious, do you write the type of the function first?

When I used to write haskell, I'd very often write a function, iterate on it until it did what I want, then infer the type of the function and insert that into the program. Now, I was relatively new to haskell, so was probably less comfortable writing types than reading them (so I assume it was nicer to have the compiler do that for me, eyeball it to check it's what I meant to do, and put it in).

I'm wondering if someone more familiar would think "alright, what type do I want my function to be", fill that in, and then write the type out?

I definitely agree that a program is more readable with types, which is why I always filled them in (I just did it afterwards!)

I do both in Haskell. Sometimes I write the types first and sometimes I write the function first.

Usually, the functions with more imperative flavour get their implementation first, and the more functionally flavoured bits get their type first. But that's not always the case.

Sometimes I even write the QuickCheck properties first.

Again, can't speak for haskell.

In agda you usually have 2 goals creating a function

* Proving a property of some other object. In this case you have to write the type first since type is the theorem you want to prove, and implementation is the proof.

* Implement a transformation. In this case, as you described you might get away first writing the impl, and then the type, but I personally never even attempt to do that since writing out the type gives me a lot to think about the implementation of the transformation. Once types are explicit, implementation usually ends up being a lot more obvious.

Type inference in C++ (and Go) is still very limited. It only works in the 'forward' direction.

In Haskell, OCaml and eg Rust, the compiler can infer the type of a new variable depending on how you are using it later.

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.

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.

> 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

I do not really understand what this means. Something like given y : yt and let x = y we can infer that x : yt?

Yeah.

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

This falls short with generics, e.g.

    let map = HashMap::new(); // <K,V> unknown
    map.insert("hello", 1);

I think that works in Rust, and they only do local inference (in the same function).

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

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

Wow! Very cool!

Reply on news.ycombinator.com