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

[Miles Sabin]

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

Cheers,


Miles