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

Add Integer/toSigned #675

Closed
wants to merge 1 commit into from

Conversation

@ocharles
Copy link
Member

ocharles commented Jul 29, 2019

This new builtin splits an Integer apart into a Natural, and an encoding
of its sign.

There are a few points of motivation:

  1. We have Integer/show, but this could be decomposed into
    Integer/toSigned and Natural/show.

  2. We can represent exact rational numbers via the type
    { numerator : Natural, denominator : Natural }. However, constructing
    values of this type is difficult. One familiar way to construct such
    a value would be to use scientific notation. For example, 0.15625
    could be written as e 15625 -5.

  3. #508 wants a way to
    show Integers signed, but only showing the sign when it's
    negative (that is, no leading +). This cannot be done with Integers
    currently, forcing this work to invent its own signed integer type.

This does open the door to exposing the total ordering of Integers (as
we now expose enough to determine the total ordering of Naturals). It
also gives you some form of Integer arithmetic, but you can't
reconstruct an Integer from it's signed type.

This new builtin splits an Integer apart into a Natural, and an encoding
of its sign.

There are a few points of motivation:

1. We have Integer/show, but this could be decomposed into
   Integer/toSigned and Natural/show.

2. We can represent exact rational numbers via the type
   { numerator : Natural, denominator : Natural }. However, constructing
   values of this type is difficult. One familiar way to construct such
   a value would be to use scientific notation. For example, 0.15625
   could be written as `e 15625 -5`.

3. #508 wants a way to
   show Integers signed, but only showing the sign when it's
   negative (that is, no leading +). This cannot be done with Integers
   currently, forcing this work to invent its own signed integer type.

This does open the door to exposing the total ordering of Integers (as
we now expose enough to determine the total ordering of Naturals). It
also gives you *some* form of Integer arithmetic, but you can't
reconstruct an Integer from it's signed type.
@@ -1269,6 +1269,26 @@ the nearest `Double`. Ties go to the `Double` with an even least significant
bit. When the magnitude of `a` is greater than or equal to `c`, the magnitude
will round to `Infinity`, where `c = 2^1024 - 2^970 ≈ 1.8e308`.


`Integer/toSigned` transforms an `Integer` into a pair of a `Natural` number,

This comment has been minimized.

Copy link
@ocharles

ocharles Jul 29, 2019

Author Member

Calling this a pair is a bit loose, would people prefer something more precise? Or should I move the a -> 0 rule further up, if we assume rules are tried sequentially?

and the sign of the number.


f ⇥ Integer/toSigned a ⇥ -n

This comment has been minimized.

Copy link
@ocharles

ocharles Jul 29, 2019

Author Member

Should this rule say ; n != 0 too? It seems potentially ambiguous otherwise.

@singpolyma

This comment has been minimized.

Copy link
Collaborator

singpolyma commented Jul 29, 2019

@ocharles

This comment has been minimized.

Copy link
Member Author

ocharles commented Jul 29, 2019

@singpolyma Then fine, that can be a matter of taste that the user can choose. Right now, they do not have that choice. This PR is more than just enabled scientific notation though. I would prefer to be able to write 0.whatever and get a { numerator : Natural, denominator : Natural } or something, but that's a much bigger change.

@singpolyma

This comment has been minimized.

Copy link
Collaborator

singpolyma commented Jul 29, 2019

@ocharles

This comment has been minimized.

Copy link
Member Author

ocharles commented Jul 29, 2019

Maybe, but I don't think that has much bearing on this PR - I still want to be able to write e foo -5. Given that Integers support no arithmetic at all at the moment, I don't think I can make any more progress.

@sjakobi

This comment has been minimized.

Copy link
Collaborator

sjakobi commented Jul 29, 2019

< Negative : Natural | Zero | Positive : Natural > has the downside of two unwanted but possible states: Negative 0 and Positive 0.

Alternatively you could use a representation inspired by two's complement: < N : Natural | P : Natural > where +0 is represented as P 0, -1 as N 0, -2 as N 1 etc. I haven't found any nice names for the alternatives though.

@singpolyma

This comment has been minimized.

Copy link
Collaborator

singpolyma commented Jul 29, 2019

If we do this, I would love to see the names more like

< `-`: Natural, `0`, `+`: Natural >

Though that's just how I feel. The current names are fine.

I also feel like if we want this it sort of makes me question why we want the Integer type at all. Maybe we just want a syntactic sugar for generating something like this?

@Nadrieril

This comment has been minimized.

Copy link
Collaborator

Nadrieril commented Jul 29, 2019

@singpolyma I'd say it's for the same reason Optional is a special thing instead of being encoded as < None | Some : T >

@singpolyma

This comment has been minimized.

Copy link
Collaborator

singpolyma commented Jul 29, 2019

@Nadrieril My feelings on Optional aside, Optional is at least directly useful, though. Right now the only reason to use Integer is to have an opaque type -- if we merge this then we lose that (since you could go to Natural, do stuff, then convert back to Integer)

@ocharles

This comment has been minimized.

Copy link
Member Author

ocharles commented Jul 29, 2019

At first I thought you couldn't turn a natural into an integer, but now I realise that you could fold the natural (which is a horribly inefficient strategy, but would work). So yes, this does change something more fundamental than I originally thought

@Gabriel439

This comment has been minimized.

Copy link
Contributor

Gabriel439 commented Jul 30, 2019

I have the same concern as @sjakobi: the < Negative : Natural | Zero | Positive : Natural > representation allows invalid states to be representable.

However, I think if the end goal here is to be able to embed rational numbers in Dhall then I'd prefer to instead add native language support for rational numbers, for the same reason that the language supports Integers.

My reasoning is that Dhall is, first and foremost, a configuration file format, meaning that even if you strip away all of the programming language features Dhall still has to satisfy the basic property that it can ergonomically store data. This is why dhall supports Integers natively, even though they are opaque; users still need a place to put Integers, even if only to pass them through to the host program being configured.

@ocharles

This comment has been minimized.

Copy link
Member Author

ocharles commented Jul 30, 2019

Ok, I will look into closing this and standardising rational numbers. I actually think Double as is is really Rational - it only supports writing literals, and hence only rational numbers - you cannot write truly irrational numbers like start(2). I'll have a think

@ocharles ocharles closed this Jul 30, 2019
@Gabriel439

This comment has been minimized.

Copy link
Contributor

Gabriel439 commented Jul 30, 2019

@ocharles: Perhaps you could add a Double/toRational : Double → { numerator : Natural, denominator : Natural } built-in

@singpolyma

This comment has been minimized.

Copy link
Collaborator

singpolyma commented Jul 30, 2019

@ocharles

This comment has been minimized.

Copy link
Member Author

ocharles commented Jul 30, 2019

We may also want to consider Agda's model, which model x / 1 as { numerator = x, denominator-1 = 0 }

@ocharles

This comment has been minimized.

Copy link
Member Author

ocharles commented Jul 30, 2019

I am also not interested in 0, -0, +0, NaN and Inf, so it does suggest it's something different.

@Gabriel439

This comment has been minimized.

Copy link
Contributor

Gabriel439 commented Jul 30, 2019

We should probably continue this discussion on a Discourse thread

@ocharles

This comment has been minimized.

Copy link
Member Author

ocharles commented Jul 30, 2019

I agree - there's one already open, let's carry on there.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
5 participants
You can’t perform that action at this time.