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

user_5916915 0
Viewed 76

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>
ocaml types
2 Answers

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*)
user_73693660

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).

user_152613150
Related