Struggling with (higher-kinded?) polymorphism

[jbe]

@octachron

[…] it will use the name '_a to indicate that it is a weakly polymorphic type variable named a. The names weak%d are used for anonymous weakly polymorphic type variables. (I should update the manual to mention the underscore case).

Ah, so any type variable beginning with '_ is weak, and the weak part is just inserted when they are anonymous. Yeah, the manual is a bit misleading, though strictly speaking not wrong (it doesn’t say that those beginning with '_weak are the only weak type variables, but it is somewhat implied to the reader).

@octachron

However in general, you don’t want to use unification variables at all (except for some expert use cases).

I’m curious what’s wrong with them and when to use them and when not. I have used them a couple of times (especially with type constructors, like val f : 'a list -> 'a.

@octachron

You should use locally abstract types, either with the inline version:

let shuffle_convert (type i e o) 
  (input_conv: i -> e array) 
  (output_conv: e array -> o)
  (input i): o =
  ...

This brings me back to the previously discussed: Understanding type quantification and locally abstract types - #18 by jbe.

I’m not sure exactly why I would want locally abstract types. Afterall, they don’t protect me from this:

let shuffle_list_badsurprise (type a) : a list -> a list =
  shuffle_convert Array.of_list Array.to_list

Where I get:

val shuffle_list_badsurprise : '_a list -> '_a list = <fun>

Which is weakly polymorphic, as I learned. So the locally abstract types don’t ensure my function is polymorphic.

In that other thread, I (possibly wrongly) concluded:

@jbe

Locally abstract types may also be replaced (once and forever) by type inference with a concrete type (which is a different mechanism) or be polymorphic (like 't).

But that seems to be wrong:

# let x (type a) : a = 5;;

Error: The constant 5 has type int but an expression was expected of type a

So I think I still don’t fully understand what abstract local types do exactly.

To avoid the bad surprise above, I can also write:

let shuffle_list_rejected : 'a. 'a list -> 'a list =
  shuffle_convert Array.of_list Array.to_list

Error: This definition has type 'a list -> 'a list which is less general than
         'a0. 'a0 list -> 'a0 list

Same as I could write:

let shuffle_list_rejected : type a. a list -> a list =
  shuffle_convert Array.of_list Array.to_list

Error: This definition has type 'a list -> 'a list which is less general than
         'a0. 'a0 list -> 'a0 list

But my point is: In this case, I don’t need the locally abstract type to protect me from surprises, but I need the explicit polymorphic annotation (either using 'a. or type a.). So why and when should I use locally abstract types (other than when dealing with GADTs)? (Sorry if I have trouble understanding the concept, but I think it’s pretty complex to grasp.)