proposal: Go 2: Add dimensionality to enrich type system and strengthen compile-type checking

[czetie]

Author background

• Would you consider yourself a novice, intermediate, or experienced Go programmer?
  Novice with Go, experienced with other languages esp. C

• What other languages do you have experience with?
  Fortran, Pascal, Algol, C, Rust, Python, PL/M, various assembler

Related proposals

• Has this idea, or one like it, been proposed before?
  Not to my knowledge or that of other Go programmers I spoke with

• Does this affect error handling?
  No

• Is this about generics?
  No

Proposal

• What is the proposed change?
  Golang does not allow mathematical operations between operands of different types, even if they have compatible underlying types. This provides highly useful protection for addition and subtraction and is helpful in avoiding a certain class of logical errors. For example, it is almost certainly a logical error to attempt to calculate speed + elapsedTime, (assuming their types have been appropriately defined as float64, for example). However, this is too restrictive for multiplication and division: distance = speed * elapsedTime is a perfectly reasonable calculation. In order to perform this calculation today, the programmer must reduce everything to compatible types, typically the underlying types, this sacrificing the benefits of type checking. For example:

type distance float64
type time float64
type velocity float64

var v velocity
var d distance = 100
var t time = 2

v = d / t                                                  //will not compile, incompatible types
v = velocity(float64(d) / float64(t))        //will compile, but throws away type checking of d and t

A small enhancement to the rules for type mixing in expressions would allow useful constructs as mentioned above such as distance = speed * elapsedTime, as well as other more complex calculations, while still preventing mistakes such as distance = speed + elapsedTime. The characteristic of these calculations is that they mix values of different "dimension", in this case velocity, which in turn can be defined as having dimension Length/Time; and Time. And the resulting value has dimension different from either, i.e. Length in this case. While adding values of different dimension makes no sense, multiplying or dividing them can be perfectly meaningful and extremely useful.

This proposal would allow the developer to specify, by using the type system, dimensions and valid combinations of dimensions together with the new dimension that they result in.

• Who does this proposal help, and why?
  This proposal would help any programmer working with data that has dimensions, e.g. physical quantities of Length, Time, Distance, or combinations of them, i.e. essentially all scientific and engineering data, by providing an added compile-time check that only quantities of the correct dimension are being mixed.

It could also help programmers in commercial applications where dimension might be defined more abstractly than in physics. For example, to estimate project cost we multiply "number of FTEs" by "fully loaded FTE cost" to get a result in dollars (or appropriate currency). We should not be able to use any old number defined in dollars in this calculation, but only one defined as an FTE cost. Or we might estimate project duration by dividing "number of story points" by "story points per FTE per day" and multiplying by "number of FTEs" to get a result with dimension measured in Days. Other examples of common classes of commercial mistake that can be caught with appropriate definitions include mixing quantities in different currencies; or multiplying by a fraction (0.0 to 1.0) instead of a percentage (0.0 to 100.0).

The more complex the calculation, the more valuable the checking of dimension. And to reiterate, this checking is lost today even if the programmer defines types, because in order to write calculations that mix types, they must be reduced to the underlying type, e.g. float64.

• Please describe as precisely as possible the change to the language.
  This proposal would ADD a new form of type definition as an extension to existing syntax to define a type as the product or quotient of other types.

It would also MODIFY the restriction on mixing types in arithmetic expressions: it would still be forbidden to mix types in addition and subtraction, but it would be permitted to mix types in multiplication and division provide they have compatible underlying types.

• What would change in the language spec?

1. Multiplication or division of values and variables of different types would be allowed, provided their underlying types are compatible.
2. The syntax for defining types would be extended to define types in terms of the product or quotient of other types, e.g.

type distance float64
type time float64
type mass float64
type velocity (distance / time)
type acceleration (velocity / time) 
type force (mass * acceleration)
type energy (mass * velocity * velocity)

Such type definitions could be compounded to any (reasonable) degree necessary for the domain of the application.

