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

[Andres Loeh]

> Can someone explain to me why decidability is of any practical interest 
> at all? What's the (practical) difference between a decision procedure 
> which might never terminate and one which might take 1,000,000 years to 
> terminate? Actually, why push it out to 1,000,000 years: in the context 
> of a compiler for a practical programming language, a decision 
> procedure which might take an hour to terminate might as well be 
> undecidable ... surely all we really need is that the decision 
> procedure _typically_ terminates quickly, and that where it doesn't we 
> have the means of giving it hints which ensure that it will.

I'm tempted to agree with you. I don't care if the compiler terminates
on all my programs, or if it sometimes quits and says: "I don't know if
this is correct." However, I do think that it is of very much importance
that programmers and compiler implementors know which programs are legal
and which are not.

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.

Cheers,
  Andres