Ali Caglayan (Aug 13 2021 at 12:02): Ali Caglayan (Aug 13 2021 at 12:02):How difficult would it be to drop the need for an end in a match block in coq? I'm wondering since ocaml is able to do so.
Pierre-Marie Pédrot (Aug 13 2021 at 12:03):That would be a very bad idea, I believe.
Pierre-Marie Pédrot (Aug 13 2021 at 12:04):The lack of a delimiter for match blocks is a major pain point of OCaml
Pierre-Marie Pédrot (Aug 13 2021 at 12:04):it's not robust to pattern extension and it's very annoying for nested matches
Pierre-Marie Pédrot (Aug 13 2021 at 12:05):plus a few more issues with precedence
Pierre-Marie Pédrot (Aug 13 2021 at 12:06):I've already heard major OCaml developers openly complaining about the OCaml syntax which is notoriously broken, even outside of the core dev circle
Ali Caglayan (Aug 13 2021 at 12:07):Do you remember around when ocaml accepted these kinds of match statements? I'm interested in seeing why they did it.
Pierre-Marie Pédrot (Aug 13 2021 at 12:07):it's very old
Pierre-Marie Pédrot (Aug 13 2021 at 12:07):since the inception of the language essentially
Pierre-Marie Pédrot (Aug 13 2021 at 12:08):caml light already had this syntax IIRC
Pierre-Marie Pédrot (Aug 13 2021 at 12:08):the grandiose time when internet was not even widely available
Ali Caglayan (Aug 13 2021 at 12:08):OK, so it's unlikely that I am going to find a well thought out argument for them
Pierre-Marie Pédrot (Aug 13 2021 at 12:08):nope
Ali Caglayan (Aug 13 2021 at 12:09):On a side note, what is our preference on using them in coq ml?
Pierre-Marie Pédrot (Aug 13 2021 at 12:09):wdym?
Ali Caglayan (Aug 13 2021 at 12:10):Is it good style to not close matches? I see closed and unclosed ones all them time when reading code, so I am wondering what the preference is
Pierre-Marie Pédrot (Aug 13 2021 at 12:10):I think that we only close them when necessary
Pierre-Marie Pédrot (Aug 13 2021 at 12:11):otherwise it's very verbose since you also have to add a begin
Ali Caglayan (Aug 13 2021 at 12:11):Oh, I didn't know that the begin was necessary
Pierre-Marie Pédrot (Aug 13 2021 at 12:12):you're talking about OCaml, right?
Ali Caglayan (Aug 13 2021 at 12:12):Yes
Pierre-Marie Pédrot (Aug 13 2021 at 12:13):so yes in OCaml there is no end block for a match, this needs to be enclosed in a begin-end
Ali Caglayan (Aug 13 2021 at 12:13):right
Ali Caglayan (Aug 13 2021 at 12:13):Thanks for the info, I will continue on not to think about it too much :-)
Pierre-Marie Pédrot (Aug 13 2021 at 12:13):or parentheses but I personally find this to be unreadable
Pierre-Marie Pédrot (Aug 13 2021 at 12:14):(full disclaimer: I believe that LISP is a shibboleth language designed to tell apart humans from stack automata)
Enrico Tassi (Aug 13 2021 at 17:34):Unless we also start to make indentation matter, a terminator for match is very handy. I could live with an exception if it is the outermost one, eg Definition f x := match x with ... . in some sense the . would also close the match.
Note that if you load ssreflect you get to write if n is S p then f p else q which is a binary match with no terminator.
Last updated: Jun 09 2023 at 08:01 UTC