On Sun, Feb 20, 2011 at 8:56 PM, Brandon Moore
Typechecking with regular types isn't hard.
So do I have the right idea then? To check against a signature, I can just unify the two types and then check if the unified type is 'equivalent' (is there a special word for this kind of equivalence?) to the original signature? I've gotten the impression from multiple people that type checking with infinite types is hard. Maybe this isn't so?
The problem is, the type system is almost useless for catching bad programs. Every closed lambda expression is typeable if infinite types are allowed.
Yes, this part I understand quite well :) Usually systems add some sort of ad-hoc restriction on regular types, like requiring that all all cycles
pas through
a record type. Yeah, what I really want is just a better ad-hoc restriction or annotation. I quite routinely work with code that would be much more simple and elegant with infinite types. - Job