rank 2-polymorphism and type checking
Janis Voigtlaender <email@example.com>
Thu, 25 Oct 2001 09:41:47 +0200 (MET DST)
Hello, and thanks for the various answers!
Martin Odersky writes:
> 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
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 :-)