• Please also describe the change informally, as in a class teaching Go.
  Consider the following code fragment that attempts to calculate a velocity from the division of distance by time.

type distance float64
type time float64
type velocity float64

var v velocity
var d distance = 100
var t time = 2

v = d / t		//will not compile

The compiler will reject the assignment because the quotient of d and t has a different type from v, even though they have the same underlying types. Specifically, d / t has type (or dimension) distance / time, which is not the same as velocity- at least as far as the compiler knows! We could make it compile by the following explicit type conversions:

v = velocity(float64(d) / float64(t))

However, now we have sacrificed the type checking that we had hoped for by creating types for distance and time; d and t could mistakenly be variables of any type whose underlying type is float64.

A better approach which allows us to retain the type checking is to define the type velocity not as float64 but as the quotient of types distance and time:

type distance float64
type time float64
type velocity (distance / time)

var v velocity
var d distance = 100
var t time = 2

v = d / t		//will compile, retains type checking

Of course, this example is very simple; real scientific and engineering formulas will often have many more variables and types.

• Is this change backward compatible?
  Yes. This does not remove or change any existing syntax; nor change the semantics of any existing compilable code. It extends the allowed forms for calculations (type mixing) and for specifying types in terms of other types.

• Orthogonality: how does this change interact or overlap with existing features?
  The concept of dimension is complementary to existing syntax for types, but as far as other language features are concerned, e.g. parameter passing, the end result behaves just like existing types.

• Is the goal of this change a performance improvement?
  No.

Costs

• Would this change make Go easier or harder to learn, and why?
  Probably minimal change. One small addition to the syntax for types is added, and a potential confusion about mixing types is removed.

• What is the cost of this proposal? (Every language change has a cost).
  Modest. Existing code for determining the underlying types of variables and expressions and for converting between types, particularly to and from arithmetic types, will be relevant and can probably be reused. Additional code will be required in the code for parsing arithmetic expressions (see below under proposed implementation).

• How many tools (such as vet, gopls, gofmt, goimports, etc.) would be affected?
  Compiler only.

• What is the compile time cost?
  Modest. Additional checking for type compatibility in multiplications and divisions involving defined types whereas today those expressions are quickly rejected as errors.

• What is the run time cost?
  Nil. After compile-time checking, the code reduces to the underlying types like any other calculation.

• Can you describe a possible implementation?
  The compiler builds a dependency tree of types defined in terms of other types all the way down to underlying types. When it encounters an expression that multiplies or divides types it traverses the tree down to one level above underlying types, and verifies that dimension matches on both sides. For example, with the definitions

type distance float64
type time float64
type mass float64
type velocity (distance / time)
type acceleration (velocity / time) 
type force (mass * acceleration)
type energy (mass * velocity * velocity)

a variable of type energy has dimension (mass * velocity * velocity) which expands to (mass * (distance / time) * (distance / time)). The compiler will also expand the types of the variables to ensure that they have the same base dimensions, e.g. (force * distance) expands to (mass * acceleration * distance) and finally to (mass * distance / time / time * distance). Note that in order to see that these two are the same dimension, they must be rearranged into a common canonical form. However, this can be as simple as a list of base dimensions and for each a list of their indexes, e.g.
mass^1
distance^2
time^-2

Therefore, verifying compatibility requires only traversing the dependency tree to the bottom and accumulating a count of the index of each base dimension.

• Do you have a prototype? (This is not required.)
  No.

Long prose description of proposal:
Enhancement request_ Dimensionality of Types.docx

[ianlancetaylor]

Historically Go has encouraged programming by writing code rather than coding by designing types. This change seems to make the type system more complicated in order to simplify the actual code. That's not a path that Go usually takes.

I'm also not completely clear on how this works. If velocity is distance divided by time, then distance is time multiplied by velocity. If I write type distance float64; type time float64; type velocity (distance / time) then will the compiler permit distance to be divided by time but will not permit velocity multiplied by time?

[czetie]

