Hindley-Milner Type Inference (2012)

Ocaml use Hindley-Milner type inference. I was taught programming with it and ended up deeply spoiled.<p>I could not understand why most static language required writing so many types that were easy to deduce and why people where saying that not having to write types made dynamic language better.<p>I can count on the finger of my hands the number of times when I needed to write explicit types in Ocaml (my single use case for explicit types in Ocaml was data deserialization).<p>Plus, the compiler is fast.

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&#x27;s the simplest programming trick I ever saw.<p>When I first came across it in the gosu code base (<a href="https:&#x2F;&#x2F;gosu-lang.github.io" rel="nofollow">https:&#x2F;&#x2F;gosu-lang.github.io</a>) I said:<p>&quot;Wait. That&#x27;s all you do? You just take the type from the right hand side and then put it on the left hand side?&quot;<p>&quot;Yep.&quot;<p>&quot;That&#x27;s type inference?&quot;<p>&quot;Yep.&quot;<p>It called into question many aspects of my computer science education.

The great thing about languages that implement HM types is that they allow you work as quickly or as carefully as you&#x27;d like without needing to change languages.<p>If you&#x27;ve done something a million times before and are familiar with how it works, you can leave off all the type hints, and it&#x27;ll figure them out for you and stay out of your way so that you can work more quickly. If you make a mistake somewhere, the compiler will still tell you.<p>If you&#x27;re doing something new, or don&#x27;t quite understand something, you&#x27;re free to add type hints wherever you need them to gain clarity. You can even do stuff like:<p><pre><code> let var: () = ...; </code></pre> if you have no idea what type something is and just want to ask the compiler for help.<p>Once you&#x27;re done, you can tidy up if you think it makes your code more readable. You can still leave top level hints to be kind to your coworkers or future you.<p>I think the ability to dynamically shift between &quot;cautious exploratory mode&quot; and &quot;reckless I-know-what-I&#x27;m-doing mode&quot; at the drop of a hat is why you hear a lot of anecdotes about people using languages like OCaml or Rust as if they were scripting languages.

This tutorial seems to miss the level-based generalization optimization, which is crucial for production-strength HM inference. For, that you can look at:<p><a href="http:&#x2F;&#x2F;okmij.org&#x2F;ftp&#x2F;ML&#x2F;generalization.html" rel="nofollow">http:&#x2F;&#x2F;okmij.org&#x2F;ftp&#x2F;ML&#x2F;generalization.html</a>

I had to implement this in Haskell while in university, we started with an interpreter for a Scheme-like language, then added static typing and inference.<p>Parser combinators, monads, monad transformers, curry-howard. Think for 15 minutes, write 5 lines of code, repeat. What I remember is that was code was really elegant but brain hurt so much.

Why is Damas dropped when referring to HM type inference? Not being critical, just genuinely curious. I imagine there&#x27;s a good reason.

I put 2012 as an upper bound on the year above: <a href="https:&#x2F;&#x2F;web.archive.org&#x2F;web&#x2F;20120324053910&#x2F;http:&#x2F;&#x2F;www.ian-grant.net&#x2F;hm&#x2F;" rel="nofollow">https:&#x2F;&#x2F;web.archive.org&#x2F;web&#x2F;20120324053910&#x2F;http:&#x2F;&#x2F;www.ian-gr...</a>. Perhaps it is earlier?

Learnt this in my compiler class.It was the most brutal week of my life.

If my understanding is correct, type inference producing a set of possible types - instead of a single type - for each term has proven to be undecidable?<p>This is a shame, because sum types (e.g. Shape := Circle U Square U Triangle) are actually pretty useful, and languages such as Java ended up implementing them via class or interface inheritance. Languages often also required type coercion to deal with things like 0.2 + 5, otherwise + could have had a type signature like: float U int -&gt; float U int -&gt; float U int.

One of my favorite resources that develop the HM algorithm from scratch is Ben Lynn&#x27;s[0], who treats it like a series of interview questions, because really type inference algorithms match up two trees into constraints, which can contain concrete types or type variables, then solves those constraints.<p>[0] <a href="https:&#x2F;&#x2F;crypto.stanford.edu&#x2F;~blynn&#x2F;lambda&#x2F;hm.html" rel="nofollow">https:&#x2F;&#x2F;crypto.stanford.edu&#x2F;~blynn&#x2F;lambda&#x2F;hm.html</a>

I code both ways simultaneously.<p>I&#x27;m interested in what types I need to solve my business problem. The rest of it, I don&#x27;t care. The reason I care about the types I need for my business problem is that I don&#x27;t want my code doing something that it shouldn&#x27;t: DDD-style coding allows me to code in such a way that it&#x27;s impossible for the program to exist in a state that&#x27;s invalid. That&#x27;s a great time-saver. Other than that, polymorphic coding FTW.

<i>The algorithm, the type system, and some of the logical background are explained in this tutorial, along with an implementation in standard ML.</i><p><a href="http:&#x2F;&#x2F;steshaw.org&#x2F;hm&#x2F;hindley-milner.pdf" rel="nofollow">http:&#x2F;&#x2F;steshaw.org&#x2F;hm&#x2F;hindley-milner.pdf</a> I found this 30 page PDF document very helpful in understanding the Algorithm.

One of the principal maintainers of the Racket language once gave a talk, I think it was at the main Clojure conference, on a topic about Typed Racket, where he strongly outlined the reasons why HM inference is a bad idea. It was interesting to hear these differences in philosophies.

This may be my favourite explanation of the algorithm&#x27;s logic: <a href="https:&#x2F;&#x2F;stackoverflow.com&#x2F;a&#x2F;42034379&#x2F;20371" rel="nofollow">https:&#x2F;&#x2F;stackoverflow.com&#x2F;a&#x2F;42034379&#x2F;20371</a>

I&#x27;m starting to understand why HMTI, and OCaml&#x2F;Haskell et. al., struggle from such obscurity despite its fanboys swearing by it. The problem is that it&#x27;s a crap technology in both easy mode and hard mode.<p>- easy mode: beginners just want to learn how to program as quickly as possible, something like python is fantastic for that. And the side-benefit, you can do amazing stuff with it, like bypass whole of symbolic AI of 80s and 90s (including HMTI, OCaml&#x2F;Haskell) and go straight to deep learning, BERT, GPT what not.<p>- hard mode: mathematicians would love a helpful computing system that&#x27;ll make them more productive mathematicians. When they attempt to explore stuff like Coq, and HoTT etc, the first thing that&#x27;s thrown at their face is that they have to give up law of excluded middle, non-constructive logic and what not. I&#x27;m sorry but the tail does not wag the dog. If your theorem assistants and checkers require the mathematicians to turn their world upside down, most won&#x27;t give a rat&#x27;s ass about what you have to say about propositions-as-types and programs-as-proofs.<p>There is a medium mode, or shall we say mediocre mode, whereby you fall in love with type-theory and type-based languages, you want to live in your own bubble and not be bothered by what&#x27;s happening in the outside world. And that&#x27;s were the users of these systems live.