But I have little experience with these languages (I've mostly read about them) so I'd be interesting to hear about your experiences.
None of these are acceptable in Agda actually, since they would all be partial functions (i.e. functions that are not defined for some inputs.) The simplest, intuitive explanation is that since Agda has dependent types it needs to be able to evaluate functions during typechecking, and if you allow partial functions (e.g. infinite loops, halting functions, functions that timeout, or functions that are undefined for untested input) the typechecking would be undecidable.
Instead Agda has a bunch of built-in tools to help the compiler figure out if a function is total (the opposite of a partial function, meaning it's defined for all possible inputs). Things like the termination checker can detect a subset of all terminating functions, and sized types let the programmer aid the compiler in figuring this out. There are also language pragmas to overide this totality check on a per function basis.
I've implemented an algorithm, that I knew on paper terminated, and had it rejected by Agda, although I'm not experienced enough to know how easily these things are solved in general.
To quibble with "none of these are acceptable in Agda": it seems unlikely that Agda or anything like it would detect hangs or timeouts due to code not meeting its deadline. Deadlines and performance constraints are not part of any type system I've ever heard of. Furthermore, performance is dependent on the compile toolchain, the runtime, and what else is running on the same machine, so it's not even well-defined for static analysis unless you make a bunch of deployment-specific assumptions.
A language may guarantee that a function is total in a theoretical sense, but you might not be able to calculate its value for some inputs in practice. (Consider something like "a ↑↑↑ b".) So this guarantee is subtly different from what most users of computer systems would actually want.
Of course, as a another commenter pointed out, this sort of practical bug-finding is not actually what the termination guarantee is for.
Static analysis is a funny word to use about what Agda does.. Remember, Agda has dependent types, so what you're calling "static anaysis" involves evaluating/executing functions. In fact it needs to be able to evaluate/execute any functions beyond value-level in any imported modules just to be able to parse a sourcefile, due to the presence of mixfix-notation[0] and how it affects typechecking.
> Testing is rarely exhaustive. However, testing will find performance issues where static analysis won't.
How do you test a function that takes a natural number? Not an unsigned integer, but an actual countably infinite natual number? For every natural number n you test your function with, you can construct a new natural number n+1 which your function is untested for, (literally) ad infinitum.
The answer, of course, is mathematical induction[1] and in the case of more general data structures we have the more general structural Induction[2]. But at this point you don't call it testing, you call it proving, and it's this that Agda is aspiring to.
> To quibble with "none of these are acceptable in Agda": it seems unlikely that Agda or anything like it would detect hangs or timeouts due to code not meeting its deadline.
Yes, your right that actually detecting hangs or timeouts would be difficult or impossible. But that's not what Agda does. Agda only allows functions that the compiler can figure out are total, which can never be all total functions (otherwise we would have a solution to the halting problem I think.)
Basically, functions are either (provably total by the compiler) and hence acceptable. In the case of long/diverging computations Agda just has a timeout threshold, where it rejects a function if it takes too long to evaluate it during typechecking. I'm pretty sure that's what would happen if you tried "a ↑↑↑ b".
> Of course, as a another commenter pointed out, this sort of practical bug-finding is not actually what the termination guarantee is for.
Correct, it's not for bug-finding at all, but rather to keep the type theory/logic sound when using Agda as a proof assistant.
Just to be clear: your criticism makes a lot of sense from a software engineering perspective, but considering the general performance characteristics of Agda, and the almost noneexisiting tooling around it, I think we're a couple of years away from "deployment specific assumtions" being something Agda needs to be too concerned about :)
[0] You can define a function "if_then_else_" where the underscores represent arguments, so you would use it like this: "if TRUTH_VALUE then TRUE_CONSEQUENCE else FALSE_CONSEQENCE"
Not my experience, at least if we're talking about constructive type systems (I don't find best-effort-style "static analysis" useful, personally). I don't think I've ever seen any "normal" software testing regime (junit etc.) catch a performance issue that wasn't a straightforward infinite loop of the kind that would be obvious in something like Idris.
> quibble with "none of these are acceptable in Agda": it seems unlikely that Agda or anything like it would detect hangs or timeouts due to code not meeting its deadline. Deadlines and performance constraints are not part of any type system I've ever heard of.
Languages with a more detailed type system that can express maximum evaluation time (in terms of e.g. some set of "primitive ops" for that language) do exist, though I wouldn't consider any of them remotely practical.
> A language may guarantee that a function is total in a theoretical sense, but you might not be able to calculate its value for some inputs in practice. (Consider something like "a ↑↑↑ b".) So this guarantee is subtly different from what most users of computer systems would actually want.
Sure. Requiring totality doesn't eliminate all possible code-runs-for-too-long bugs, only the vast majority of them. I don't see that as a reason not to do it.
By "static analysis" I mean anything you can learn from studying source code without running it. (Though, with Agda this isn't a clear distinction; maybe we could talk about what we can extrapolate about whatever the compiler didn't evaluate.)
I was speaking of testing broadly to include manual QA and running benchmarks. A continuous benchmark will give a graph of the system's performance for certain actions. It's typically not pass/fail, but if the developers notice a regression they can investigate. These slowdowns just aren't correctness bugs as commonly understood and many places don't notice performance issues until after the code goes live and it's noticed via monitoring. (Benchmarks are tricky to write, tricky to run consistently, don't generalize, and miss a lot of things, but nonetheless measure things that static analysis doesn't even try to do.)
"Vast majority": I guess this depends on what you put in the denominator? I can certainly believe that Agda programmers don't see performance issues. But I'll confess ignorance: is this used for anything other than doing math?
I'm thinking more along the lines of: if a more mainstream language had totality checking, what bugs would this actually find in the code that runs in data centers? Plenty, I'm sure. But I can think of lots of things it wouldn't. It's one method of bug-finding among many.
Well we've got to compare similar levels of effort. I think most "normal" teams would find it easier to adopt a more detailed type system than to set up a continuous benchmark and use it effectively. I could be wrong.
> "Vast majority": I guess this depends on what you put in the denominator? I can certainly believe that Agda programmers don't see performance issues. But I'll confess ignorance: is this used for anything other than doing math?
> I'm thinking more along the lines of: if a more mainstream language had totality checking, what bugs would this actually find in the code that runs in data centers? Plenty, I'm sure. But I can think of lots of things it wouldn't. It's one method of bug-finding among many.
I don't know so much about Agda specifically. I agree with thinking about mainstream code that runs in data centers. My thought process was: of the code-runs-too-long bugs I've seen in my career, how many of those could have happened if I'd been working in Idris with totality checking on? I can only think of one (which was due to regex catastrophic backtracking), and I can think of several that would have been caught (the case where the test used the wrong overload of the function being the most production-impactey one).
My experience is that while other methods of finding bugs do exist, the cost/benefit for type systems is just so much better than anything else that I wouldn't even think about using any other technique until I'd tried type systems first.
I wouldn't start porting production systems to Idris just yet, but I do think it's worth adopting the same kinds of techniques: avoiding loops entirely, and making sure that when you do recursion it's very clear from the code what parameter is getting smaller in what sense.