Re: is type checking in D undecidable?
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.
Re: is type checking in D undecidable?
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?
Re: is type checking in D undecidable?
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-the-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).
Re: is type checking in D undecidable?
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-the-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.
Re: is type checking in D undecidable?
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-the-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.
Re: is type checking in D undecidable?
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.
Re: is type checking in D undecidable?
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).
Re: is type checking in D undecidable?
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.
Re: is type checking in D undecidable?
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...
Re: is type checking in D 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; ```
Re: is type checking in D undecidable?
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 :)
Re: is type checking in D undecidable?
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.
Re: is type checking in D undecidable?
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?
Re: is type checking in D 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. 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.