1. The complication of the type system is minimal, and can be completely ignored by those who don't want to use it.

2. In terms of the Go philosophy I don't see this as any less idiomatic than types in general; and certainly less so than, say, the introduction of generics; or the protections afforded by interfaces. If this is the philosophy, one might as well argue against simple types (i.e. "aliasing" of underlying types) entirely, since it creates more problems than value. In any case, I would argue that there is always value in indicating intentions to the compiler and letting it help avert mistakes, especially when (a) there is no down side as using the construct is entirely optional and (b) there is no runtime cost. I am a big proponent of simple language features that remove mental burden from the developer allowing them to focus on logic rather than, say, details of the type conversion rules.

3. What is the programmatic alternative here? As far as I can see, the only way to do this without this enhancement is to cast everything down to float64, which eliminates the value of creating types in the first place; significantly complicates the code; obfuscates the programmer's intention for the reader (and isn't it a general principle that code is read many more times than it is written?). Am I missing something? If there were a way to achieve the same thing purely in code that I'm missing, I would be much more sympathetic to the argument that this is an unnecessary complication.

Perhaps the clarity and usefulness of this would be more clear in a more complicated, real-world example involving more variables and dimensions?

4. I am a huge fan of the type system in Golang, which in combination with interfaces and the direction generics are going in is IMO extremely powerful while avoiding the complexity traps other languages have fallen into. And I think it can be leveraged very powerfully as a complement to coding rather than an alternative.

5. Yes, you could also write d = v * t (with appropriate var declarations, obviously). The compiler would determine that indexes of the dimensions of v are
   distance 1
   time -1
   and of t it is
   time 1
   leaving just distance, which matches d. And the same would apply to more complex calculations with more dimensions, e.g. energy or power.

[DeedleFake]

I'm unclear how often something like would be useful. Velocity, time, and distance are pretty obvious, but in a program, how often can types be related like this? Can this handle more complicated relationships that map to more programming-related problems, rather than physics? In other words, can you give an example of something that is more likely to come up in an actual project?

[golightlyb]

I would encapsulate the type conversions in a function like so:

func calcVelocity(d distance, t time) velocity {
   return velocity(float64(d) / float64(t))
}

Is that insufficient?

[czetie]

First, thank you for your engagement on this and testing whether the idea is robust.

That's as close as I could get too. (I tried doing the equivalent with an anonymous function, but for some reason couldn't get the typing to pass the compiler...).

The main difference here is that the compiler is no longer checking dimensions for us, because we have not told it explicitly that there is a relationship between velocity, distance, and time. So if we made a coding error in the function (unlikely in this simple example, more likely in realistic examples), such as mistakenly writing

return velocity(float64(t) / float64(d))

the compiler would not be able to detect it.

So I think I would say that this is considerably more verbose than being able to write v = d / t, and a lot less clear to the reader than having to jump off to read a function definition, and loses the dimension checking. It also requires a separate function for every distinct formula we want to write this way. Finally, it adds the overhead of a function call (I have no idea how efficient that is in Golang?) - unless the compiler is smart enough to inline the function, which it might do for sufficiently simple functions.

So one way to think of this is that we are in a sense "inlining" the type checking that function parameters perform and putting it into the type checking of the variables directly in the formula; and in addition we gain the dimensional analysis that guards against incorrect formulas.

Would it help if I were to show some more extended examples?

[czetie]

@DeedleFake I have spent the last decade primarily working with people doing scientific and engineering projects so I admit I have a kind of population bias. However, with those people dimensional analysis is something they do all the time as verification of their formulas; so it would be very valuable to that population for the compiler to verify their formulas.

However, I do think lots of other domains have the potential to benefit although in less obvious ways than physics dimensions - although it might take a bit of a mental shift to realize that their variables have dimensions. For example, I have also been working with people in distributed storage-defined software and here they have many integers being juggled in calculation such as buffer size (bytes); bytes per block; blocks per network packet; overhead (bytes); queue lengths; etc. Consequently, it is easy and far from unknown to mix up what different integers represent when calculating buffer sizes, overhead allowances, etc. So for one simple example, if we want to compute how many bytes fit in a network packet, we calculate bytes per block * blocks per network packet, which very naturally has units of bytes per network packet.

