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.

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.

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

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?

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.