Stream: Coq devs & plugin devs

Topic: Pattern-matching and mutable in OCaml


view this post on Zulip Hugo Herbelin (Sep 18 2024 at 09:41):

Maybe already known: an example by Gabriel of unsoundness of OCaml's pattern-matching with mutable fields and when clause (see this paper):

type u = {a: bool; mutable b: int option}
let f x =
match x with
| {a = false; b = _} -> 0
| {a = _; b = None} -> 1
| {a = _; b = _} when (x.b <- None; false) -> 2
| {a = true; b = Some y} -> y
let _ = f {a=true; b=Some 5} (* segfault *)

view this post on Zulip Michael Soegtrop (Sep 18 2024 at 10:08):

The paper says "Our example uses a when guard which is arguably a dubious feature of OCaml". IMHO "when" as such is fine and quite useful but having assignments to mutable record fields in a when clause is indeed a very dubious feature. I would rather vote on making this an error instead of adjusting the compiler to support it.

view this post on Zulip Gaëtan Gilbert (Sep 18 2024 at 10:10):

how would you make it an error without forbidding calling functions in the when clause? ie

let f x =
  let check () = x.b <- None; false in
  match x with
  ...
  | {a = _; b = _} when check () -> 2
  ...

view this post on Zulip Michael Soegtrop (Sep 18 2024 at 10:15):

Good point (which is btw. not mentioned in the discussion at the end of the paper).

view this post on Zulip Gaëtan Gilbert (Sep 18 2024 at 10:19):

they do have a when incr () example

view this post on Zulip Michael Soegtrop (Sep 18 2024 at 10:39):

Yes - I meant the discussion at the end where they are discussing the pros and cons of merging this ("Final words"). I would say the function call argument is a very strong argument since it means that there is no alternative (the only alternatives are to fix it or to detect it as error).


Last updated: Oct 13 2024 at 01:02 UTC