Installing it with cabal on Windows proved impossible. A SuSe VM on VirtualBox couldn’t cut it either. Actually installing MinGW, which was the recommended way on WIndows, didn’t give me Idris, either. But still, I wanted it. And, sure enough, as Paulo Coelho predicted, the Universe conspired to help me get it, and one can now download precompiled binaries for Windows!
Now that I had a real dependently-typed programming language, with realistic-looking tutorials and documentation, I thought it was a great excuse to implement type-safe dimensional calculations in it. The resulting code is so terse, compared to the Scala example, it almost feels like cheating. In the beginning, is the dependent type itself.
data DimVal : Int -> Int -> Int -> Int -> Type where
DV : (m:Int) -> (k:Int) -> (s:Int) -> (a:Int) -> (v:Float) -> DimVal m k s a
Please compare it with the Scala (and C++) equivalent. The similarities are obvious but this version completely blends the two levels together. DimVal is a type constructor indexed by four integers and DV is its sole constructor.
Calculating with these types needs the usual arithmetic operations. Unfortunately, trying to overload the operators did not work for me, as they were imported already by the Num class in the Prelude.
||| The Num class defines basic numerical arithmetic. class Num a where (+) : a -> a -> a (-) : a -> a -> a (*) : a -> a -> a ||| Absolute value abs : a -> a ||| Conversion from Integer. fromInteger : Integer -> a
DimVal cannot be made an instance of Num, because types need to be closed under all three operations, and this cannot be the case, since the point is to represent each dimension vector by a different type. So I faked four appropriate operators.
infixr 10 /+/ (/+/) : DimVal m k s a -> DimVal m k s a -> DimVal m k s a (DV m k s a v1) /+/ (DV m k s a v2) = DV m k s a (v1+v2) infixr 10 /-/ (/-/) : DimVal m k s a -> DimVal m k s a -> DimVal m k s a (DV m k s a v1) /-/ (DV m k s a v2) = DV m k s a (v1-v2) infixr 20 /*/ (/*/) : DimVal m1 k1 s1 a1 -> DimVal m2 k2 s2 a2 -> DimVal (m1+m2) (k1+k2) (s1+s2) (a1+a2) (DV m1 k1 s1 a1 v1) /*/ (DV m2 k2 s2 a2 v2) = DV (m1+m2) (k1+k2) (s1+s2) (a1+a2) (v1*v2) infixr 20 /// (///) : DimVal m1 k1 s1 a1 -> DimVal m2 k2 s2 a2 -> DimVal (m1-m2) (k1-k2) (s1-s2) (a1-a2) (DV m1 k1 s1 a1 v1) /// (DV m2 k2 s2 a2 v2) = DV (m1-m2) (k1-k2) (s1-s2) (a1-a2) (v1/v2)
Next up, printing dimensioned values. For this, I used an intermediate Dimension type.
data Dimension : Type where
Dim : (m:Int) -> (k:Int) -> (s:Int) -> (a:Int) -> Dimension
unitToStr : Dimension -> String
unitToStr (Dim m k s a) =
case (m, k, s, a) of
(0,0,1,1) => "C"
(1,1,-2,0) => "N"
(0,0,-1,0) => "Hz"
(-1,1,-2,0) => "Pa"
(2,1,-3,-2) => "ohm"
(2,1,-3,-1) => "V"
(-2,-1,3,2) => "S"
(2,1,-3,0) => "W"
(2,1,-2,0) => "J"
(-2,-1,4,2) => "F"
(2,1,-2,-2) => "H"
(2,1,-2,-1) => "Wb"
(0,1,-2,-1) => "T"
_ => (if m /= 0 then "m" ++ (if m /= 1 then (show m) else "") else "") ++
(if (m /= 0) && (k /= 0) then "." else "") ++
(if k /= 0 then "Kg" ++ (if k /= 1 then (show k) else "") else "") ++
(if (abs(m) + abs(k)) /= 0 && s /= 0 then "." else "") ++
(if s /= 0 then "s" ++ (if s /= 1 then (show s) else "") else "") ++
(if (abs(m) + abs(k) + abs(s)) /= 0 && a /= 0 then "." else "") ++
(if a /= 0 then "A" ++ (if a /= 1 then (show a) else "") else "")
toStr : DimVal m k s a -> String
toStr (DV m k s a v) = (show v) ++ " " ++ (unitToStr (Dim m k s a))
instance Show (DimVal m k s a) where
show dv = toStr dv
The Num class was out of the question, but Eq and Ord are readily instantiable.
dimValEq : DimVal m k s a -> DimVal m k s a -> Bool
dimValEq (DV m k s a v1) (DV m k s a v2) = (v1==v2)
dimValComp : DimVal m k s a -> DimVal m k s a -> Ordering
dimValComp (DV m k s a v1) (DV m k s a v2) = compare v1 v2
instance Eq (DimVal m k s a) where
dv1 == dv2 = dimValEq dv1 dv2
instance Ord (DimVal m k s a) where
compare dv1 dv2 = dimValComp dv1 dv2
Idris has syntax support for creating DSLs so, a native Idris speaker would probably go on to create a better DSL for creating values, arithmetic etc. I’ll just show how type-safe calculations can naturally be encoded in plain Idris. I did not go into the trouble of defining all named physical types but I guess you see how this can be done without any problem.
Mass : Type
Mass = DimVal 1 0 0 0
mass : Float -> Mass
mass = DV 1 0 0 0
main : IO ()
main =
let x = DV 1 1 (-2) 0 14.5 in
let y = DV 1 1 (-2) 0 15.5 in
let z = DV 2 2 0 0 15.5 in
let xpy = x /+/ y in
let xmy = x /-/ y in
let xtz = x /*/ z in
let xdz = x /// z in
let m : Mass = mass 12.6 in
do
putStrLn (show m)
putStrLn (show x)
putStrLn (show y)
putStrLn (show z)
putStrLn (show (x == x))
putStrLn (show (x == y))
-- putStrLn ((show (y == z))) -- Doesn't even compile!
putStrLn (show (x < y))
-- putStrLn ((show (z < y))) -- Doesn't even compile!
putStrLn (show xtz)
putStrLn (show xdz)
It does feel like cheating, doesn’t it? Calculating with physical types is actually done at two levels: the values themselves are operated upon as if they were dimensionless, while the dimensions are vectors representing exponents and are operated upon using exponent arithmetic. Idris handles both levels in the same way, very naturally. It is said that all high-level languages are equivalent in the computations they can express, but their compilers are certainly not equivalent.
dsouflis 