5 ms·

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, sin

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.

deleted 2y ago
[deleted]
dmkolobov 2y ago
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.
- gpm 2y ago
  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.
  - AnimalMuppet 2y ago
    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.
- skybrian 2y ago
  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.
samatman 2y ago
> 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.
- skybrian 2y ago
  Yes, agreed.
- nextaccountic 2y ago
  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)
- gpm 2y ago
  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".
bmacho 2y ago
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.
- mrkeen 2y ago
  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.
  - chowells 2y ago
    > 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.
    - AlotOfReading 2y ago
      There's some useful cousins to the sleep() function in that family.
    - mrkeen 2y ago
      Are there any examples of such a function (a->a) which will eventually terminate, but cannot be optimised away at compile-time?
marssaxman 2y ago
> 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.
philh 2y ago
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".
- hun3 2y ago
  Yeah, if your table sources are small enouguh it will probably be fast enough to analyze anyway.

deleted 2y ago

[deleted]

dmkolobov 2y ago

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.

gpm 2y ago
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.
- AnimalMuppet 2y ago
  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.
skybrian 2y ago
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.

samatman 2y ago

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

skybrian 2y ago
Yes, agreed.
nextaccountic 2y ago
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)
gpm 2y ago
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".

bmacho 2y ago

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.

mrkeen 2y ago
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.
- chowells 2y ago
  > 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.
  - AlotOfReading 2y ago
    There's some useful cousins to the sleep() function in that family.
  - mrkeen 2y ago
    Are there any examples of such a function (a->a) which will eventually terminate, but cannot be optimised away at compile-time?

marssaxman 2y ago

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

philh 2y ago

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

hun3 2y ago
Yeah, if your table sources are small enouguh it will probably be fast enough to analyze anyway.