[Haskell-cafe] Decidable type systems? (WAS: Associated Type
miles at milessabin.com
Thu Feb 16 21:07:47 EST 2006
John Meacham wrote,
> > 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.
I was (unintentionally) playing fast and loose with terminolgy there.
What I really meant by "well defined" in the above was much weaker than
the context implied. I meant something more like "operationally useful
and agreed on" in the way that most informal or semi-formal specs are.
That's probably going to seem unsatisfactory to a lot of the readers of
this list, and I guess I could reasonably be accused of begging Andres'
But I stand by my original point. What I should have said in reponse to
Andres' is that it's all very well, but most (or at least a very large
proportion of) interesting problems are undecidable so, for those at
least, the benefits of a decidable specification are moot. Expressive
type systems, and programming languages in general, are a Good Thing,
and I'm prepared to trade expressive power for decidability. Having a
well understood and decidable fragment of such seems like a Good Thing
too, it's just that I don't see many circumstances under which I'd need
or want to restrict myself to working in that fragment.
More information about the Haskell-Cafe