Proving that a program terminates eventually is a very weak guarantee, since it could be a program that terminates after a million years. This matters mostly for proof languages, where it’s useful to write proofs about functions that you never run. If the function provably terminates, you can assume that whatever value it returns exists, without calculating it.

For a possibly long-running job like a SQL query, a static guarantee that it terminates eventually is almost certainly not what you want. You’re going to need to test its performance, and ideally have a timeout and a way of handling the timeout. If you want to get fancy, a progress bar and cancel button might be nice.

Edit:

Compilers need to run fast for the programs we actually write. A type system that possibly doesn’t terminate under unusual conditions isn’t that big a deal, as long as people don’t write code like that. Hopefully you get a decent error message.

Compare with memory use. We don’t want compilers to use excessive amounts of memory, but don’t need static guarantees about memory use.

The intro here flags that the author i) is not happy with the post in its current form, ii) was resynthesized from wikipedia "without particularly putting in the effort to check my own understanding", which doesn't inspire confidence.

And then when you do get into the content, stuff looks incorrect, but a non-expert reader, given the caveats in the intro, should be on the lookout for errors but isn't equipped to identify them with confidence. E.g. the very first inference rule included is described as:

> if you have a variable x declared to have some polytype π, and if the monotype μ is a specialisation of π, then x can be judged to have type μ

... but I think this should be "π is a specialization of μ".

Basically, I think this is the kind of material where detail matters, where errors seriously impede understanding, and a resource where the reader/learner has to be on guard second-guessing the author is a bad intro resource. But surely there are better ones out there.

From the article:

> HM type systems can't implement heterogenous lists [...] > [well it does when wrapping the elements in a sum type, but then] > it can only accept types you know about in advance. > [which makes it] a massive pain to work with.

Sorry, I totally disagree... Heterogeneous lists without the sum types are a massive pain! Maybe it is easier for the initial development effort, but if you need to maintain code with heterogeneous lists (or dynamically typed code in general) the pain will come at some point and likely when already in production.

I much rather fix compile errors than runtime errors. And a massive thanks to Hindley and Milner for advancing type systems!

Found their photos in gratitude just now:

https://www.researchgate.net/profile/J-Hindley

https://en.wikipedia.org/wiki/Robin_Milner