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

Generic Arithmetic #831

Open
jackfoxy opened this issue Jan 30, 2020 · 12 comments
Open

Generic Arithmetic #831

jackfoxy opened this issue Jan 30, 2020 · 12 comments

Comments

@jackfoxy
Copy link

@jackfoxy jackfoxy commented Jan 30, 2020

Generic Arithmetic

I propose we implement generic arithmetic by allowing the arithmetic operators, (+, -, *, /, %), and comparison operators to operate on mixed number types, and expand their use to operate on functions and collections.

The sub-typing involved is deterministic and transparent (obvious to the user).

This proposal was inspired by the generic arithmetic implementation in Sussman and Wisdom, Structure and Interpretation of Classical Mechanics (MIT, 2014), 16 n, 509.

The existing way of approaching this problem in F# is applying a conversion operator to bring both binary operators into conformity. This proposal demonstrates deterministic rules for this conversion which can be done in the compiler.

Inferred conversion of number types

I will use 'Scalar to refer to the generic type of all numbers, with the familiar number types being the subtypes. (I may have that reversed.)

bool (treat as a number for arithmetic, but possibly not for comparison)
sbyte
byte
int16
uint16
...
uint64
decimal
float32
float

The rule for the compiler is to convert the less explicit to the more explicit number type before performing the operation. (I use explicit to refer to the count of representable numbers.) Thus the result of arithmetic operations will be in the more explicit number type.

let x = 1 + 2.0
\\ 3.0

The rule for mixing signed and unsigned on addition and multiplication is maybe not so transparent. In order to prevent overflow, if the more explicit type is unsigned, and the less explicit signed, both numbers should be converted to the signed integer one step higher. (In the case of uint64 this should be BigInteger, but this is probably not possible since that type is defined in System.Numerics.)

Operations and 'Scalar conversions respect units of measure.

Operations on functions

Arithmetic and comparison operations on functions require the signature of both functions to be the same up to result, and both results are 'Scalar. The result is a new function.

