[Haskell-cafe] Type-level naturals & multiplication

[Brad Larsen]

On Tue, Oct 13, 2009 at 3:37 AM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
[...]
> It's also worth noting that while "undecidable" instances sound scary, but all it means is that the type checker can't prove that type inference will terminate.  We accept this lack-of-guarantee for the programs we *run*, and type inference can (worst case) take exponential time which is not so different from failing to terminate; so risking non-termination in type inference is arguably not so bad.
>
> Simon

Indeed!

On a related note, template instantiation in C++ is undecidable.  See
``C++ Templates are Turing Complete'' by Todd Veldhuizen:
<http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.3670>.
And similarly, heavy use of templates in C++ can be *extremely*
compute-intensive.

Sincerely,
Brad