Another example comes from own experience in a factory automation system, one of the gnarliest I dealt with as field engineer. At a canned food factory there was a production line subsystem that counted cans off the line, and a warehouse management subsystem that counted them into the warehouse. However, the latter subsystem was crashing periodically with an integer overflow. Eventually I found the problem at the interface between the two subsystems: the warehouse subsystem was expecting to receive a count of the number of pallets, which it then multiplied by 16 to get the number of cases of product in stock. However, the programmer of the production line system was not passing the number of pallets, but rather the number of cases, which when multiplied by 16 caused the crash. Judicious use of definitions (dimensions) such as countCansPerCase, countCasesPerPallet, countCases, and countPallets could have prevented the confusion. Lots of errors of this class happen at the interface between subsystems (e.g. the Mars mission that was lost because of a confusion between Metric and Customary units).

For another domain example, consider project tracking/planning software. You might have lots of integer values such as number of FTEs; story points for each story; story points per day for each programmer; burn down rates; etc. As integers they can be combined in many ways, most of them meaningless. By defining dimensions such as FTEs, story points, days, etc. we can ensure that we are only combining them in meaningful ways.

[czetie]

@DeedleFake P.S. if you have an existing codebase I could look at and see how it might work with this proposal, I am willing to do so. I think that is a fairer test than my making up an arbitrary or hypothetical example.

[OwlSaver]

I really like this idea. It brings something that we naturally do every day and makes it a part of the language. In banking and insurance domains there are many dimensions that would only help to ensure the calculations are correct. It seems to me that this is a mechanical check that is actually very hard for humans to do. But it would be easy for a machine to do.

Make it a basic feature of function parameters. Then it can easily be applied to the special case of operators.

[atdiar]

Dimension checking is something that gets drilled into us when dabbling in physics but from a comp.sci point of view, how would someone implement this?

All I can think of seems to rely on operator overloading at its basis (which is not allowed in Go for also good reasons) .
Is this what this proposal could be reduced to? Anyone has an idea?

Edit: more specifically, a subset of operation overloading restricted to subtypes.
Basically, being able to further specify the operation + as a monomorphizable quasi-method plus(u, v Number) Number for instance. plus would be using a switch case and would have to be extendable for the various relations between defined subtypes of Number... Don't know if it makes sense or if it is really possible, especially when wanting to avoid whole-program analysis.

[apparentlymart]

I am familiar with this sort of dimensional-analysis-driven programming in some high-level languages, but I don't think any general-purpose language I've used has included it as a first-class feature.

Instead, I've typically seen it implemented by starting in a language that offers operator overloading and then using a library which allows constructing quantity types which include suitable overloads to make the arithmetic operators work correctly with them while also propagating the dimensions (and sometimes also converting units).

For example:

• uom and dimensioned in Rust.
• Pint in Python.
• units in C++

Of course I don't claim that the languages I'm familiar with are the only languages worth considering, but I would consider the three languages I used for the examples above to all have some intended use-cases in common with Go. (If you are thinking of some specific other languages that do have dimensions and quantities as first-class language primitives rather than as libraries, I'd love to learn about them!)

Assuming that it were valuable to model dimensions and quantities in Go, might it be more appropriate to follow the lead of these other languages and implement operator overloading as the language-level primitive, and then leave it to libraries to deal with the specific domain of engineering and scientific applications that would benefit most from dimensions and quantities?

[ianlancetaylor]

The proposal here is not for operator overloading. It is to extend the type system to permit certain type combinations that are currently not permitted. Right now, the language does not permit dividing a variable of type distance by a variable of type time. With this proposal, it would permit dividing variables of those types, and the result would be type velocity.