Polymorphism in OCaml - ad hoc,parametric, inclusion/subtyping

Question

I am having a problem understanding the different types of polymorphism, specifically in regards to OCaml. I understand that polymorphism allows for multiple types in OCaml denoted as 'a, but I do not understand what the different types of polymorphism are.
If someone could give me an explanation with relatively low-level language that would be awesome! ad hoc, parametric, inclusion/subtyping

Answer 1

I actually don't think this kind of question is particularly suited to the strengths of Stack Overflow. There are entire books written about types. In fact, I'd recommend reading Types and Programming Languages by Pierce, which I found to be extremely enlightening and delightful.

As a quick answer (based mostly on what I remember from Pierce :-), here's my take on these terms.

parametric polymorphism refers to types with free variables in them, where the variables can be replaced by any type. The function List.length has such a type, as it can find the length of any list (no matter what the type of the elements).

# List.length;;
- : 'a list -> int = <fun>

One of the fantastic things about OCaml is that it not only supports types like this, it infers them. Given a function definition, OCaml infers the most general parametrically polymorphic type for the function.

Subtyping is a relation between types. A type T is a subtype of the type U if all instances of T are also instances of U (but not necessarily vice versa). OCaml supports subtyping, that is, it allows a program to treat a value of type T as a value of its supertype U. However, the programmer has to ask for this explicitly.

# type ab = [ `A | `B ];;
type ab = [ `A | `B ]
# type abc = [`A | `B | `C ];;
type abc = [ `A | `B | `C ]
# let x : ab = `A;;
val x : ab = `A
# let y : abc = x;;
Error: This expression has type ab but an expression was expected
of type abc. The first variant type does not allow tag(s) `C
# let y : abc = (x :> abc);;
val y : abc = `A

In this example, type type ab is a subtype of type abc, and x has type ab. You can use x as a value with type abc, but you must explicitly convert using the :> type operator.

Ad-hoc polymorphism refers to polymorphism that is defined by the programmer for particular cases, rather than being derived from fundamental principles. (Or at least that's what I mean by it, maybe other people use the term differently.) A possible example of this is an OO inheritance hierarchy, where the actual types of the object state need not be related in any way as long as the methods have the proper relations.

The key observation about ad-hoc polymorphism (IMHO) is that it's up to the programmer to make it work. Hence, it doesn't always work. The other types of polymorphism here, being based on fundamental principles, actually can't fail to work. That's a comforting feeling when working with complex systems.

Answer 2

Here's an approximation.

Ad-hoc polymorphism usually refers to being able to declare the same name (usually a function) with different types, e.g. + : int -> int -> int and + : float -> float -> float in SML. These are different functions, and they can act in totally different ways, but the compiler or interpreter chooses the appropriate one depending on the context. I can't think of any instances of ad-hoc polymorphism in OCaml. It is common in C++ and Java, however.

Parametric polymorphism is when a single function can work with an argument of any type due to not trying to look into that argument's structure. For example, cons : 'a -> 'a list -> 'a list is able to prepend a value v of any type to a list of values of the same type, because it does not matter to cons what the structure (layout) of v is, or what operations it supports. In C terms, cons does not need to "dereference" the pointer, or perform any operation on v that is specific to the actual type of v. Note that unlike in ad-hoc polymorphism, cons has to act the same way for all types. Parametric and ad-hoc polymorphism are thus in a way natural "opposites" of each other. Parametric polymorphism is responsible for the great majority of instances of polymorphism in OCaml.

Subtype polymorphism is when you can use values of type t where values of type u are expected. This could be because type t supports all the operations of type u, or because t's structure can be used where u is expected. Examples of this would be subclassing (perhaps a Bus can be used wherever a Vehicle can), or polymorphic variants (you can use 'A | 'B where 'A | 'B | 'C is expected).

EDIT per comment

Note, however, that subtyping has to be requested explicitly in OCaml. If you have, for example, a function f : u -> int, and you want to apply it to v : t where t is a subtype of u, you have to write f (v :> u). The (v :> u) syntax is a type coercion.

OCaml also supports row polymorphism, which is a form of parametric polymorphism with constraints. If f is instead f : #u -> int (for object types) or f : [< u] -> int (for polymorphic variants), the #u/[< u] syntax represents a type variable, similar to 'a, but which can only be replaced with the respective "subtypes" of u (in the restricted sense that they can support more fields/less constructors, respectively). Then, you can do f v without the coercion. OCaml automatically infers types that use row polymorphism for many expressions involving polymorphic variants and objects, but you have to write the types explicitly if you are creating a signature.

There are more usages and considerations to row polymorphism. I've neglected the actual row variables and additional syntax, and only described something that looks like bounded quantification (as in Java generics). More detailed and accurate discussion of row polymorphism, its name, and/or its formalism, is perhaps best saved for separate questions.