is type checking in D undecidable?
bcarneal at gmail.com
Thu Oct 22 19:24:53 UTC 2020
On Thursday, 22 October 2020 at 18:46:07 UTC, Ola Fosheim Grøstad
> 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 ...
> 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.
I dont think it is any easier to prove the "will increase faster"
proposition than it is to prove the whole thing.
> But this is really the frontier of programming language
Agree. As I see it, D is on the frontier of practical (meta)
programming. A very exciting place to be.
On a related topic, I believe that type functions enable a large
amount of code in the "may be hard to prove decidable" category
(templates) to be (re)written as clearly decidable code. Easier
for the compiler to deal with and, more importantly, easier to
More information about the Digitalmars-d-learn