is type checking in D undecidable?

Bruce Carneal bcarneal at
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 
> design...

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 mailing list