[pron]

It's not the halting problem. You can track worst-case computation complexity in the type system just as you do effects (why don't you jump about the halting problem when you need to "decide" if some effect will occur?). You can Google for it -- there are about a thousand papers on it. Just to give you an intuitive feel, think of a type system that limits the counter in loops. You can also look up the concept of "gas" in total languages. Something similar is also used in some blockchain languages.

You can even track space complexity in the type system.

[littlestymaar]

Are you really summoning non-Turing complete languages to the rescue here? This is hilarious.

We were talking about JavaScript, remember?

[pron]

First, no rescue is needed. I said that not tracking complexity is a matter of choice, and you mistakenly thought it amounts to deciding halting; I pointed out the well-known fact that it isn't. Second, you don't need a non-Turing-complete language in order to track computational complexity in the type system, just as you don't need a language that cannot perform IO in order to track IO in the type system.

As to JavaScript, there are much more commonplace things that it doesn't track in the type system, either, and they're all a matter of choice. There is no theory that says what should or shouldn't be tracked, and no definitive empirical results that can settle all those questions, either. At the end of the day, what you choose to track is a matter of preference.

[littlestymaar]

> I said that not tracking complexity is a matter of choice, and you mistakenly thought it amounts to deciding halting

And you implicitly acknowledged this fact by using TPL as example: you know, the class of language where all you can write is a provably halting program (that's the definition of Total programming languages!).

The halting problem being a property of Turing-complete languages, you just sidestepped the issue here.

[pron]

You can track complexity in Turing complete languages, just as you can track effects; neither should bother you more than the other. While doing either precisely amounts to deciding halting, the way it is done in programming languages does not (when we track effects the type system does not tell us an effect will occur, only that it may; similarly for complexity -- we track the worst-case complexity of a given term, which, for Turing complete languages, can be infinite for some terms, but certainly not all).