Random question for the type experts out there: is there any language that lets me track the units of my numeric variables? For instance, something like this:
float<km> drop(float<m> x0, float<s> duration) {
float<m> x = x0;
float<s> t = 0;
float<m/s> v = 0;
float<m/s^2> g = -10;
float<s> dt = 0.01;
while (t < duration) {
v += g*dt;
x += v*dt;
t += dt;
}
return x * (1<km>/1000<m>); // abbrev for a cast: (float<km/m>).001
}
Then I want the compiler to check that I'm not mixing up my units. It seems like this would be really useful, but I've never seen it before.
Haskell has a few libraries to do this. I particularly like unittyped[1], which not only keeps track of units but also converts among compatible ones automatically. So 1 meter + 1 inch would typecheck and be converted automatically, but 1 meter + 1 second would give you a type error.
The wiki page[2] has a bunch of examples, which I find pretty compelling. The one problem is that error messages are ugly, but they're ugly in a consistent way. You can just ignore the ugliness as unnecessary noise.
*Main> (1 meter / second) * 5 second
5.0 m/s⋅s
*Main> 2 meter + (1 meter / second) * 5 second
7.0 m
One cute thing is that prefixes like "kilo" are just functions, letting you write things like:
Haskell is really good at dealing with numeric types in general. For example, it's quite easy for a library to define its own types, which then behave just like built-in ones including nice syntax. Unittyped follows this philosophy, letting you use units with things that aren't floats, like rational numbers, meaning you don't have to lose precision.
*Main> (1 % 2) . meter `as` foot
625 % 381 ft
It's a really slick design and manages to give you safety as well as additional expressivity (since units get converted automatically).
I'm not sure why, but your examples aren't working with me...
1 *| meter |+| 35 *| centi meter
1.35 m
works, but
1 meter
fails with
<interactive>:42:1:
No instance for (Num (Value LengthDimension (U Meter) f0 -> t0))
arising from the literal `1'
Possible fix:
add an instance declaration for
(Num (Value LengthDimension (U Meter) f0 -> t0))
In the expression: 1
In the expression: 1 meter
In an equation for `it': it = 1 meter
<interactive>:42:3:
No instance for (Fractional f0) arising from a use of `meter'
The type variable `f0' is ambiguous
Possible fix: add a type signature that fixes these type variable(s)
Note: there are several potential instances:
instance Fractional Double -- Defined in `GHC.Float'
instance Fractional Float -- Defined in `GHC.Float'
instance Integral a => Fractional (GHC.Real.Ratio a)
-- Defined in `GHC.Real'
...plus four others
In the first argument of `1', namely `meter'
In the expression: 1 meter
In an equation for `it': it = 1 meter
EDIT: you may also want to start ghci with the "-XNoImplicitPrelude" flag, or explicitly disambiguate operations such as "*" with "UnitTyped.NoPrelude.*" or "Prelude.*"
Thanks, but that's not enough. The error seems due to the fact that `meter` is passed as an argument to `1` which is not a function, and indeed I don't see how that could be valid haskell code (unless there's some language flag I should enable, but unfortunately the wiki/docs of unittyped doesn't seem to be comprehensive enough)
Weird, it is enough on my machine (running ghc 7.6.3, unittyped 0.1), but unittyped does seem to use a lot of language extensions internally, it is seems possible that it would behave weirdly on different versions.
To answer the question of how it is possible, we can start by looking at the types. ":t" is a ghci command to show the type of an expression:
ghci> :t 1
1 :: Num a => a
This indicates that "1" can be any type that implements the "Num" typeclass.
Next, we want to determine what type "1" takes in the expression "1 meter". We can do this with:
ghci> let a=1; b=a meter
ghci> :t a
a :: UnitTyped.Value Double LengthDimension Meter
-> UnitTyped.Value
Double
('UnitTyped.UnitCons
* Length ('UnitTyped.Pos 'UnitTyped.One) 'UnitTyped.UnitNil)
Meter
We can see that, in the expression "1 meter", "1" is actually a function. Looking at the source code [1], it seems like this is accomplished in a relativly hacky manner:
instance (Fractional f, Convertable a b, t ~ Value f a b) => (Prelude.Num (Value f a b -> t)) where
fromInteger i x = Prelude.fromInteger i . x
(+) = error "This should not happen"
(*) = error "This should not happen"
abs = error "This should not happen"
signum = error "This should not happen"
This works because the "+" being defined here is Prelude.+, not UnitTyped.NoPrelude.+ (which is defined seperatly).
and I cannot see any instance of Num defined anywhere inside unittyped's src
PS: ok, since I wanted to see exactly what was the problem with unittyped compiling under ghc7.8 I cloned the sources, but I forgot to checkout the actual release... thus running directly from tip was the cause
Installing it directly from hackage solved it, it's embarrassing how I was stunned by this in hindsight
pjungwir's example code is actually really close to what you'd see in F#. In F# you'd typically write it in a more functional way with say a recursive inner function but I'll leave it imperative for clarity's sake:
[<Measure>] type s
[<Measure>] type m
[<Measure>] type km
let mtokm (x:float<m>) = x * 1.<km>/1000.<m>
//the types of g and ground are inferred
let drop g ground (x0:float<m>) =
let mutable x = x0 //type inferred here
let mutable t = 0.0<s>
let mutable v = 0.0<m/s>
let dt = 0.01<s>
while x >= ground do
v <- v + g*dt
x <- x + v*dt
t <- t + dt
t
> drop -10.0<m/s^2> 0.<m> 50.<m>
val it : float<s> = 3.16
Adding to all the other answers, here is what Haxe can do:
class Metric {
static function main() {
var coinRadius:Millimeters = 12;
var myHeight:Centimeters = 180;
var raceLength:Meters = 200;
var commuteDistance:Kilometers = 23;
diff( coinRadius, myHeight ); // 1.788 meters
diff( raceLength, commuteDistance ); // 22800 meters
sum( commuteDistance, coinRadius ); // 23000.012 meters
}
static function diff( a:Meters, b:Meters ) {
var d = Math.abs( a-b );
trace( '$d meters' );
}
static function sum( a:Meters, b:Meters ) {
var s = Math.abs( a+b );
trace( '$s meters' );
}
}
And the best part is, at runtime those are all floats. Take a look at the compiled JS code:
(function () { "use strict";
var Metric = function() { };
Metric.main = function() {
var coinRadius = 12;
var myHeight = 180;
var raceLength = 200;
var commuteDistance = 23;
Metric.diff(coinRadius / 1000,myHeight / 100);
Metric.diff(raceLength,commuteDistance * 1000);
Metric.sum(commuteDistance * 1000,coinRadius / 1000);
};
Metric.diff = function(a,b) {
var d = Math.abs(a - b);
console.log("" + d + " meters");
};
Metric.sum = function(a,b) {
var s = Math.abs(a + b);
console.log("" + s + " meters");
};
Metric.main();
})();
The compiler takes care of all the conversions for you. To see the complete compileable example, including my type definitions for each unit, take a look at this gist: https://gist.github.com/jasononeil/b6b1845824f45f5d19df
In theory you can do that in any language that allows you to override operators. It's definitely being done in Rust. For instance you sleep for `Duration::milliseconds(10)`.
Jav^H^H^H errr... I mean, Xtend [1] :). It does this through a mechanism called "extension methods" [2]. Kotlin has something similar called "extension functions", so I'm guessing it should be possible with it too.
