Hacker News new | ask | show | jobs
by gnulinux 1549 days ago
E.g. you can require all programs to halt, which makes the language non-TC since the language has a trivial solution to its halting problem. There are other ways too, but this is approach e.g. Agda takes.

Note that you can still build useful programs this way since such languages can still allow certain forms of recursion such as primitive recursion, structural recursion etc... You can also use sized types [1] to allow even a larger set of (halting) programs.

[1] This is a way of compiler statically analyzing the size of each type (i.e. how many recursive constructors necessary) which puts an upper bound on the number of recursions need to be performed.