\\ f1 : 'input -> 'Scalar
\\ f2 : 'input -> 'Scalar
let f3 = f1 + f2
(\*
fun (input : 'input) -> (f1 input) + (f2 input)
\*)

Or result signatures are compatible for operations on collections (see below),

or one operand is a 'Scalar and the function operand has a compatible result signature,

or two function operands have a result signature of 'input2 -> 'result, where 'result is any compatible type already mentioned.

Operations on collections

Available for the collections Array, List, seq, and Set (maybe Map).
The collection signature must be Array<'Scalar> or Array<'input -> 'Scalar>

A 'Scalar operation on a collection is syntactic sugar for

\\ s : 'Scalar
\\ arr : Array<'Scalar>
let arr2 = s + arr
(\*
arr |> Array.map (fun a -> s + a)
\*)

and between like collections is syntactic sugar for

\\ arr1 : Array<'Scalar>
\\ arr2 : Array<'input -> 'Scalar>
let arr3 = arr1 + arr2
(\*
Array.zip arr1 arr2 |> Array.map (fun (a1, a2) -> fun (input : 'input) -> (a2 input) + a1)
\*)

Pros and Cons

The advantages of making this adjustment to F# are making code more concise and readable. Explicit number type conversion is still an available option. I maintain the type safety of the status quo provides no useful safety in arithmetic and comparison.

The disadvantage of making this adjustment to F# is the risk of any modifications to the type system. Mixing bool and number types for comparison operators is the one instance (I can think of) where we could lose type safety. Therefore we may want to exclude this case.

Extra information

Estimated cost: Large

I am ignorant of the implications for type unification and inference.

Ideally BigInteger would be the escalation type for signed/unsigned int64 addition and multiplication, but this is complicated by it being defined in System.Numerics.

A System.Numerics.FSharp implementation would ideally cover BigInteger, Complex, Quaternion, and Vector types.

Related suggestions:

#737
#562

This is different than supporting generic numbers as a type.
#737 (comment)

Affidavit

Please tick this by placing a cross in the box:

  • This is not a question (e.g. like one you might ask on stackoverflow) and I have searched stackoverflow for discussions of this issue
  • I have searched both open and closed suggestions on this site and believe this is not a duplicate
  • This is not something which has obviously "already been decided" in previous versions of F#. If you're questioning a fundamental design decision that has obviously already been taken (e.g. "Make F# untyped") then please don't submit it.

Please tick all that apply:

  • This is not a breaking change to the F# language design
  • I or my company would be willing to help implement and/or test this
@drvink

This comment has been minimized.

Copy link

@drvink drvink commented Jan 30, 2020

While I understand the argument for "ergonomics" in this context, the proposal here is proposing to replicate two notoriously dangerous and surprising aspects of the Scheme-style "numeric tower" as well as C/C++'s implicit numeric promotions. You really don't want to go down this path...


F# doesn't have a rational type, but Scheme does, and it participates in the numeric tower (without going into details, just take this to mean "an ad-hoc set of rules governing implicit conversions") in a dangerous way:

scheme@(guile-user)> ,use (oop goops)
scheme@(guile-user)> (class-of 3)
$1 = #<<class> <integer> 7f38e837d630>
scheme@(guile-user)> (class-of 3.0)
$2 = #<<class> <real> 7f38e837d6c0>
scheme@(guile-user)> (class-of (/ 1 3))
$3 = #<<class> <fraction> 7f38e837d5a0>
scheme@(guile-user)> (class-of (+ 1 3.0))
$4 = #<<class> <real> 7f38e837d6c0>
scheme@(guile-user)> (class-of (/ 1 3)) ; this gives fraction, which is ok
$5 = #<<class> <fraction> 7f38e837d5a0>
scheme@(guile-user)> (class-of (+ 0.1 (/ 1 3))) ; but it decays dangerously...
$6 = #<<class> <real> 7f38e837d6c0>
scheme@(guile-user)> (/ 1 3)
$7 = 0.3333333333333333
scheme@(guile-user)> (+ 0.1 (/ 1 3))
$8 = 0.43333333333333335 ; yikes!

Explaining why this is dangerous involves a discussion of floating point representation and numerical analysis, though I'm sure you're already aware of the details here...


C/C++ has similarly dangerous rules. Here's what happens when we multiply two uint16_t that are allowed to be promoted given exactly the rules you suggest are safe:

In order to prevent overflow, if the more explicit type is unsigned, and the less explicit signed, both numbers should be converted to the signed integer one step higher.

#include <iostream>
#include <limits>
#include <cstdint>
#include <cstdlib>

static uint64_t
mul(uint16_t const a, uint16_t const b)
{
    uint32_t const res = a * b;
    return res;
}

int
main(int argc, char **argv)
{
    if (argc < 3) { return EXIT_FAILURE; }

    auto const x = mul(atoi(argv[1]), atoi(argv[2]));
    std::cout << x << std::endl;

    return EXIT_SUCCESS;
}
arch-vm[989]:~% g++ -Wall -O0 -o dennace dennace.cpp
arch-vm[990]:~% ./dennace 65535 65535
4294836225
arch-vm[991]:~% g++ -Wall -O2 -o dennace dennace.cpp
arch-vm[992]:~% ./dennace 65535 65535
18446744073709420545

Yikes. (The optimization is significant here, as it enables the rule that you claim is reasonable which I quote above.)

@jackfoxy

This comment has been minimized.

Copy link
Author

@jackfoxy jackfoxy commented Jan 30, 2020

@drvink You make very good points. I was restricting my use of safe to type safety.

To summarize your first example (and you have a deeper understanding than I), floating point.

Programmers are going to mix numeric types. They do it all the time, and usually get away with it. Now they have to do it in a wonky fashion. Programming languages are tools, not ends in themselves (well, maybe brainfuck). Razors are tools. You can use one to shave, or cut your throat. We don't outlaw razors.

Your point on integer overflow is even better.

uint32_t const res = a * b

As you demonstrate, we can already overflow on add and multiply within the same integer type and the runtime will happily give you a result.

So yes, my unsigned rule does not prevent (at best it mitigates) overflow, definitely my faux pas.

But perhaps I didn't explain clearly, the conversion should happen before the arithmetic operation.

// and thanks for pointing out Int32 does not save us
int64 (65535us * 65535us)
// val it : int64 = 1L
int64 65535us * int64 65535us
// val it : int64 = 4294836225L
@jackfoxy

This comment has been minimized.

Copy link
Author

@jackfoxy jackfoxy commented Jan 30, 2020

Apologies if I misinterpreted either of your examples. I can sort of read Scheme, C++ is out of my depth.

@drvink

This comment has been minimized.

Copy link

@drvink drvink commented Jan 30, 2020

No worries! Indeed, F# already does the reasonable thing in the example you for that particular case of "optimization"--the point is basically that when these kinds of rules accumulate, the end result may be surprising to not just the language designer, but particularly the user :)

@gusty

This comment has been minimized.

Copy link

@gusty gusty commented Jan 31, 2020

@drvink would you prefer the Generic Numbers proposal instead?

@cartermp

This comment has been minimized.

Copy link
Member

@cartermp cartermp commented Jan 31, 2020

See this comment and the following discussion regarding inferred numeric types: #737 (comment)

@drvink

This comment has been minimized.

Copy link

@drvink drvink commented Jan 31, 2020

@gusty @cartermp i've replied in #737 since the inference issue is actually separate from this one.

@ReedCopsey

This comment has been minimized.

Copy link

@ReedCopsey ReedCopsey commented Jan 31, 2020

To me, this feels like 3 or 4 separate feature requests - 1) numeric type handling and "auto promotion" of number types, the collection handling, and function handling (and potentially the combination of the latter two).

Personally, I am a fan of the current behavior in terms of numeric type handling and the lack of promotion. The fact that there are no implicit conversions actually does add safety - mostly in API design.

If this proposal were to be implemented, the "promotion" to different numeric types could easily change the inferred type of functions without any compiler warnings or errors. The current behavior of not having implicit conversions or promotions of numeric types has prevented issues in our (heavily mathematical) code. In particular, promotion of integer types to floating point types has been problematic in C++, and F# avoids that nicely.

The one place where I might have less of an issue would be automatically allowing promotion of literals (only), but that definitely seems like a separate, very limited subset of this request.

@jackfoxy

This comment has been minimized.

Copy link
Author

@jackfoxy jackfoxy commented Jan 31, 2020

@ReedCopsey You have identified a use case I had not thought of, emitting an unintended api method signature without benefit of a signature file.

The only other use case I can think of is coding-up an offending let binding first, and never noticing the input signature of all the consuming code.

I'm really interested to hear of other use cases. Otherwise the type checker is always going to alert you.

In my experience of F# math coding, explicit conversion has been nothing but an annoyance. But I consistently use signature files over my api's.

@charlesroddie

This comment has been minimized.

Copy link

@charlesroddie charlesroddie commented Jan 31, 2020

Can't this request be narrowed down to allowing operator overloads in extension members? Then you could do:

type System.Double with
    static member (+) (x:int,y:float) = (float x + y)

I personally wouldn't use this as I like the restrictiveness of F#, and would love it if other languages I have to use (SQL) had a mode with no implicit conversions.

@dsyme

This comment has been minimized.

Copy link
Collaborator

@dsyme dsyme commented Jan 31, 2020

Can't this request be narrowed down to allowing operator overloads in extension members? Then you could do:

Good point.

The processing of primitive types and SRTP is a little sensitive and I would like to check if this works as part of the RFC for this

@gusty

This comment has been minimized.

Copy link

@gusty gusty commented Jan 31, 2020

@charlesroddie I did quite a lot generic arithmetic sometime ago and I can tell you that overloading operators that way doesn't take you too far.

Sooner than later you will get type inference problems, ambiguous overload resolution, you'll be forced to annotate every single parameter. But those are not technical limitations, those are logical problems.

IMHO overloads a-la C# don't scale, overloads should be organized in a consistent way, that's why Category Theory stuff is becoming important nowadays, because it provides you a framework where you (and usually type inference as well) can reason about the types and predict overload resolution in a non-surprising way.

The Haskell approach was to stick with operations like (+) :: Num -> Num -> Num and the flexibility comes from generic literal numbers instead. Still their Numerics abstractions are far from ideal, but at least solve the interaction between different numbers in a nice way.

Unfortunately F# didn't define math operators (at global level) that way, probably due to the fact that pre-existing types from the framework have already mixed types (stuff like DateTime + float).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked pull requests

Successfully merging a pull request may close this issue.

None yet
7 participants
You can’t perform that action at this time.