Many languages allow the type parameters of generic functions to be explicitly given.

As an example, if we have a function in Java or TypeScript with the following signature:

void f<T>();

…and a type MyType, we can write f<MyType>() to call f with type parameter T explicitly given as MyType.

Does OCaml have this feature?

If the answer is no – is this because the type inference of OCaml is so strong that a situation in which type application would be useful can never arise?

CodePudding user response：

OCaml type inference is principal outside of five exceptions (GADTs, higher-rank polymorphism, higher-order labeled functions, recursive polymorphism, and type-directed disambiguation). This means that the type inferred by the typechecker is always the most generic possible type and adding type annotations to some OCaml program can only transform a well-typed program into an ill-typed one, the reverse direction is not possible. (Once again outside of the advanced subset mentioned earlier).

In particular, the typing of function application is principal and the type of f x can always be inferred.

Thus it is neither needed nor useful to provide an explicit type argument à la System F to functions when writing an application.

CodePudding user response：

OCaml does not have ad hoc polymorphism. That is, you can't have a function behave differently based on the type of the arguments it's given or is expected to return. Therefore, the example you give from Java/TypeScript would simply be unsound in OCaml.

Additionally, OCaml allows type annotations on any expressions. Therefore there's no need for a distinct syntax specifically for function application. To annotate the return type of function application you could either do (f (): my_type) or let x: my_type = f () in ..., for example.