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鈥檒l occasionally send you account related emails.

Already on GitHub? Sign in to your account

Integer negate and clamp #780

Merged
merged 5 commits into from Oct 29, 2019

Conversation

@SiriusStarr
Copy link
Contributor

SiriusStarr commented Oct 19, 2019

PR for proposed addition of Integer/negate and Integer/clampToNatural builtins per discussion on Discourse.

Someone smarter than I needs to confirm the beta-normalization for Integer/negate is correct, please. 馃槅

Additionally, it should be noted that, as Integer/clampToNatural is longer than other builtin names, it overflows the lined-up equals signs in the ABNF (line 406 in the diff of standard/dhall.abnf). I did not reformat the extant entries to match this longer name so as to avoid introducing a much larger whitespace diff, but I can obviously do so if that's desired.

SiriusStarr added 2 commits Oct 19, 2019
@Gabriel439

This comment has been minimized.

Copy link
Contributor

Gabriel439 commented Oct 19, 2019

@SiriusStarr: Maybe shorten Integer/clampToNatural to Integer/clamp since I can't think of any other type we would be clamping Integer to. That would also side-step the alignment problem 馃檪

@sjakobi

This comment has been minimized.

Copy link
Collaborator

sjakobi commented Oct 19, 2019

Maybe shorten Integer/clampToNatural to Integer/clamp since I can't think of any other type we would be clamping Integer to.

Integer/clamp could have type Integer -> Integer

But if everyone's in favor of the shorter name, I wouldn't mind it.

Copy link
Collaborator

sjakobi left a comment

Looks great!

Can you add parser tests for both builtins? Not sure whether we also need binary-decode tests.

Once this is accepted, please also add Integer.negate and Integer.clampToNatural to the Prelude.

@SiriusStarr

This comment has been minimized.

Copy link
Contributor Author

SiriusStarr commented Oct 19, 2019

Updating to Integer/clamp (and caught a typo in the beta normalization), gimme a few minutes.

Beta-normalization had Integer/negate where Integer/clamp was intended.
@SiriusStarr

This comment has been minimized.

Copy link
Contributor Author

SiriusStarr commented Oct 19, 2019

@sjakobi RE parser tests, it doesn't look like other builtins have them (not seeing one for Natural/subtract, for example)? Could you point me to an example?

@SiriusStarr

This comment has been minimized.

Copy link
Contributor Author

SiriusStarr commented Oct 19, 2019

RE the prelude, shall I add some or all of the utilities discussed on Discourse as well, (e.g. nonPositive, positive, nonNegative, negative, toNatural (the Optional version), and abs)?

@sjakobi

This comment has been minimized.

Copy link
Collaborator

sjakobi commented Oct 19, 2019

RE parser tests, it doesn't look like other builtins have them (not seeing one for Natural/subtract, for example)? Could you point me to an example?

Oh, never mind then.

RE the prelude, shall I add some or all of the utilities discussed on Discourse as well

That would be great! But maybe wait a bit in case there are some fundamental disagreements over the proposal.

@SiriusStarr

This comment has been minimized.

Copy link
Contributor Author

SiriusStarr commented Oct 19, 2019

Okay, this should be ready for review/comments/whatnot. I will add the builtins to the prelude if/when it's accepted.

Copy link
Contributor

Gabriel439 left a comment

Looks great!

@Gabriel439

This comment has been minimized.

Copy link
Contributor

Gabriel439 commented Oct 20, 2019

@SiriusStarr: At this point, we're just waiting either for 7 days to pass or 3 days plus all three approvals, whichever comes first. For more details, see: https://github.com/dhall-lang/dhall-lang/blob/master/.github/CONTRIBUTING.md#how-do-changes-get-approved

@SiriusStarr

This comment has been minimized.

Copy link
Contributor Author

SiriusStarr commented Oct 20, 2019

Yep, I read as much, but thanks for the update.

@f-f
f-f approved these changes Oct 22, 2019
@singpolyma

This comment has been minimized.

Copy link
Collaborator

singpolyma commented Oct 26, 2019

I'm curious if Integer/build : Natural -> <Positive | Negative> -> Integer would be more like what we want (especially in light of the desire for clamp or for an Integer destructing here).

@SiriusStarr

This comment has been minimized.

Copy link
Contributor Author

SiriusStarr commented Oct 26, 2019

@singpolyma You mean instead of Integer/negate?

@singpolyma

This comment has been minimized.

Copy link
Collaborator

singpolyma commented Oct 26, 2019

@sjakobi

This comment has been minimized.

Copy link
Collaborator

sjakobi commented Oct 26, 2019

Integer/build : Natural -> <Positive | Negative> -> Integer

If we'd add this instead of Integer/negate, we couldn't recover the absolute value of a negative Integer.

It might be a good addition to the Prelude though!

@Gabriel439

This comment has been minimized.

Copy link
Contributor

Gabriel439 commented Oct 26, 2019

Note that we can create an Integer/build in the Prelude from Integer/negate + Natural/toInteger

@singpolyma

This comment has been minimized.

Copy link
Collaborator

singpolyma commented Oct 26, 2019

If we'd add this instead of Integer/negate, we couldn't recover the absolute value of a negative Integer.

Would not:

