Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Replace "not is_nonexpansive" by "maybe_expansive" #8598

Merged
merged 7 commits into from Apr 9, 2019

Conversation

@trefis
Copy link
Contributor

commented Apr 8, 2019

I find double negations harder to read.

Also, I took the opportunity to make the function non-fragile, as this has proved to be a source of bugs in the past (see #2166 and #2167 for instance).
In the process, I noticed that Texp_unreachable was deemed expansive, which seems wrong to me, so I changed that.

@trefis trefis added the typing label Apr 8, 2019
typing/typecore.ml Outdated Show resolved Hide resolved
@trefis trefis force-pushed the trefis:is_expansive branch from d430e24 to 687722f Apr 8, 2019
typing/typecore.ml Outdated Show resolved Hide resolved
@trefis trefis force-pushed the trefis:is_expansive branch from 687722f to 60d727e Apr 8, 2019
@xavierleroy

This comment has been minimized.

Copy link
Contributor

commented Apr 9, 2019

I'm not happy with this proposal.

First, the literature on the topic uses "nonexpansive" as the generalization criterion, not "not expansive". I'm afraid you're making it harder to relate the code with the papers, something that is already famously difficult.

Second, nonexpansiveness/expansiveness is undecidable because it's a semantic notion, so what we're using are syntactic approximations. I expect a function called is_nonexpansive to return true if its argument is DEFINITELY not expansive, and a function called is_expansive to return true if its argument is DEFINITELY expansive. Your is_expansive function doesn't fit this reading.

Third, I'm a bit tired of pull requests of the form "this code works fine but is not to my personal tastes, let's change it at the risk of introducing bugs and consuming much reviewing time".

@gasche

This comment has been minimized.

Copy link
Member

commented Apr 9, 2019

I agree with @xavierleroy's remark on the naming: is_expansive e is not the right name for not (is_nonexpansive e). On the other hand, I believe that the change of @trefis comes from the multiple occurrences of not (is_nonexpansive e) in the type-checker implementation; I find them a bit surprising, given that I would expect (from the papers indeed) to find logic such as "if it is non-expansive then do this refined thing", but this suggests that "not being definitely nonexpansive" is an important concept in the type-checker implementation, so it may deserve a clearer name than not (is_nonexpansive e).

Maybe a reasonable middle-ground would be to have an alias

let may_be_expansive e = not (is_nonexpansive e)

to use at the call sites, without changing the definition of is_nonexpansive.

@trefis

This comment has been minimized.

Copy link
Contributor Author

commented Apr 9, 2019

Ack.
I’ll switch to @gasche's version then; and keep the change making the function non-fragile.

@gasche

This comment has been minimized.

Copy link
Member

commented Apr 9, 2019

Yes, the non-fragility is an improvement for forward maintenance.

@dra27

This comment has been minimized.

Copy link
Contributor

commented Apr 9, 2019

On the basis that @trefis hasn't pushed yet, can I point out the difference between maybe (expressing doubt - "Maybe this is non-expansive?") and may_be (expressing permission - "This may be non-expansive"). FWIW, I think you want maybe_expansive as the dual of is_nonexpansive. And I need to stop distracting myself from what I should be doing...

@trefis trefis force-pushed the trefis:is_expansive branch from 60d727e to 4218eeb Apr 9, 2019
@trefis

This comment has been minimized.

Copy link
Contributor Author

commented Apr 9, 2019

I just pushed a version with the maybe_expansive wrapper.
I kept the non-fragile change, as well as the decision to make Texp_unreachable nonexpansive.

@dra27

This comment has been minimized.

Copy link
Contributor

commented Apr 9, 2019

LGTM - assuming the change for Texp_unreachable is correct.

@xavierleroy

This comment has been minimized.

Copy link
Contributor

commented Apr 9, 2019

The function names are fine. Thank you!

@gasche
gasche approved these changes Apr 9, 2019
@trefis trefis changed the title Replace "not is_nonexpansive" by "is_expansive" Replace "not is_nonexpansive" by "maybe_expansive" Apr 9, 2019
@trefis trefis merged commit 183c4ae into ocaml:trunk Apr 9, 2019
0 of 2 checks passed
0 of 2 checks passed
continuous-integration/appveyor/pr Waiting for AppVeyor build to complete
Details
continuous-integration/travis-ci/pr The Travis CI build is in progress
Details
@trefis trefis deleted the trefis:is_expansive branch Apr 9, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
6 participants
You can’t perform that action at this time.