stedolan / counterexamples

Counterexamples in Type Systems
http://counterexamples.org
372 stars 23 forks source link

Three more examples of monotonicity failures in OCaml #12

Open yallop opened 3 years ago

yallop commented 3 years ago

This PR adds three more examples of monotonicity failures in OCaml, relating to

  1. the relaxed value restriction and strict positivity
  2. compatibility
  3. labeled arguments

Another possible addition involves constructor disambiguation:

type t = A | B

module M :
sig
  type t (* = A *)
end =
struct
  type t = A
end

let f = M.[A;B]

but I think that one's less convincing, because it's more about namespacing than type systems as such.