is type checking in D undecidable?
Ola Fosheim Grøstad
ola.fosheim.grostad at gmail.com
Thu Oct 22 18:46:07 UTC 2020
On Thursday, 22 October 2020 at 18:38:12 UTC, Stefan Koch wrote:
> On Thursday, 22 October 2020 at 18:33:52 UTC, Ola Fosheim
> Grøstad wrote:
>> In general, it is hard to tell if a computation is
>> long-running or unsolvable.
> You could even say ... it's undecidable :)
:-) Yes, although you can impose restrictions on the language.
Something that is desirable for type systems. For instance, a
Prolog program may perhaps not terminate, but all Datalog
programs will terminate. But is Datalog expressive enough? Not
sure. Could be cool to try it out though.
Also, some advanced systems might be able to detect that no real
progress is possible. For example being able to prove that the
number of "subqueries" to be tried will increase faster than the
number of "subqueries" that can be resolved.
But this is really the frontier of programming language design...
More information about the Digitalmars-d-learn