[Haskell-cafe] Decidable type systems? (WAS: Associated Type
miles at milessabin.com
Thu Feb 16 07:10:15 EST 2006
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: 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.
 Boolos, G., A Curious Inference, Journal of Philosophical Logic, 16,
1987. Also in Boolos, Logic, Logic and Logic, 1998. Useful citation
More information about the Haskell-Cafe