Is a record with polymorphic methods rank 1?

user_2637899 0
Viewed 54

From my understanding:

  • OCaml uses rank 1 polymorphism
  • In rank 1 polymorphism all quantifiers must be at the outermost (prenex) position

However the following is possible to type:

type 'a myArray = { map : 'b. ('a -> 'b) -> 'b myArray; }

Where the type quantifier 'b is nested. In fact, this can be used to simulate higher rank polymorphism in OCaml).

So can there be nested type quantifiers in rank-1 polymorphism, such as this case? And the type system is still predicative, i.e. full type inference is possible?

polymorphism ocaml
1 Answers

Type inference is still possible because myArray is named, giving hints to the type inference.

The moment the typechecker sees a map field, it knows to use a 'a myArray and hence knows exactly where the quantifier should be.

In a way, because a record is named and with a type definition, there is no need to infer what has to be in the type definition. Note that this wouldn't be possible with tuples as they don't rely on an external definition and are fully inferred.

user_32102570
Related