Advanced Type System Features

Only *syntactic values* (functions, constants, constructors) are generalized:

29.1 The value restriction & weak types

Only *syntactic values* (functions, constants, constructors) are generalized:

Relaxed value restriction: type variables that occur only in covariant positions are generalized anyway (let l = List.map Fun.id [] → 'a list).

Why: if ref [] were 'a list ref, you could store an int and read a string.

let id x = x                  (* 'a -> 'a  — polymorphic *)
let f = id id                 (* '_weak1 -> '_weak1  — application, not generalized *)
let f x = id id x             (* eta-expansion restores polymorphism: 'a -> 'a *)
let r = ref None              (* '_weak1 option ref — prevents unsoundness *)

29.2 Variance annotations

Required in signatures of abstract types for subtyping and relaxed value restriction:

! marks injectivity: type !'a t.

type +'a producer = unit -> 'a       (* covariant *)
type -'a consumer = 'a -> unit       (* contravariant *)
type 'a cell = { mutable v : 'a }    (* invariant *)

module type S = sig type +'a t val empty : 'a t end

29.3 Locally abstract types

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

29.4 Explicit polymorphism & polymorphic recursion

type 'a nested = Flat of 'a | Nested of 'a list nested

let rec depth : 'a. 'a nested -> int = function   (* 'a. = explicitly polymorphic *)
  | Flat _ -> 0
  | Nested n -> 1 + depth n                        (* called at 'a list *)

29.5 Polymorphic record fields (higher-rank)

type mapper = { f : 'a. 'a list -> 'a list }
let apply_both { f } = (f [1;2], f ["a"])
let _ = apply_both { f = List.rev }

29.6 Phantom types

Type parameters with no runtime presence, used to track states:

module File : sig
  type 'mode t
  type read and write
  val open_read : string -> read t
  val open_write : string -> write t
  val read_line : read t -> string
  val write_line : write t -> string -> unit
end = struct
  type 'mode t = string          (* just a name, for illustration *)
  type read and write
  let open_read p = p
  let open_write p = p
  let read_line _ = "data"
  let write_line _ _ = ()
end
(* File.write_line (File.open_read "x") "oops"  -> type error *)

(* Validation states *)
type unvalidated and validated
type 'a form = { email : string }
let validate (f : unvalidated form) : validated form option = ...
let submit (f : validated form) = ...

29.7 Constraints on type parameters

type 'a t = 'a constraint 'a = < name : string; .. >

29.8 Nominal vs structural typing

Records & variants: nominal (type name matters).

Objects & polymorphic variants: structural (shape matters).

Module types: structural.

29.9 Type-directed disambiguation & principal types

Warnings 40–42 relate to constructor/field disambiguation. -principal flag checks principality of inferred types.

29.10 Recursive types & -rectypes

By default OCaml rejects cyclic types ('a -> 'a unified with 'a) except via objects/polymorphic variants. -rectypes relaxes this (rarely needed).

29.11 Unboxed / immediate attributes

type t = { x : float } [@@unboxed]
type small = A | B | C [@@immediate]

29.12 The Type module (5.1+)

let int_id : int Type.Id.t = Type.Id.make ()
let str_id : string Type.Id.t = Type.Id.make ()

let cast_to_int (type a) (id : a Type.Id.t) (v : a) : int option =
  match Type.Id.provably_equal id int_id with
  | Some Type.Equal -> Some v        (* here the compiler knows a = int *)
  | None -> None

let _ = cast_to_int int_id 5         (* Some 5 *)
let _ = cast_to_int str_id "x"       (* None *)