What is the difference between type variables and locally abstract types?

Question

I am trying to understand the purpose of locally abstract types in OCaml. How are locally abstract types different from type variables? It appears that they have the same behavior:

(* Type variable *)
# let f (x : 'a) : 'a = x;;
val f : 'a -> 'a = <fun>

(* Locally abstract type *)
# let f (type a) (x : a) : a = x;;
val f : 'a -> 'a = <fun>

Tarragon

Does this answer your question? In OCaml, what is the difference between `'a.` and `type a.` and when to use each? – Dissimilitude

Answer 1

Unification types variables and locally abstract types have completely different behaviors.

In particular, it useful to keep in mind that unification type variables:

• can be unified, for instance

let f (x:'a) (y:'a) : 'a = ()

is valid and yields f: unit -> unit -> unit.

• are in scope for the whole toplevel definition.

  For instance, the variable 'a is the same across the whole scope of f (which thus has type unit -> unit)

let f x =
   let () = (():'a) in
   (x:'a)

Contrarily, locally abstract types are:

• locally abstract, thus they cannot be unified with any other types.

  For instance,

let f (type a) (x:a) (y:a) : a = ()

yields the expected

Error: This expression has type unit but an expression was expected of type a

• well-scoped, the local type cannot outlive its scope. Typically,

let f x =
   let y (type a): a = assert false
   (* let's pretend that we can define such `y` value *) in
   (x:a)

yields the expected out-of-scope error

Error: Unbound type constructor a

Due to those fundamental difference behaviors, locally abstract types have been extended to support more advanced features of the type systems. Indeed, locally abstract types:

• can be used to define local modules, because they are type constructors and not type variables

let f (type a) (cmp:a -> a -> int) (x:a list) =
  let module S = Set.Make(struct type t = a let compare = cmp end) in
  x |> S.of_list |> S.elements

• can be refined with a local type equation when pattern matching on GADTs, because they have a well-defined scope:

type _ t =
| Int: int t
| Float: float t
let zero (type a) (x:a t) = match x with
| Int -> 0 (* in this branch a = int *)
| Float -> 0. (* whereas a = float in this one*)

Botha

Another distinction that I think is important to understand: Unification variables can be introduced and used in any type expression, while locally abstract types need to first be defined in a function definition and can therefore only be used in the definition, including type expressions that occur in the definition. But locally abstract types cannot be used in the signature of the function itself, because it precedes the definition, one must there use unification variables in its place. – Dissimilitude

Answer 2

This page indicates at least one difference:

This construction is useful because the type constructors it introduces can be used in places where a type variable is not allowed. For instance, one can use it to define an exception in a local module within a polymorphic function.

let f (type t) () =
  let module M = struct exception E of t end in
  (fun x -> M.E x), (function M.E x -> Some x | _ -> None)

Here is another example:

let sort_uniq (type s) (cmp : s -> s -> int) =
  let module S = Set.Make(struct type t = s let compare = cmp end) in
  fun l ->
    S.elements (List.fold_right S.add l S.empty)

It is also extremely useful for first-class modules (see section 10.5) and generalized algebraic datatypes (GADTs: see section 10.10).

Carree