is type checking in D undecidable?

[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 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...