[Haskell-cafe] Decidable type systems? (WAS: Associated Type Synonyms question)

[John Meacham]

On Thu, Feb 16, 2006 at 12:45:03PM +0000, Miles Sabin wrote:
> Andres Loeh wrote,
> > If a problem is decidable, it has the nice property that the problem
> > (*not* the algorithm) can be used as a specification. Implementors
> > are free to implement different algorithms, as long as they all solve
> > the problem. If the problem is undecidable, how do you make sure that
> > different compilers accept the same programs? If you don't want to
> > find a subproblem that is decidable, you'll have to specify an
> > algorithm, which is usually far more complicated, error-prone, and
> > difficult to grasp for programmers.
> 
> Again, I'm not sure that decidability helps practically here: we're not 
> interested in "compiler A and compiler B accept the same programs", 
> we're interested in "compiler A and compiler B accept some well defined 
> subset of possible programs in a reasonable amount of time and space".

But it seems that well defining that subset is equivalent to the problem
of finding a suitable decidable algorithm.

        John 

-- 
John Meacham - ⑆repetae.net⑆john⑈