is type checking in D undecidable?

[Bruce Carneal]

On Thursday, 22 October 2020 at 18:46:07 UTC, Ola Fosheim Grøstad 
wrote:
> 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 
teach.