Guaranteed termination of a sound dependent type system is only useful as a mathematical property, not a practical one (yes, I know the mathematical consequences have practical benefit but I mean directly it doesn’t say anything about what a typical user thinks of as “termination”). You could still trivially write an algorithm at the type level which is Turing-complete in a practical sense.
For example, write a type that implements a Turing machine parameterized by a program and a natural number N of evaluation steps to take. Apply that type to Graham’s number or some suitably large natural number. You now have a type that is, for all practical purposes, Turing-complete, even though it is theoretically guaranteed to terminate.
For example, write a type that implements a Turing machine parameterized by a program and a natural number N of evaluation steps to take. Apply that type to Graham’s number or some suitably large natural number.
To do that you’d first need to be able to fit Graham’s number into your source code which unfortunately is never going to happen.
Idris has a termination checker which in practice rejects non-primitive recursion. If you can’t prove to the type checker that your recursive function deferments toward a base case at every step then your program won’t type check. So there’s no back-door method to get Graham’s number or other silliness like the Ackerman function into your types.
Comments
Guaranteed termination of a sound dependent type system is only useful as a mathematical property, not a practical one (yes, I know the mathematical consequences have practical benefit but I mean directly it doesn’t say anything about what a typical user thinks of as “termination”). You could still trivially write an algorithm at the type level which is Turing-complete in a practical sense.
For example, write a type that implements a Turing machine parameterized by a program and a natural number N of evaluation steps to take. Apply that type to Graham’s number or some suitably large natural number. You now have a type that is, for all practical purposes, Turing-complete, even though it is theoretically guaranteed to terminate.
For example, write a type that implements a Turing machine parameterized by a program and a natural number N of evaluation steps to take. Apply that type to Graham’s number or some suitably large natural number.
To do that you’d first need to be able to fit Graham’s number into your source code which unfortunately is never going to happen.
Idris has a termination checker which in practice rejects non-primitive recursion. If you can’t prove to the type checker that your recursive function deferments toward a base case at every step then your program won’t type check. So there’s no back-door method to get Graham’s number or other silliness like the Ackerman function into your types.
I’ve done it in Agda - it’s not even hard. The naive definitions are accepted without issue.
https://github.com/mokus0/junkbox/blob/master/Agda/ack.agda