https://numbat.dev/articles/intro.html

Introducing Numbat

Part I: The type system

Numbat is a programming language that aims to provide a convenient
way to perform computations with physical units. One of the main
goals of the language is to help users write correct programs. It has
a static type system where physical dimensions act as types. The
expression 3 months, for example, has a type of Time. Similarly, the
expression 2 years also has a type of Time. The compound expression 3
months + 2 years is therefore well-typed:

3 months + 2 years # you can edit these examples!

On the other hand, 3 months + 2 lightyears is ill-typed, because the
right-hand side is of type Length. You can change 'years' to
'lightyears' in the editor above to see the resulting compiler error.

Before we describe the type system in more detail, let's look at two
simple examples. The first program computes the oscillation period of
a (mathematical) pendulum using the gravitational acceleration g0.
Note that you can change the unit of the pendulum length to, say,
inch without having to change the type annotations. This is in
contrast to a lot of unit libraries in other programming languages
that typically lift units -- not the physical dimensions -- to the type
level. Also, note that you can completely remove the explicit : Type
annotations and let the compiler infer the types:

let pendulum_length: Length = 30 cm let t_oscillation: Time = 2 p
sqrt(pendulum_length / g0) t_oscillation

The second example demonstrates how explicit type annotations can
help avoid mistakes. We want to compute the ratio of gravitational
forces exerted on Earth by both the Sun and the Moon. However, the
computation contains a mistake. Try to annotate the definitions of
force_sun and force_moon with the intended Force dimension and see if
the compiler error can help you fix the equations. The correct result
should be closer to 180.

let distance_sun: Length = 1 AU # astronomical unit let
distance_moon: Length = 384_400 km let force_sun = G * earth_mass *
solar_mass / distance_sun let force_moon = G * earth_mass *
lunar_mass / distance_moon force_sun / force_moon

A type in Numbat can be one of three things. It can be 1 -- which is a
special type for dimensionless quantities, it can be a base
dimension, or it can be an algebraic combination of other types. We
use the dimension keyword to introduce new types. For example, this
is how basic physical dimensions from classical mechanics are defined
in Numbat's prelude:

dimension Length dimension Area = Length2 dimension Time dimension
Frequency = 1 / Time dimension Velocity = Length / Time dimension
Acceleration = Length / Time2 dimension Mass dimension Force = Mass x
Acceleration dimension Pressure = Force / Area dimension Energy =
Force x Length dimension Power = Energy / Time

Note how the three base dimensions length, time and mass can be
combined using multiplication, division and exponentiation. Now there
is not a lot we can do with those types until we introduce
corresponding units to build quantities that inhabit those types:

unit metre: Length unit second: Time unit kilogram: Mass # in the
real prelude, we properly handle prefixes unit hertz: Frequency = 1 /
second unit newton: Force = kilogram metre / second2 unit pascal:
Pressure = newton / metre2 unit joule: Energy = newton metre unit
watt: Power = joule / second 2 * newton + 1 * watt / (metre / second)

Now take a look at the last line. When the type checker encounters an
expression like this, it infers the overall type (Force) by
recursively walking the syntax tree. Multiplication and division
nodes are easy. We simply combine the types in the same way that we
combine the expressions:

type(a * b) = type(a) * type(b)
type(a / b) = type(a) / type(b)

However, addition and subtraction are different. If the types on both
hand sides are the same, we return that type. If they are not, we
raise a type check error:

type(a + b) =
  if type(a) == type(b) {
    type(a)
  } else {
    error("incompatible dimensions in addition ...")
  }

Comparison operators like == or > also work in a similar way -- can't
compare apples and oranges -- except that they return a boolean type.
You can try this by replacing addition with a comparison operator in
the example above.

Finally, there is exponentiation: a^b. And it turns out to be quite a
bit more complicated. We first note that the exponent b needs to be
dimensionless. An expression like (2 m)^(3 kg) is not meaningful. But
even then there is a problem. Imagine something like (2 m)^(1 + 2).
It should have a type of Length^3. But this means that the type of
the expression depends on the value of the exponent. It turns out we
need to evaluate the expression b at compile time to determine the
type of a^b:

type(a ^ b) =
  if type(b) != 1 {
    error("exponent needs to be dimensionless")
  } else {
      if type(a) == 1 {
        1
      } else {
        type(a) ^ consteval(b)
      }
  }

Numbat therefore has a special const-evaluation mode that can compute
a subset of expressions as part of the type-checking phase. Note that
the restriction to a subset of operations is not a limitation in
practice. Real world computations often have complicated expressions
in the exponent. But in those cases, the left-hand side (a) is always
dimensionless and the overall type is simply 1. And when a is not
dimensionless, the exponent expression is typically just a (rational)
number.
One interesting application of the exponentiation operator is the
sqrt function that you saw in the very first example. It can take
dimensionful quantities as an argument. And it can be defined in this
way:

fn my_sqrt<D>(x: D^2) -> D = x^(1/2) my_sqrt( G / c^5) # Planck time

Here, D is a generic type parameter. The function takes an argument
of type D^2 and returns a D. In the example here, it turns Time^2
into Time. In general, type inference for functions is an interesting
topic for another day.

Our final example demonstrates how you can make use of custom
dimensions and units. This is often useful when you want to count
things (people, atoms, pixels, or in this case: drops). Say we want
to compute the required IV drip rate for an infusion of 1200 mL of
saline solution over 6 hours. Even if it might look like overkill in
this simple example, note how the introduction of a new unit not just
helps with correctness, but also with readability:

unit drops # Implicitly creates a new base dimension 'Drops'
dimension DripRate = Drops / Time let saline_volume = 1200 mL let
drop_factor = 15 drops / mL let total_time = 6 hours let iv_drip_rate
= saline_volume * drop_factor / total_time iv_drip_rate -> drops /
min

If you want to learn more about Numbat, consider reading the language
tutorial. Numbat is open source. It is available both on the web
(running locally in your browser) and as a command-line application.