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

[Miles Sabin]

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.

Fair comment.

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' 
question.

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.

Cheers,


Miles