sharkdp / numbat

A statically typed programming language for scientific computations with first class support for physical dimensions and units
https://numbat.dev
Apache License 2.0
1.17k stars 50 forks source link

Add/Sub type classes for operator overloading #462

Open sharkdp opened 3 months ago

sharkdp commented 3 months ago

We currently use operator overloading for DateTimes. We can perform the following three operations:

Every other addition/subtraction operation with DateTimes is disallowed. This is important because constructions like DateTime + DateTime are not meaningful.

The currently implemented operator overloading works fine whenever we have concrete types:

>>> now() + 4 days

    = Sat, 15 Jun 2024 18:44:56 +0200    [DateTime]

but if fails if intermediate type variables are involved (see similar issue for structs here: #459). For example, we currently can not do this:

fn id(x) = x
id(now()) + 4 days

Similarly, if we write the function

fn add_four_days(dt) = dt + 4 days

without a type annotation for the parameter type, we will not get the most general type inferred (which cannot even be expressed in Numbats type system at the moment).

Ideally, we would have something like a (multiparameter) type class or trait (Add, Sub), that we could use to model operator overloading. This would allow us to infer the most-general type (using a Rust-like syntax again):

fn add_four_days<A, B>(dt: A) -> B
  where A: Add<Time, Output = B>
  = …

which would allow us to use this function both with DateTime and Time.


If it were only for DateTime, I think we might be able to live with the current restriction. But there might be some other cool examples where we could make use of proper Add/Sub constraint handling. For example, we could introduce specialized types for Celsius and Fahrenheit that would potentially implement (in close analogy to what we have for DateTime and Time):

Ref: #184

Another use case might be logarithmic units like decibel, for which we could implement specialized addition/subtraction operations.

Ref: #387

We could start by only allowing those constraints to be resolved internally by the type checker, without going all in on user-definable type classes. But those would be interesting as well, obviously:

struct Vec {
  x: Length,
  y: Length,
}

impl Add<Vec> for Vec {
  type Output = Vec;

  fn add(lhs: Vec, rhs: Vec) -> Output = …
}

impl Mul<Scalar> for Vec {
  type Output = Vec;

  fn add(lhs: Vec, rhs: Scalar) -> Output = …
}
sharkdp commented 3 months ago

One thing that we should consider before implementing this is whether or not we can keep up the quality of error messages.