www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.learn - is type checking in D undecidable?

reply Bruce Carneal <bcarneal gmail.com> writes:
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.
Oct 22 2020
next sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
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.
Oct 22 2020
parent reply Bruce Carneal <bcarneal gmail.com> writes:
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?
Oct 22 2020
next sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
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.
Oct 22 2020
parent reply Stefan Koch <uplink.coder googlemail.com> writes:
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 :)
Oct 22 2020
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
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...
Oct 22 2020
parent reply Bruce Carneal <bcarneal gmail.com> writes:
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.
Oct 22 2020
next sibling parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
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).
Oct 22 2020
prev sibling parent reply Paul Backus <snarwin gmail.com> writes:
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.
Oct 22 2020
parent reply Bruce Carneal <bcarneal gmail.com> writes:
On Thursday, 22 October 2020 at 20:37:22 UTC, Paul Backus wrote:

 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.


Sure, most languages are Turing complete at run time.  A few are 
Turing complete at compile time but templates are also pattern 
matching code expanders. Polymorphic.

By design templates are open ended and powerful (in both the 
practical and theoretical sense).  In some situations they're 
exactly what you need.  They are also harder to employ correctly 
than functions.

When you write functions, the compiler helps you out with fully 
automated constraint checking.  When you write templates you can 
write them so that they look like simple functions, in which case 
you're on pretty solid ground.  Your manual constraints will 
probably work.  Hard to screw up a four line eponymous template 
with constraints.  Hard to screw up a "leaf" template with a 
small number of template args.  Possible but hard.  Not so hard 
to screw up 
"wanna-be-as-general-as-possible-but-special-case-performant-and-sometimes-wierdly-recursive-cuz-otherwise-th
-compiler-blows-up" templates.

It'd be great if we could get rid of many such templates, and, 
even more importantly, avoid writing a lot more.  That is likely 
when we start asking if type functions can reduce bugs long term, 
both those experienced in the currently tortured template 
subsystem and those experienced in user code.  The performance 
gains exhibited by type functions are, to me, just gravy.
Oct 22 2020
parent reply Paul Backus <snarwin gmail.com> writes:
On Friday, 23 October 2020 at 00:53:19 UTC, Bruce Carneal wrote:

 When you write functions, the compiler helps you out with fully 
 automated constraint checking.  When you write templates you 
 can write them so that they look like simple functions, in 
 which case you're on pretty solid ground.  Your manual 
 constraints will probably work.  Hard to screw up a four line 
 eponymous template with constraints.  Hard to screw up a "leaf" 
 template with a small number of template args.  Possible but 
 hard.  Not so hard to screw up 
 "wanna-be-as-general-as-possible-but-special-case-performant-and-sometimes-wierdly-recursive-cuz-otherwise-th
-compiler-blows-up" templates.


This is true, but it has nothing at all to do with 
decidability--which is a term with a precise technical definition 
in computer science.

The reason writing correct generic code using templates (or any 
macro system) is so difficult is that templates (and macros in 
general) are, effectively, dynamically typed. Unlike regular 
functions, templates are not type checked when they are declared, 
but when they are "executed" (that is, instantiated). In that 
sense, writing templates in D is very similar to writing code in 
a dynamically-typed language like Python or Javascript.
Oct 22 2020
parent Bruce Carneal <bcarneal gmail.com> writes:
On Friday, 23 October 2020 at 04:24:09 UTC, Paul Backus wrote:

 On Friday, 23 October 2020 at 00:53:19 UTC, Bruce Carneal wrote:

 When you write functions, the compiler helps you out with 
 fully automated constraint checking.  When you write templates 
 you can write them so that they look like simple functions, in 
 which case you're on pretty solid ground.  Your manual 
 constraints will probably work.  Hard to screw up a four line 
 eponymous template with constraints.  Hard to screw up a 
 "leaf" template with a small number of template args.  
 Possible but hard.  Not so hard to screw up 
 "wanna-be-as-general-as-possible-but-special-case-performant-and-sometimes-wierdly-recursive-cuz-otherwise-th
-compiler-blows-up" templates.


 This is true, but it has nothing at all to do with 
 decidability--which is a term with a precise technical 
 definition in computer science.


Yep.  The thread started with the technical definition, as you'll 
note in the wiki articles that I cited, and then moved on.  I 
probably should have started another thread.


 The reason writing correct generic code using templates (or any 
 macro system) is so difficult is that templates (and macros in 
 general) are, effectively, dynamically typed. Unlike regular 
 functions, templates are not type checked when they are 
 declared, but when they are "executed" (that is, instantiated). 
 In that sense, writing templates in D is very similar to 
 writing code in a dynamically-typed language like Python or 
 Javascript.


Yep. Good observations.  Functions offer some nice benefits.  I'd 
like to see their use increase (type functions displacing 
templates wherever appropriate).
Oct 22 2020
prev sibling parent reply Kagamin <spam here.lot> writes:
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.


What they do with code that does, say, a hash preimage attack?
Oct 23 2020
parent Bruce Carneal <bcarneal gmail.com> writes:
On Friday, 23 October 2020 at 16:56:46 UTC, Kagamin wrote:

 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.


 What they do with code that does, say, a hash preimage attack?


Not my area but after a quick wiki skim my guess is that the 
termination checkers would not be helpful at all.

If you do pick up one of the termination checker languages and 
experiment, please post back with the results.
Oct 23 2020
prev sibling parent Dennis <dkorpel gmail.com> writes:
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;
```
Oct 22 2020