I think this article would be better if it ignored the issue of proving termination.
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.
> 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.
In practical algorithms of significance, we can often do much better than this, proving both termination, and the time complexity of that termination. For instance, a DFA of a regular language will terminate in O(n) of the length of the haystack, and we also have a bound for the time it takes to construct that DFA.
Sometimes, as you're alluding to, we know something terminates, but the time complexity is impractical: exhaustive naïve search for Traveling Salesman will, in principle, halt. This is, itself, useful information.
The article claims (I believe correctly) not just that H-M inference halts, but that it does so in "near-linear" time. That's a much tighter bound than merely proving termination.
If "near-linear" time was a bound it would be, but it's not. HM type inference is exptime-complete. Near-linear here is just "most programs people actually write type check in something close to linear time".
Complexity sometimes is still too little, because the constants can overwhelm your O(n) for all n that you care about in practice. Or rather, complexity can't help you to select between two competing O(n) algorithms
However, without a precise cost model of your operations (say, you just know each operation has a bounded time and such they are each O(1 ) but nothing beyond that), that's often the best you can do
There's something called resource aware computation that can do more finer grained bounds on the runtime and memory usage of functions (and other resource usage like stack space so you can prove you always use less than 8MB or whatever number) not only complexity but also the constants. With the right cost model you could model CPU and memory latencies and other things like CPU port usage, cache usage etc, but there's an interplay with the optimizer here (this could even be used to spot performance regressions of compiler codegen even without running any benchmark)
I don't necessarily disagree. But I do think there's something to be said for knowing that my sql query is "just" slow, not trapped in an infinite loop. Not confident, but I feel like debugging "why is this query so slow that it hasn't returned yet" seems easier than debugging "why has this slow-or-maybe-nonterminating query not returned yet".
The problem with “not writing code like that” is that eventually someone does.
At work we use a home-grown Haskell-like language with “row types” which can be split into disjoint sets of fields in order to represent joins and the like.
It works well in most cases, but it’s very easy to forget a type annotation and trigger unmanageable build-times. Often times, it is not obvious where something needs to be annotated. Sure, we can act as human time-outs, but the productivity loss can be substantial, especially for a newcomer to the language.
The solution to "eventually someone does" is "add a timeout, and when you hit that timeout give them an error so they can fix their code".
There's no practical difference between exponential and infinite time, you need to do this for bad exponential time cases anyways.
Many langauges type systems (Java, Typescript, C++, Rust, ...) really aren't guaranteed to terminate in the absence of a timeout either. They're (the type systems) turing complete, you can write infinite loops that the compiler can't know are infinite loops. This makes no practical difference relative to languages which "merely" have exponential time type systems, because with an exponential time type system you're alread accepting the risk that typechecking might not terminate before the heat death of the universe.
A timeout (or recursion/expansion depth limit) could be useful to give the human some specifics about what went wrong. But humans generally kill compilations that take much longer than usual. If it took 20 seconds before, and now it's run for 10 minutes and hasn't finished, I'm probably going to control-C it (or whatever), and then diff against the previous code to try to figure out what went wrong.
Yes, making it possible to reason locally about compiler performance can be pretty helpful. It’s one reason I like to have type declarations for public API’s. Also, hitting an implementation-defined limit (that you can raise) for unreasonable constructs might result in better errors than just continuing to run, but slowly.
A termination guarantee for type checking doesn’t really help.
I second this, for programs to terminate eventually, is not a good goal to pursue. In practice if you need termination, you will need bounded termination, which solves your eventual termination problem completely.
I don't understand why people talk so much about eventual termination.
Think of it not like proofs but like tests, i.e. it catches bad stuff.
Having static types is a low cost solution that catches a lot of possible bugs. Purity catches another bunch of bugs. No-nulls catches even more. At this point you can kinda start trusting function names and type signatures to do what they say on the box (often said about Haskell). Likewise, if it compiles, it probably does the right thing.
So where's the next gap in Haskell that lets bugs through? I'd argue that (eventual) termination would be that next step. If you say a function has type a->a (for all a), it only admits one possible implementation... except for bad ones, like 'undefined' or an infinite recursion - both of which termination would catch for you.
> If you say a function has type a->a (for all a), it only admits one possible implementation... except for bad ones, like 'undefined' or an infinite recursion - both of which termination would catch for you.
To be super-pedantic, it only admits one possible denotation, assuming termination. There are an infinite number of implementations that waste finite time on something useless before returning the argument. We usually don't talk about those, because... Why would you write code that does that? But it's worth keeping in mind as an edge case in this sort of discussion.
Cannot be optimized away? No. Will not be optimized away? Sure.
Given:
verySilly :: Int -> (a -> a)
verySilly = go . abs . toInteger
where
go n
| n == 1 = id
| even n = go (n `div` 2)
| otherwise = go (n * 3 + 1)
On a 64-bit platform, `verySilly 976532468728515` has type (a -> a) and will eventually terminate (the hailstone sequence is known to enter the 4-2-1 loop on all inputs that small), but no compiler is going to prove it. In theory it could happen. In practice it won't, especially when you consider that there are countless problems you could substitute in.
> I think this article would be better if it ignored the issue of proving termination.
I agree; that part went on so long that I got bored and stopped reading before the article actually got around to saying anything about type inference.
Can someone familiar with the territory recommend a better or complementary resource of similar level of approachability?
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.
For whatever it's worth, when I first wrote this I submitted it to /r/haskell (https://www.reddit.com/r/haskell/comments/cs7jyu/a_reckless_...) and it doesn't look like there were any corrections from that; and since then I've implemented an HM type checker and don't remember finding anything that made me think "oh, I was wrong about ...".
So I'm more confident in the essay than I was at the time. But yeah, getting put on guard by those caveats doesn't seem ideal for intro material. (But if I hadn't had them and I'd gotten something wrong, that would also not have been ideal...)
For writing the type checker, "write you a haskell" that someone else linked was really helpful, and so was a paper called "typing haskell in haskell": https://web.cecs.pdx.edu/~mpj/thih/thih.pdf
"Types and Programming Languages" by Benjamin Pierce is an excellent textbook (and approachable, even to people without formal CS education) that covers type inference and introduces a lot of the nomenclature/formalism gradually.
I don't know if it will be useful to you, but I worked up dependency-free parsers/type checkers in Rust for the "languages" defined in most of the chapters (at least the ones I cared about) https://github.com/lazear/types-and-programming-languages
This is nice and genuinely entertaining https://youtu.be/IOiZatlZtGU
(Propositions as types by phil wadler). Its true focus is the 1-1 mapping between type systems and logic systems, but it's well worth the watch.
The quoted paragraph is correct as written. E.g. if
f: ∀A, B. A -> B -> A
Then we have poly type π = "∀A, B. A -> B -> A".
The monotype μ = Str -> Int -> Str is a specialization of π, so we are also permitted to judge that f has type μ.
The type specialization operator "looks backwards", where we write sorta "π ≤ μ" because there's a kind of "subtyping" relationship (though most HM type systems don't actually contain subtyping) - anywhere that a term of type μ is used, a term of type π can be used instead because it can be specialized to μ.
> ... but I think this should be "π is a specialization of μ".
Can we reflect on how this person was so wary of reading the article for fear of being misled (instead of just reading it and afterwards reflecting/evaluating) because they were so sure it must be wrong (for whatever reasons) and it turns they themselves were wrong. This is called irony and dunning krueger.
I encountered HM a lot in my working life as a programmer. I did not expect that when I first encountered the names.
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!
They're only a pain if you need to know the run-time types of the elements. If you're just operating on them through a narrowly defined interface, that's just dynamic polymorphism, which is indeed more flexible with regards to future expandability, as long as you define the interface appropriately.
> as long as you define the interface appropriately
Well, if you have an interface that all entries adhere to it is not a heterogeneous list in my book. In Haskell that could be achieve without a sum type wrapper, but with a type class.
I mean, a heterogeneous list is literally a list where its elements may be of different types. To use a tired example, if a list that contains both a Cat and a Dog is not heterogeneous just because both adhere to the Mammal interface, then what is a heterogeneous list?
Native heterogeneous lists will often be convenient, and sometimes when you've used them they're going to turn out in retrospect to have been a bad idea but sometimes they'll be just fine, especially if they stay fairly locally scoped. I haven't done any serious work in a language that supports them for years, so I don't have a strong opinion about how often each of those cases happens.
But if you decide you want heterogeneous lists, but your language doesn't support them, so you try to implement that with a sum type, then that's basically always going to be a massive pain.
I'm not familiar with that technique and don't know what's going on from that snippet.
In Haskell, any time a heterogeneous list turns out to be fine, I expect to be able to model it. Often it'll look like "I'm applying a polymorphic function to every one of these list elements", and then you can either do a sum type (as discussed in the post) or an existential (which doesn't need you to list up front all the types you might use). If the function is "is negative?", it'll look something like (untested)
data SomeNum = forall a. Num a => SomeNum a
isNegative :: SomeNum -> Bool
isNegative (SomeNum n) = n < 0
numbers = [SomeNum (3 :: Int), SomeNum (5.2 :: Double), SomeNum valOfUnexpectedNumericType]
anyNegative = any isNegative numbers
...but it'll often be easier to just apply the `< 0` check to every element before putting them in the list. (If you have several functions you want to apply to them all, that's when the existential trick becomes more useful.)
So you can model heterogeneous lists in this case, and it's safer (because you can't put in a value that can't be compared to 0) but also less convenient. Whether that's an improvement or not will depend on the situation.
It's a slightly confusing name, though; it makes me think of a difference list, which seems to be a completely unrelated data structure (basically a rope).
You could construct a basically-equivalent data structure in Haskell, but I think normally you'd use an HList (defined in many places but e.g. https://hackage.haskell.org/package/HList-0.5.2.0/docs/Data-...). I've only occasionally had use for them myself, at any rate I don't think they're convenient for the "apply a function to all these elements" case.
In the technique I showed, I am using a difflist to enumerate a set of HTTP POST form fields and their expected types. This difflist type is defined in such a way that one of its type parameters gets inferred as a function type which takes the decoded values in the correct order and returns a record containing the decoded form. Eg from Field.[int "id"; string "name"] we get a type parameter int -> string -> 'a, where 'a is the type of the final decoded form.
This is the kind of real-world usage where difflists or heterogeneous lists shine. The same technique is used by this library to define type-safe GraphQL resolvers: https://github.com/andreas/ocaml-graphql-server
I'm still working at the same company as when I wrote this, and that company is still using Haskell (now mostly Typescript instead of Elm). If I did move on I'd ideally want to keep using Haskell, or failing that some other strongly typed language.
But I don't expect that my own experience says much about the language ecosystem in general. I don't particularly have an opinion on whether or not strong types have "won", and I didn't intend to comment on that question.
I would definitely choose a Lisp if it had an Intellij-like IDE. Especially since the type system of CL is good, though not static, obviously. But it's a tradeoff between having Haskell during compile time and CL during development time, for me.
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.