is type checking in D undecidable?
Ola Fosheim Grøstad
ola.fosheim.grostad at gmail.com
Thu Oct 22 18:33:52 UTC 2020
On Thursday, 22 October 2020 at 18:24:47 UTC, Bruce Carneal wrote:
> 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
"Decidable" is a term that means that there are some cases which
cannot be decided even if you had near infinite computational
resources at your disposal. So it is a very theoretical term, and
not very practical. I don't know what kind of solvers those
languages use, so I am not exactly sure what they mean by
"termination checker". In general, it is hard to tell if a
computation is long-running or unsolvable.
More information about the Digitalmars-d-learn