Re: [Haskell-cafe] Infinite types should be optionally allowed

From: Job Vranish On Sun, Feb 20, 2011 at 8:56 PM, Brandon Moore wrote:

...

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?

I haven't thought about checking against signatures. I think what you do is replace all the variables in the signature with Skolem constants, and unify the inferred type against that. There may be more complications if type inference is directed by the signature.

...

Usually systems add some sort ofad-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.

The restrictions I mentioned are supposed to allow using recursive record types to build an object system. It sounds like you want to allow infinite types only as specified by signatures. I think you could take a signature with explicit recursion, label those indicated cycles as allowed, somehow propagate the labels during unification, and check that the only cycles that appear are those specifically licensed by the signature. Brandon