In OCaml, what type definition is this: ‘a. unit -> ‘a

Questions

It was my first time I saw a type definition like 'a. unit -> 'a in Explicit polymorphic type in record

Q1: What is this 'a. (notice the dot)?

Q2: What is the terminology for this kind of type definition?

If I do

let f:'a. 'a list -> int = fun l -> List.length l;;

utop shows

val f : 'a list -> int = <fun>

Q3: Why doesn't utop shows the type 'a. 'a list -> int?

Q4: When should I use this kind of type definition?

In addition, I can use this kind of definition in record:

type t = { f: 'a. 'a list -> int};; (* this is correct *)

but I can't use it in variants:

type t = Node of ('a. 'a list -> int);; (* this is wrong *)

Q5: why?

Update / Summary

I did some experiments on this forall type definition as I can't find any articles on the web about this topic in OCaml and I want to induct to find out what's behind.

I summarise these experiments here and hope someone might give more insight.

From the answer below and its comments, I feel 'a. is a kind of force forall thing.

1. 'a. in function definition

let f:('a -> int) = fun x -> x + 1 (* correct *) 

Above is fine because OCaml is free to narrow down the type of f's parameter and replace 'a with int.

However,

let f:'a. ('a -> int) = fun x -> x + 1 (* wrong *)

This won't pass compiler, because it forces f to be applicable on all types via 'a.. Apparently, it is impossible from the definition part as the only possible type for x is int.

This example is interesting as it shows the logic and magic behind OCaml's static type inferring system. The types normally show themselves naturally from the function definition, i.e., you care more about what the function does, instead of giving a type first.

To me, it makes rare sense to really use 'a. when defining functions, as if the function's definition can handle all types, its type will naturally be 'a.; if the function anyway cannot handle all types, it makes no sense to force all types. I guess this is one of the reasons why the OCaml top-level usually doesn't bother showing it

2, 'a. in type inferring

let foo f = f [1;2;3] + f [4;5;6] (* correct *)

function f will be inferred as int list -> int because OCaml sees [1;2;3] first and it is a int list, so OCaml assumes f will take int list.

Also this is why the below code fails as the 2nd list is string list

let foo f = f [1;2;3] + f ["1";"2";"3"] (* wrong*)

Even if I know List.length would be a good candidate for f, OCaml won't allow due to the type infer system.

I thought if I force f to be 'a., then f can handle both int list and string list in foo, so I did:

let foo (f:'a. 'a list -> int) = f [1;2;3] + f ["1";"2";"3"];; (* wrong *)

It failed and OCaml seems not allow it. and I guess this is why you cannot always do type inference in the presence of impredicative polymorphism, so OCaml restricts its use to record fields and object methods.

3. 'a. in record

Normally I take 'a from the type parameter like this:

type 'a a_record = {f: 'a list -> int};; (* correct *)

However, the limitation is once you apply you get the concrete type:

let foo t = t.f [1;2;3] + t.f [4;5;6];;  (* correct *)

OCaml will infer t as an int a_record, not a 'a a_record anymore. So the below will fail:

let foo t = t.f [1;2;3] + t.f ["1";"2";"3"];; (* wrong*)

In this case, we can use 'a. as OCaml allows it in record type.

type b_record = {f: 'a. 'a list -> int};; (* correct *)
let foo t = t.f [1;2;3] + t.f ["1";"2";"3"];; (* correct *)

b_record is itself a concrete record type and its f can be applied on all types of lists. then our foo above will pass OCaml.