[Haskell-cafe] Infinite types should be optionally allowed

[Brandon Moore]

>From: Job Vranish <jvranish at gmail.com>
>On Sun, Feb 20, 2011 at 8:56 PM, Brandon Moore <brandon_m_moore at yahoo.com> 
>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