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

[Miles Sabin]

Martin Sulzmann wrote,
> By possible you mean this extension won't break any of the existing
> ATS inference results? You have to be very careful otherwise you'll
> loose decidability. 

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.

There's a very nice paper by George Boolos on this[1]: he gives an 
example of an inference which is (and is intuitively) valid in second- 
order logic, and which can be first-orderized ... but the proof of the 
first-order equivalent is completely unfeasible.

[1] Boolos, G., A Curious Inference, Journal of Philosophical Logic, 16,
    1987. Also in Boolos, Logic, Logic and Logic, 1998. Useful citation
    here,

http://www.nottingham.ac.uk/journals/analysis/preprints/KETLAND.pdf

Cheers,


Miles