{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/8413","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/8413/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/8413/comments","events_url":"https://api.github.com/repos/coq/coq/issues/8413/events","html_url":"https://github.com/coq/coq/issues/8413","id":357270213,"node_id":"MDU6SXNzdWUzNTcyNzAyMTM=","number":8413,"title":"General discussions on the design of ssreflect","user":{"login":"herbelin","id":460771,"node_id":"MDQ6VXNlcjQ2MDc3MQ==","avatar_url":"https://avatars1.githubusercontent.com/u/460771?v=4","gravatar_id":"","url":"https://api.github.com/users/herbelin","html_url":"https://github.com/herbelin","followers_url":"https://api.github.com/users/herbelin/followers","following_url":"https://api.github.com/users/herbelin/following{/other_user}","gists_url":"https://api.github.com/users/herbelin/gists{/gist_id}","starred_url":"https://api.github.com/users/herbelin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/herbelin/subscriptions","organizations_url":"https://api.github.com/users/herbelin/orgs","repos_url":"https://api.github.com/users/herbelin/repos","events_url":"https://api.github.com/users/herbelin/events{/privacy}","received_events_url":"https://api.github.com/users/herbelin/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-09-05T14:58:00Z","updated_at":"2018-09-05T15:05:37Z","closed_at":null,"author_association":"MEMBER","body":"Bouncing on a [discussion](https://github.com/coq/coq/pull/8372) started about the `of` and `&` syntax for binders which the ssreflect plugin defines, I'm opening this issue for general discussions about the design of ssreflect, hoping that it shall eventually help to give us convergent objectives about the future of Coq in whatever domains to which the ssreflect developers are willing to contribute.\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/418765415","html_url":"https://github.com/coq/coq/issues/8413#issuecomment-418765415","issue_url":"https://api.github.com/repos/coq/coq/issues/8413","id":418765415,"node_id":"MDEyOklzc3VlQ29tbWVudDQxODc2NTQxNQ==","user":{"login":"herbelin","id":460771,"node_id":"MDQ6VXNlcjQ2MDc3MQ==","avatar_url":"https://avatars1.githubusercontent.com/u/460771?v=4","gravatar_id":"","url":"https://api.github.com/users/herbelin","html_url":"https://github.com/herbelin","followers_url":"https://api.github.com/users/herbelin/followers","following_url":"https://api.github.com/users/herbelin/following{/other_user}","gists_url":"https://api.github.com/users/herbelin/gists{/gist_id}","starred_url":"https://api.github.com/users/herbelin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/herbelin/subscriptions","organizations_url":"https://api.github.com/users/herbelin/orgs","repos_url":"https://api.github.com/users/herbelin/repos","events_url":"https://api.github.com/users/herbelin/events{/privacy}","received_events_url":"https://api.github.com/users/herbelin/received_events","type":"User","site_admin":false},"created_at":"2018-09-05T15:05:37Z","updated_at":"2018-09-05T15:05:37Z","author_association":"MEMBER","body":"I'm copying below the last comment I made in about the `of` and `&` [discussion](https://github.com/coq/coq/pull/8372), a comment about which a more general-purpose place for further discussions has been requested (for more context, see the rest of discussion at #8372).\r\n\r\n------\r\n\r\n> fun ... & phant_id u v => ... without a leading of for instance factories - there are over 30 instances in ssralg.v alone\r\n\r\nAh, I thought that the idiom was to use `&` only after a `of`, so I did not try to grep it. Thanks for telling.\r\n\r\nI'm not sure I'm convinced though. I was expecting a more universal approach and, @ggonthier, the more I read your argumentation, the more I feel it is just an idiom rather than a standard solution.\r\n\r\nI still like the idea to be able to write `Inductive list A := nil | cons of A & list A` and I'd be in favor of supporting it. I'm however less convinced by the other uses. I'm unsure that `foo of some type` or `foo & some type` are clearer than simply providing a dedicated general syntax for `(_ : T)` as most of us initially thought this PR was about. The symbol `&` suggests a conjunction, so, making `& T` an abbreviation for `_:T` would either need to rethink at it in another role than the role of conjunction, or to forbid it in first position, but that would then be quite artificial to allow a notation for `_:T` only from the second position. As far as `of` is concerned, let's try to make the mental effort that a notation `Definition foo n of typ :=` denotes an object taking an `n` and some (object of type) `typ`. OK, why not. But this would be restricted to `_:T` in last positions because (even by changing the precedences), this would start to be strange to write `Definition foo n of t p of t q := ...` (or at least, we would start to diverge quite a lot from the original motivation of specifically using `of` and `&` over other symbols because of the analogy with OCaml syntax of inductive types). So, if the purpose is before all to abbreviate `_:T`, and not to echo to the syntax of OCaml inductive types, I don't see why `of` and `&` would be better than any other symbols. In particular, a neutral symbol, which does not prejudge of the existence or not of other binders before or after, would look better to me. Actually, I just checked and, unless I mixed up my tests, I didn't see the `` ` `` turning the corresponding argument into an implicit argument, even when a class, so it basically does the same as `of`, up to the question of parentheses (do we agree on this observation?).\r\n\r\nAbout parentheses, saying that parentheses would be spurious if writing `of (P x)` rather than `of P x` seems a bit excessive to me. Parentheses are anywhere needed somewhere to represent tree-like data. So, the spurious is obviously here a spurious according to your own aesthetics, which, as you said, prefers to sacrifice a binder coming after a `of`/`&` rather than seeing parentheses (or some other form of delimiters). Note that I'm perfectly ok with the fact that we all have our own criteria for aesthetism. If I'm making this remark it is only to clarify that the word spurious is somehow an appropriate word in the discussion in that it conveys a moral meaning while it is only about personal tastes.\r\n\r\nSo, if we summarize, there is already a notation for `_:T` in vanilla coq, and, indeed ``Inductive nat := O | S `(nat).`` works perfectly (even if I did not realize it until today!!). This notation is versatile, it is a bit an arbitrary symbol but it has no connotation such as `&` which comes with the connotation of connecting two things.\r\n\r\nIncidentally, there is no reason to expect parentheses in `` `(nat)``, and this constraint could be dropped. Of course, keeping parentheses around an application remains needed if one accepts to prefer versatility.\r\n\r\nNow, more generally, what to do with the cool ideas of ssreflect, what to do with the redundancies between cool ideas of ssreflect and features from coq? By initiating this discussion, I had hopes that a discussion with ssreflect developers could converge towards the general interest of the diversity of all users. Maybe I'm wrong, but I feel that your position, @ggonthier, is more to preserve ssreflect as it is, as a plugin with its idioms and redundancies than at working altogether at providing a language which rubs out the existing idiosynchracies and targets all users, all styles, all habits. Am I correct?\r\nBut are you sure that this is the best we can do? Don't underestimate the impact of your attitude on other ssreflect developers. If yourself shows turned towards the future, towards wishing a synthesis of the best of what ssreflect provides and of what coq provides, rather than preserving idiosynchracies a priori, I would not be surprised to see other ssreflect developers welcoming the change, with maybe other potential positive impacts in sight...\r\n"}}
{"actor":{"display_login":"herbelin"}}