3 ms·

Agreed -- it was difficult to get motivated to read deeply into the article when I was wondering why there is more to say than "values in physics should be stro

by bo1024 14y ago

Agreed -- it was difficult to get motivated to read deeply into the article when I was wondering why there is more to say than "values in physics should be strongly typed".

evincarofautumn 14y ago
The system itself is interesting, though. In the simple case, a dimension associated with a value is a product of nonzero integer powers of units of different kinds—in the type theory sense—which may be the empty set for dimensionless values. Different units of the same kind could define implicit conversions—for example, metres and yards are both of kind “length”. Each kind would be associated with an underlying type or interface—for example, length only makes sense for scalar values, such as integers and floats. F# units of measure are an implementation of this special case. You could generalise it, though, to associate arbitrary static metadata with a type. That seems potentially useful, and like something someone should do.
mturmon 14y ago
But dimensional analysis has an automatic method of transforming objects of one type to another. When you talk about "strongly typed", I think you mean the programming concept, in which there is no such automatic method.
- tikhonj 14y ago
  Hmm, I don't see any reason why a type system couldn't have automatic conversions like this. I remember reading about a system recently where certain typing rules would actually insert runtime code. In this particular case, it was a type system for C that would insert runtime asserts if it couldn't prove things statically, but this approach would certainly work for converting between units as well. In fact, you can even bludgeon an existing type system like Haskell's--a language well-known for not being dependently typed--into doing automatic conversions with units. This is exactly what the unittyped package[1] does, in fact. It's actually very cool. [1]: http://hackage.haskell.org/package/unittyped-0.1 http://hackage.haskell.org/package/unittyped-0.1
- evincarofautumn 14y ago
  Many type systems do include a notion of automatic (implicit) conversion between types. This doesn’t preclude strong typing in the usual sense; then again, “strong” is kind of a soft term, which isn’t really used in type theory.

by bo1024 14y ago

Agreed -- it was difficult to get motivated to read deeply into the article when I was wondering why there is more to say than "values in physics should be strongly typed".

evincarofautumn 14y ago

The system itself is interesting, though. In the simple case, a dimension associated with a value is a product of nonzero integer powers of units of different kinds—in the type theory sense—which may be the empty set for dimensionless values. Different units of the same kind could define implicit conversions—for example, metres and yards are both of kind “length”. Each kind would be associated with an underlying type or interface—for example, length only makes sense for scalar values, such as integers and floats. F# units of measure are an implementation of this special case. You could generalise it, though, to associate arbitrary static metadata with a type. That seems potentially useful, and like something someone should do.

mturmon 14y ago

But dimensional analysis has an automatic method of transforming objects of one type to another. When you talk about "strongly typed", I think you mean the programming concept, in which there is no such automatic method.

tikhonj 14y ago
Hmm, I don't see any reason why a type system couldn't have automatic conversions like this. I remember reading about a system recently where certain typing rules would actually insert runtime code. In this particular case, it was a type system for C that would insert runtime asserts if it couldn't prove things statically, but this approach would certainly work for converting between units as well. In fact, you can even bludgeon an existing type system like Haskell's--a language well-known for not being dependently typed--into doing automatic conversions with units. This is exactly what the unittyped package[1] does, in fact. It's actually very cool. [1]: http://hackage.haskell.org/package/unittyped-0.1 http://hackage.haskell.org/package/unittyped-0.1
evincarofautumn 14y ago
Many type systems do include a notion of automatic (implicit) conversion between types. This doesn’t preclude strong typing in the usual sense; then again, “strong” is kind of a soft term, which isn’t really used in type theory.