is type checking in D undecidable?

[Bruce Carneal]

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.