6 ms·

Physics has a simple form of types, namely units. Checking units at the end of solving a problem was emphasized by every physics professor I ever had. As for d

by c-cube 3y ago

Physics has a simple form of types, namely units. Checking units at the end of solving a problem was emphasized by every physics professor I ever had. As for dependent types, they're only one of the ways to express mathematical properties of programs. Check out what Ada/spark does for example. A layer of logic on top of a program doesn't have to be embedded in the types (and if your language is imperative you probably don't want that anyway).

tsimionescu 3y ago
Measurement units are not types. They are conceptually similar, but the way they are used is actually entirely different. You can encode units into types, but it gets ugly fast once you do anything more complex than addition and multiplication, so no one does it actually. You won't find any matrix library that uses types to encode the measurement units of every element of a matrix the way you would in a regular physics computation. The way measurement units are normally used is essentially like special dimensionless constants that algebraic operations except +/- work on normally. So, you can multiply measurement units, you can divide them, a measurement unit divided by itself equals 1, you can raise a measurement unit to a power etc.
- malcolmgreaves 3y ago
  I agree that units aren't types. However, I think there's validity to thinking about concepts such as acceleration vs. speed vs. mass etc. as distinct types. Each of those can be specified with different units from different systems of measurement. Some of those are compatible with one another, given some transformations. E.g. for speed, one can convert X m/s into MPH: different units, but same type. However, mass is incompatible with acceleration: there's no possible valid transformation for Y grams into m/^2. If I was writing a program, I would like the language to prevent me from putting in a mass value into a place where I need a velocity. If I was writing a physics "proof," it would similarly be invalid to intermix values from these two distinct concepts.
  - tsimionescu 3y ago
    I agree that types are a decent way of representing measurement units for many common use cases. But I think the difference between the two is more fundamental. It's true of course that you can't transform a mass into a speed. However, the interesting thing is that you can multiply 5kg by 10 meters/second and get 50m×kg/s, and this is a meaningful operation (in this case, you get a momentum). You can then divide this by 5s and get 10m×kg/s² which is still meaningful (a change in momentum). Even more, you can now divide this by 5kg/s (a change in mass), and get 2m/s (speed). The way multiplication and division work with measurement units, you can't easily define them as functions that take the measurement units of their parameters as types, since you'd constantly get new types. E.g. the type of `x = foldl (×) listOfMeterQuantties` would be `meter^len(listOfMeterQuantties)`. You could do this in a dependently-typed language of course, but it would be quite unnatural I think. Essentially, the way you'd probably represent all this is to have a single type family that has a numeric parameter for every measurement unit you want to be able to represent. It would be something like PhysicalQuantity<X, Y, Z, W> == 1 m^X s^Y kg^Z k^W. + and - would be defined on pairs of PhysicalQuantity<X, Y, Z, W> and PhysicalQuantity<X, Y, Z, W>. × and / would be defined on pairs of PhysicalQuantity<X1, Y1, Z1, W1> and PhysicalQuantity<X2, Y2, Z2, W2> and they would produce PhysicalQuantity<X1+X2, Y1+Y2, Z1+Z2, W1+W2> (or - for division). How usable this would then be (i.e. the type of "1m" would be PhysicalQuantity<1,0,0,0>) is debatable. But even if it would be good enough, I think it is quite apparent that the type representation is nowhere near intuitive or direct.

by c-cube 3y ago

tsimionescu 3y ago

Measurement units are not types. They are conceptually similar, but the way they are used is actually entirely different. You can encode units into types, but it gets ugly fast once you do anything more complex than addition and multiplication, so no one does it actually. You won't find any matrix library that uses types to encode the measurement units of every element of a matrix the way you would in a regular physics computation. The way measurement units are normally used is essentially like special dimensionless constants that algebraic operations except +/- work on normally. So, you can multiply measurement units, you can divide them, a measurement unit divided by itself equals 1, you can raise a measurement unit to a power etc.

malcolmgreaves 3y ago
I agree that units aren't types. However, I think there's validity to thinking about concepts such as acceleration vs. speed vs. mass etc. as distinct types. Each of those can be specified with different units from different systems of measurement. Some of those are compatible with one another, given some transformations. E.g. for speed, one can convert X m/s into MPH: different units, but same type. However, mass is incompatible with acceleration: there's no possible valid transformation for Y grams into m/^2. If I was writing a program, I would like the language to prevent me from putting in a mass value into a place where I need a velocity. If I was writing a physics "proof," it would similarly be invalid to intermix values from these two distinct concepts.
- tsimionescu 3y ago
  I agree that types are a decent way of representing measurement units for many common use cases. But I think the difference between the two is more fundamental. It's true of course that you can't transform a mass into a speed. However, the interesting thing is that you can multiply 5kg by 10 meters/second and get 50m×kg/s, and this is a meaningful operation (in this case, you get a momentum). You can then divide this by 5s and get 10m×kg/s² which is still meaningful (a change in momentum). Even more, you can now divide this by 5kg/s (a change in mass), and get 2m/s (speed). The way multiplication and division work with measurement units, you can't easily define them as functions that take the measurement units of their parameters as types, since you'd constantly get new types. E.g. the type of `x = foldl (×) listOfMeterQuantties` would be `meter^len(listOfMeterQuantties)`. You could do this in a dependently-typed language of course, but it would be quite unnatural I think. Essentially, the way you'd probably represent all this is to have a single type family that has a numeric parameter for every measurement unit you want to be able to represent. It would be something like PhysicalQuantity<X, Y, Z, W> == 1 m^X s^Y kg^Z k^W. + and - would be defined on pairs of PhysicalQuantity<X, Y, Z, W> and PhysicalQuantity<X, Y, Z, W>. × and / would be defined on pairs of PhysicalQuantity<X1, Y1, Z1, W1> and PhysicalQuantity<X2, Y2, Z2, W2> and they would produce PhysicalQuantity<X1+X2, Y1+Y2, Z1+Z2, W1+W2> (or - for division). How usable this would then be (i.e. the type of "1m" would be PhysicalQuantity<1,0,0,0>) is debatable. But even if it would be good enough, I think it is quite apparent that the type representation is nowhere near intuitive or direct.