Is instantiabilty of templated types decidable?

[Nick Sabalausky]

On Mon, 12 Nov 2012 00:46:06 +0100
Timon Gehr <timon.gehr at gmx.ch> wrote:

> On 11/11/2012 09:40 PM, Nick Sabalausky wrote:
> > On Sun, 11 Nov 2012 19:37:45 +0100
> > Timon Gehr <timon.gehr at gmx.ch> wrote:
> >
> >> On 11/11/2012 03:45 PM, Peter Alexander wrote:
> >>>
> >>> Collatz sequence.
> >>>
> >>> struct Collatz(int n)
> >>> {
> >>>       enum next = n % 2 == 0 ? n / 2 : 3 * n + 1;
> >>>       Collatz!(next)* foo;
> >>> }
> >>>
> >>> It's an unsolved problem in mathematics whether or not this
> >>> instantiates an infinite number of templates.
> >>
> >> The possible inputs are finite, so the property is decidable.
> >
> > Technically, yea, but I think upwards of ~4 billion template
> > instantiations is quite unrealistic, to the point of being
> > effectively undecidable.
> >
> 
> Undecidability has a precise definition in theoretical computer
> science. It means that there is no algorithm that implements the
> given predicate. It is a lot stronger than impracticality of
> implementation.
> 

I'm not disagreeing with that. But when the question is "Should the
compiler loop for days trying to instantiate millions, if not
billions of types for a design that's flawed and impractical (due to
said explosion of type instantiations)?", or something along those
lines, then the question of "undecidable versus unrealistic" becomes
irrelevent.

If there's laziness techniques that can drastically reduce the number
of instantiations the compiler actually needs to analyze/create, then
fine, but at some point it *still* has a decision to make of "Geez,
we've just created hundreds (thousands?) of recursive instantiations,
and in at least this particular case we have no fucking idea how many
more we might need, should we continue for a ridiculous amount of
time/resources, or just tell the user he's using an impractical
approach?" When you're facing that judgement call, it really doesn't
matter whether that "ridiculous amount of time/resources" is
technically finite or not.