Is type checking in D undecidable?  Per the wiki on dependent types it sure looks like it is.

I assume that it's well known to the compiler contributors that D type checking is undecidable which, among other reasons, is why we have things like template recursion limits.

Confirmation of the assumption or refutation would be most welcome.

On Thursday, 22 October 2020 at 17:25:44 UTC, Bruce Carneal wrote:
> Is type checking in D undecidable?  Per the wiki on dependent types it sure looks like it is.

Even if it is, you can still write something that is decidable in D, but impractical in terms of compile time.

You probably mean more advanced type systems where these things are expressed more implicitly. Basically type systems where you can express and resolve properties related to infinite sizes. D does not have such capabilities, so you have to go out of your way to end up in that territory in D.

On Thursday, 22 October 2020 at 18:04:32 UTC, Ola Fosheim Grøstad wrote:
> On Thursday, 22 October 2020 at 17:25:44 UTC, Bruce Carneal wrote:
>> Is type checking in D undecidable?  Per the wiki on dependent types it sure looks like it is.
>
> Even if it is, you can still write something that is decidable in D, but impractical in terms of compile time.

Yep.  Within some non-exponential CTFE speed factor that's equivalent to saying your program might run too long.

>
> You probably mean more advanced type systems where these things are expressed more implicitly. Basically type systems where you can express and resolve properties related to infinite sizes. D does not have such capabilities, so you have to go out of your way to end up in that territory in D.

Where "out of your way" means what?  Use of templates with potentially unbounded recursive expression?  Other?

Per the wiki on termination analysis some languages with dependent types (Agda, Coq) have built-in termination checkers.  I assume that DMD employs something short of such a checker, some combination of cycle detection backed up by resource bounds?

On Thursday, 22 October 2020 at 18:24:47 UTC, Bruce Carneal wrote:
> Per the wiki on termination analysis some languages with dependent types (Agda, Coq) have built-in termination checkers.
>  I assume that DMD employs something short of such a checker, some combination of cycle detection backed up by resource bounds?

"Decidable" is a term that means that there are some cases which cannot be decided even if you had near infinite computational resources at your disposal. So it is a very theoretical term, and not very practical. I don't know what kind of solvers those languages use, so I am not exactly sure what they mean by "termination checker". In general, it is hard to tell if a computation is long-running or unsolvable.

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 :)

On Thursday, 22 October 2020 at 17:25:44 UTC, Bruce Carneal wrote:
> Is type checking in D undecidable?  Per the wiki on dependent types it sure looks like it is.

It is indeed undecidable. Imagine you had a decider for it. Because CTFE is clearly turing-complete, you can express that in a D function `bool typeChecks(string code)` and then do this (similar to the halting problem):
```
enum int x = typeChecks(import(__FILE__)) ? "abc" : 100;
```

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

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.

On Thursday, 22 October 2020 at 19:24:53 UTC, Bruce Carneal wrote:
> I dont think it is any easier to prove the "will increase faster" proposition than it is to prove the whole thing.

They probably just impose restrictions so that they prove that there is reduction and progress over time. One common for strategy for proving termination is that something is reduced every iteration (or at some points in the program that is passed through).

On Thursday, 22 October 2020 at 19:24:53 UTC, Bruce Carneal wrote:
> 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.

Type functions, like regular functions, are Turing-complete, and therefore undecidable in the general case.