Stream: Coq devs & plugin devs

Topic: Dropping end from match in coq


view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Aug 13 2021 at 12:03):

That would be a very bad idea, I believe.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Aug 13 2021 at 12:05):

plus a few more issues with precedence

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Aug 13 2021 at 12:07):

it's very old

view this post on Zulip Pierre-Marie Pédrot (Aug 13 2021 at 12:07):

since the inception of the language essentially

view this post on Zulip Pierre-Marie Pédrot (Aug 13 2021 at 12:08):

caml light already had this syntax IIRC

view this post on Zulip Pierre-Marie Pédrot (Aug 13 2021 at 12:08):

the grandiose time when internet was not even widely available

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Aug 13 2021 at 12:08):

nope

view this post on Zulip Ali Caglayan (Aug 13 2021 at 12:09):

On a side note, what is our preference on using them in coq ml?

view this post on Zulip Pierre-Marie Pédrot (Aug 13 2021 at 12:09):

wdym?

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Aug 13 2021 at 12:10):

I think that we only close them when necessary

view this post on Zulip Pierre-Marie Pédrot (Aug 13 2021 at 12:11):

otherwise it's very verbose since you also have to add a begin

view this post on Zulip Ali Caglayan (Aug 13 2021 at 12:11):

Oh, I didn't know that the begin was necessary

view this post on Zulip Pierre-Marie Pédrot (Aug 13 2021 at 12:12):

you're talking about OCaml, right?

view this post on Zulip Ali Caglayan (Aug 13 2021 at 12:12):

Yes

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Aug 13 2021 at 12:13):

right

view this post on Zulip Ali Caglayan (Aug 13 2021 at 12:13):

Thanks for the info, I will continue on not to think about it too much :-)

view this post on Zulip Pierre-Marie Pédrot (Aug 13 2021 at 12:13):

or parentheses but I personally find this to be unreadable

view this post on Zulip 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)

view this post on Zulip 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: Oct 16 2021 at 03:02 UTC