rank 2-polymorphism and type checking

[Janis Voigtlaender]

Hello, and thanks for the various answers!

Martin Odersky writes:
>
> Simon,
> 
> You are correct to have doubts. Indeed our system would not handle
> this case, as type variables can only be instantiated to monomorophic
> types, not to type schemes. The closest you can get to it is to wrap
> the instance type in a type constructor. I.e. `t' could be
> instantiated to
> 
> 	T (\c. forall d . (c->d) -> d -> d)
> 
> where T was declared
> 
> 	newtype T = T (\c. forall d . (c->d) -> d -> d)
> 
> But I guess that does not solve Janis's problem.
> 

I'm not sure whether it would. To make things more complicated, the application 
I had in mind would not only require a rank-3 type and quantification over a 
type constructor, but also polymorphic recursion. Hmm, I wanted to use the free 
theorem of g's type, but rethinking I wonder what this actually *means* in the 
presence of quantification over type constructors.
The whole story got so complicated, because I wanted to use a nested type of the 
form

 data D a = ... | forall b . F (b -> a) (D b)

If I settle for the less general but still useful

 data D a = ... | F (a -> a) (D a)

then I can do without any extensions :-)

Regards, Janis.


--
Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt@tcs.inf.tu-dresden.de