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.
