is type checking in D undecidable?
bcarneal at gmail.com
Thu Oct 22 18:24:47 UTC 2020
On Thursday, 22 October 2020 at 18:04:32 UTC, Ola Fosheim Grøstad
> On Thursday, 22 October 2020 at 17:25:44 UTC, Bruce Carneal
>> 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?
More information about the Digitalmars-d-learn