is type checking in D undecidable?

[Bruce Carneal]

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