Integer/build (Integer/clamp (-1)) (<Negative|Positive>.Positive)

Get the absolute value of a negative Integer?

I realize that build can be make out of other parts, but the reason I propose build is that it is in line with other things already in the language and acts as the natural introducer for an Integer -- whereas negate acts more like an operation on an Integer (of which we currently do not have any).

@singpolyma

This comment has been minimized.

Copy link
Collaborator

singpolyma commented Oct 26, 2019

Oh, I see, I misread. clamp is going to turn negative numbers to zero? That seems very odd...

@singpolyma

This comment has been minimized.

Copy link
Collaborator

singpolyma commented Oct 26, 2019

Alright, sorry all for my being slow. I've re-read the discourse thread and got the context more properly in my mind. I still don't love having a negate operation but the best I can come up with to cover all three things without this is indeed three builtins instead, which runs rather counter to my anti-built-in nature as well:

Integer/build : Natural -> <Negative|Positive> -> Integer
Integer/abs : Integer -> Natural
Integer/sign : Integer -> <Negative|Positive>
@singpolyma singpolyma closed this Oct 26, 2019
@singpolyma singpolyma reopened this Oct 26, 2019
@sjakobi

This comment has been minimized.

Copy link
Collaborator

sjakobi commented Oct 26, 2019

I still don't love having a negate operation

What's the problem with it?

@singpolyma

This comment has been minimized.

Copy link
Collaborator

singpolyma commented Oct 26, 2019

@sjakobi As I said, negate would introduce an operation on Integer, which we currently have none of, and then it would be the only one. It feels quite odd to have Integer be "opaque except you can negate it"

@sjakobi

This comment has been minimized.

Copy link
Collaborator

sjakobi commented Oct 26, 2019

It feels quite odd to have Integer be "opaque except you can negate it"

With Integer/negate, Integer/clamp and Natural/toInteger, Integer just really isn't opaque anymore.

I think an alternative could be to change most of the Natural operations to work on Integer, which would allow more efficient computations on Integer, but I currently don't think it's worth the trouble.

@philandstuff

This comment has been minimized.

Copy link
Collaborator

philandstuff commented Oct 26, 2019

@singpolyma recognising the danger of topic drift here, I don't think your proposed Integer/build fits the language pattern for build functions. I expect a build function to:

  • take one function as a parameter (and possibly some types before hand)
  • call the function, passing it constructors of the data type

So I would expect Integer/build to have type

鈭 ( f : 鈭(integer : Type)
      鈫 鈭(nonNegative : Natural 鈫 integer)
      鈫 鈭(negative : Natural 鈫 integer)
      鈫 integer
      )
  鈫 Integer

where we have modelled an Integer as < NonNegative Natural | Negative Natural >. I would also expect there to be a corresponding fold function as the canonical destructor for Integers.

I don't actually think this would be a valuable addition to the language; my main argument is that if we add your proposed function, we don't call it Integer/build because it violates my expectations about what Integer/build would be if it existed.

@SiriusStarr

This comment has been minimized.

Copy link
Contributor Author

SiriusStarr commented Oct 26, 2019

Agreed, elsewhere in Dhall, build is always the inverse of fold, so it would be weird for it to not be that way for integers.

@Gabriel439

This comment has been minimized.

Copy link
Contributor

Gabriel439 commented Oct 29, 2019

@SiriusStarr: This should be good to merge now. I can take care of the corresponding changes in the Haskell implementation

@SiriusStarr

This comment has been minimized.

Copy link
Contributor Author

SiriusStarr commented Oct 29, 2019

@Gabriel439 Shall I open a second PR for the prelude additions? They're ready to go but unsure how to finalize them until dhall-haskell is updated with the new builtins, since I can't generate the hashes for the imports.

@Gabriel439

This comment has been minimized.

Copy link
Contributor

Gabriel439 commented Oct 29, 2019

@SiriusStarr: Yeah, I think it's fine if the Prelude additions go in a second pull request

Gabriel439 added a commit to dhall-lang/dhall-haskell that referenced this pull request Oct 29, 2019
... as standardized in dhall-lang/dhall-lang#780
@Gabriel439

This comment has been minimized.

Copy link
Contributor

Gabriel439 commented Oct 29, 2019

@SiriusStarr: Also, here is the matching change to the Haskell implementation:

dhall-lang/dhall-haskell#1486

mergify bot added a commit to dhall-lang/dhall-haskell that referenced this pull request Oct 29, 2019
... as standardized in dhall-lang/dhall-lang#780
@sjakobi

This comment has been minimized.

Copy link
Collaborator

sjakobi commented Oct 29, 2019

@SiriusStarr Is this ready to be merged from your side?

@SiriusStarr

This comment has been minimized.

Copy link
Contributor Author

SiriusStarr commented Oct 29, 2019

@sjakobi Should be good to go, since there have been no further comments/suggestions. Prelude additions are up separately as #797

@sjakobi sjakobi merged commit ee12030 into dhall-lang:master Oct 29, 2019
1 check passed
1 check passed
hydra Hydra build #42180 of dhall-lang:780:dhall-lang
Details
@SiriusStarr SiriusStarr deleted the SiriusStarr:integer_negate_and_clamp branch Oct 29, 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鈥檛 perform that action at this time.