3 ms·
> Personally, type errors haven't been the kind of errors that haunt my dreams. The point of strongly-typed systems is that you can represent your constraints
by lallysingh 10y ago
> Personally, type errors haven't been the kind of errors that haunt my dreams.
The point of strongly-typed systems is that you can represent your constraints as types. This takes extra thinking and work, but gives you almost almost unlimited expressive power (ref: agda).
Simple example: meters and feet as different numerical types. When you multiply them, you get a silly unit (foot-meters) that doesn't fit with whatever you wanted (meters^2), and thusly fails compilation.
- xapata 10y agoI haven't met anyone other than Haskellians that would create separate types for meters and feet. I also wonder when you would make that distinction in the lifecycle of your application. I suspect not until you first encounter the bug of accidentally mixing units. If so, we'd be solving the problem at the same time, just using different techniques.
- jdmichal 10y agoF# allows sub-typing of numerics with a unit of measure. https://docs.microsoft.com/en-us/dotnet/articles/fsharp/language-reference/units-of-measure https://docs.microsoft.com/en-us/dotnet/articles/fsharp/lang...
- xapata 10y agoThat is a nifty syntax.
- lallysingh 10y agoHi! nice to meet you. I've used this in C++ to great effect. It's also in boost. I put it in anywhere I expect math on units that are easily screwed up. I don't retrofit them in. It's easy enough to have a meters_t typedef from the beginning. It also serves as documentation for the code.
- Koshkin 10y agoAn even simpler example would be the fact that it makes no sense to add values expressed in different units (without an appropriate type conversion).