{"action":"created","issue":{"url":"https://api.github.com/repos/rust-lang/rust/issues/50230","repository_url":"https://api.github.com/repos/rust-lang/rust","labels_url":"https://api.github.com/repos/rust-lang/rust/issues/50230/labels{/name}","comments_url":"https://api.github.com/repos/rust-lang/rust/issues/50230/comments","events_url":"https://api.github.com/repos/rust-lang/rust/issues/50230/events","html_url":"https://github.com/rust-lang/rust/issues/50230","id":317739740,"number":50230,"title":"Should PartialOrd require irreflexivity over <?","user":{"login":"gnzlbg","id":904614,"avatar_url":"https://avatars0.githubusercontent.com/u/904614?v=4","gravatar_id":"","url":"https://api.github.com/users/gnzlbg","html_url":"https://github.com/gnzlbg","followers_url":"https://api.github.com/users/gnzlbg/followers","following_url":"https://api.github.com/users/gnzlbg/following{/other_user}","gists_url":"https://api.github.com/users/gnzlbg/gists{/gist_id}","starred_url":"https://api.github.com/users/gnzlbg/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gnzlbg/subscriptions","organizations_url":"https://api.github.com/users/gnzlbg/orgs","repos_url":"https://api.github.com/users/gnzlbg/repos","events_url":"https://api.github.com/users/gnzlbg/events{/privacy}","received_events_url":"https://api.github.com/users/gnzlbg/received_events","type":"User","site_admin":false},"labels":[{"id":234902,"url":"https://api.github.com/repos/rust-lang/rust/labels/C-enhancement","name":"C-enhancement","color":"f5f1fd","default":false},{"id":431251592,"url":"https://api.github.com/repos/rust-lang/rust/labels/T-doc","name":"T-doc","color":"bfd4f2","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2018-04-25T18:18:10Z","updated_at":"2018-04-25T19:28:12Z","closed_at":null,"author_association":"CONTRIBUTOR","body":"Why doesn't `PartialOrd` require irreflexivity `!(a < a)` over `<` ? AFAICT `PartialOrd` does not actually express any kind of ordering relation for `<`. For: \r\n\r\n* a strict partial order on `<`: we need `PartialOrd` + `Irreflexivity`\r\n* non-strict partial order on `<=`: we need `PartialOrd` + `Eq` since `==` must be reflexive.\r\n* total order: we need`PartialOrd + Eq + Total`\r\n\r\nIs this an oversight? If not, we should document that `PartialOrd` requires:\r\n\r\n* irreflexivity: `!(a < a)`\r\n\r\nas well. That would make `PartialOrd`'s `<` denote a strict partial order on `<`. \r\n\r\nAFAICT this is actually what was intended, since all the discussions I can find online about `PartialOrd` talk about floats, and floats are strictly partially ordered under `<`, but not non-strictly partially ordered under `<=`, which would fit our current model that floats don't implement `Eq`.\r\n\r\n---\r\n\r\nAlso, the docs of `PartialOrd` do not say what `le` (`<=`) and `ge` (`>=`) actually mean. AFAICT they mean nothing for `PartialOrd` in isolation. From reading the source the default implementation is `a < b || a == b`, which would denote a non-strict total ordering over `<=` when `Eq` is implemented. But since `Eq` is not required for `PartialOrd`, I'd guess that those overriding these implementations are allowed to do something else as long as they don't implement `Eq`. It is unclear to me what that \"something else\" might mean, but the docs should probably say something about this.\r\n\r\n---\r\n\r\nAlso, I haven't been able to find any document explaining why things are the way they are, but the fact that `PartialOrd` requires `PartialEq` makes no sense to me, and it doesn't make much sense either that `PartialOrd` exposes `le` (`<=`) and `ge` (`>=`) methods, since as mentioned above, without `Eq`, `le` and `ge` do not express any meaningful ordering relation. It seems that these traits, like all other \"operators\" traits, mix operator overloading with mathematical semantics: in some cases they are used to express mathematical concepts, like a strict partial ordering relation under `<`, and in some other cases they are used \"to provide <= for floats\". If anybody has any links to any discussions / documentation about why things are the way they are I'd like to read them, and maybe we should add rationale sections to the docs."},"comment":{"url":"https://api.github.com/repos/rust-lang/rust/issues/comments/384406114","html_url":"https://github.com/rust-lang/rust/issues/50230#issuecomment-384406114","issue_url":"https://api.github.com/repos/rust-lang/rust/issues/50230","id":384406114,"user":{"login":"RalfJung","id":330628,"avatar_url":"https://avatars1.githubusercontent.com/u/330628?v=4","gravatar_id":"","url":"https://api.github.com/users/RalfJung","html_url":"https://github.com/RalfJung","followers_url":"https://api.github.com/users/RalfJung/followers","following_url":"https://api.github.com/users/RalfJung/following{/other_user}","gists_url":"https://api.github.com/users/RalfJung/gists{/gist_id}","starred_url":"https://api.github.com/users/RalfJung/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/RalfJung/subscriptions","organizations_url":"https://api.github.com/users/RalfJung/orgs","repos_url":"https://api.github.com/users/RalfJung/repos","events_url":"https://api.github.com/users/RalfJung/events{/privacy}","received_events_url":"https://api.github.com/users/RalfJung/received_events","type":"User","site_admin":false},"created_at":"2018-04-25T19:28:12Z","updated_at":"2018-04-25T19:28:12Z","author_association":"CONTRIBUTOR","body":"> @ExpHP mentioned that PartialOrd probably also requires: (a < b) if and only if (b > a) (they called it \"the 'notational' axiom\").\r\n\r\nYeah that sounds pretty reasonable. I'd express this as \"> is the dual to <\", I think that's the common terminology in maths.\r\n\r\nI briefly wondered how this relates to antisymmetry... but antisymmetry is a strange axiom in this context. In fact, antisymmetry is impossible to violate! If `a < b`, then `partial_cmp(a, b) == Some(Less)`, so we already have `!(a > b)`. So, I think we can just drop it. If we require that `lt` and `gt` are defined in terms of `partial_cmp` (or equivalent), antisymmetry will always hold."}}
{"actor":{"display_login":"RalfJung"}}