On Thursday, 22 October 2020 at 18:04:32 UTC, Ola Fosheim Grøstad
wrote:
On Thursday, 22 October 2020 at 17:25:44 UTC, Bruce Carneal
wrote:
Is type checking in D undecidable? Per the wiki on dependent
types it sure looks like it is.
Even if it is, you can still write something that is decidable
in D, but impractical in terms of compile time.
Yep. Within some non-exponential CTFE speed factor that's
equivalent to saying your program might run too long.
You probably mean more advanced type systems where these things
are expressed more implicitly. Basically type systems where you
can express and resolve properties related to infinite sizes. D
does not have such capabilities, so you have to go out of your
way to end up in that territory in D.
Where "out of your way" means what? Use of templates with
potentially unbounded recursive expression? Other?
Per the wiki on termination analysis some languages with
dependent types (Agda, Coq) have built-in termination checkers.
I assume that DMD employs something short of such a checker, some
combination of cycle detection backed up by resource bounds?
