counterexamples icon indicating copy to clipboard operation
counterexamples copied to clipboard

Three more examples of monotonicity failures in OCaml

Open yallop opened this issue 3 years ago • 0 comments

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.

yallop avatar Jul 15 '21 15:07 yallop