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

Slovakia

Answer 1

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.

Thirtyeight

Polymorphic variants (and objects) in OCaml are not subtyping but row-polymorphism, which is based on parametric polymorphism. Subtyping comes up only when you add type casts (which are explicit in OCaml). The rest is absolutely correct. Also, a good example of adhoc polymorphism is type class in Haskell (and modular implicits ...). – Lyte

That is mostly right – but that you have to explicitly write coercions for subtyping to be applied is a detail of OCaml specifically. I didn't want to complicate a conceptual answer. It is true that polymorphic sums and objects are kinds of types that support subtype relations. That there is also row-polymorphism involved with these types, and that it covers some use-cases of subtyping without needing explicit coercions in OCaml, is another matter. And, row polymorphism is certainly not what polymorphic variants and objects "are" – just one thing they support. I'll work in a note. – Thirtyeight

Answer 2

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.

Corticate

Surely you mean ad-hoc polymorphism, not ad-hoc subtyping? – Thirtyeight

But ad-hoc polymorphism is not this. What you are describing in the example is an object system in which the layout of the object does not participate in evaluating the subtype relation (i.e. whether one type is a subtype of another). Ad-hoc polymorphism is not a form of subtyping. – Thirtyeight

I consider OO inheritance to be a type of ad-hoc polymorphism. It's also based on subtyping, yes. I don't consider overloading of functions to be ad-hoc polymorphism, but maybe I should. As you say, OCaml doesn't allow overloading (but you get type inference as a compensation). – Corticate

Ad-hoc polymorphism and parametric polymorphism are both derived from the natural question of whether a function, if it is to be polymorphic, can depend on its argument's actual type or perform an operation based on the type. If the answer is no, the result is parametric polymorphism. If the answer is yes, the result is ad-hoc polymorphism. Cases are a necessary consequence – ad-hoc polymorphism is the choice to have cases on type. The two options are equally derived from fundamental principles and directly related to each other. The final paragraphs of this answer are misleading. – Thirtyeight

Answer 3

ident is polymorphous :

# let ident x = x;;
val ident : 'a -> 'a = <fun>

# ident 1;;
- : int = 1
# ident "ok";;
- : string = "ok"
# ident [];;
- : 'a list = []
# ident List.length;;
- : '_a list -> int = <fun>
# ident ident;;
- : '_a -> '_a = <fun>

fold also :

# open List;;
# fold_left (+) 0 [1;2;3];;
- : int = 6
# fold_left (^) "" ["1";"2";"3"];;
- : string = "123"
# fold_left (fun a (x,y)  -> a+x*y) 0 [(1,2);(3,4);(5,6)];;
- : int = 44

Settlings