Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Technically speaking, for each program in a TC language we can have a program in a coinductive total language with the same observable behavior.

In nutshell to those who may not be familiar with the field: total languages differ from partial TC languages in that they must always include internally a "hit the reset button" exit from potential infinite loops, and this is enforced by the type system.

Since we can't actually observe an infinite number of program steps even in TC languages, this makes total languages effectively just as powerful as TC ones, but total languages are better-behaved in the sense that we can make a statically enforced distinction between provably terminating and possibly nonterminating code, therefore having all optimization/reasoning benefits in total parts, but also infinite processes in coindutive parts.



Well, I shrug to think about how people would create a program that runs for an indeterminate time (that's most useful ones) in a coinductive total language. Yes, in practice it must be possible.

Then, total languages are just a subset of the non TC languages, and those are as prone to accumulating technical debit as TC languages. For avoiding technical debit, one needs something much less expressive.


Kudos. I wish this point of view was as commonly accepted as you present it.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: