unit.cpp

// g++ % -std=c++0x
#include <iostream>
using namespace std;

template<int m, int s, int kg>
struct unit
{
    double value;

    unit():value(0){}
    unit(double _value):value(_value){}
};

template<int m, int s, int kg>
ostream & operator<<(ostream & os, const unit<m, s, kg>& unit)
{
    return os << unit.value << " :: m^" << m << " s^" << s << " kg^" << kg;
}

template<int m, int s, int kg>
unit<m, s, kg> operator+(unit<m, s, kg> a, unit<m, s, kg> b)
{
    return a.value + b.value;
}

template<int m, int s, int kg>
unit<m, s, kg> operator-(unit<m, s, kg> a, unit<m, s, kg> b)
{
    return a.value - b.value;
}

template<int m, int s, int kg>
unit<m, s, kg> operator+(unit<m, s, kg> a)
{
    return a.value;
}

template<int m, int s, int kg>
unit<m, s, kg> operator-(unit<m, s, kg> a)
{
    return -a.value;
}

template<int m1, int s1, int kg1, int m2, int s2, int kg2>
unit<m1+m2, s1+s2, kg1+kg2>operator*(unit<m1, s1, kg1> a, unit<m2, s2, kg2> b)
{
    return a.value * b.value;
}

template<int m1, int s1, int kg1, int m2, int s2, int kg2>
unit<m1-m2, s1-s2, kg1-kg2>operator/(unit<m1, s1, kg1> a, unit<m2, s2, kg2> b)
{
    return a.value / b.value;
}

template<int m, int s, int kg>
unit<m, s, kg> operator*(double v, unit<m, s, kg> a)
{
    return v * a.value;
}

template<int m, int s, int kg>
unit<m, s, kg> operator*(unit<m, s, kg> a, double v)
{
    return a.value * v;
}

template<int m, int s, int kg>
unit<-m, -s, -kg> operator/(double v, unit<m, s, kg> a)
{
    return v / a.value;
}

template<int m, int s, int kg>
unit<-m, -s, -kg> operator/(unit<m, s, kg> a, double v)
{
    return a.value / v;
}

const unit<1, 0, 0> m = unit<1, 0, 0>(1); // meter
const unit<0, 1, 0> s = unit<0, 1, 0>(1); // second
const unit<0, 0, 1> kg = unit<0, 0, 1>(1); //kilogram
const unit<1, -2, 1> N = unit<1, -2, 1>(1); // Newton
const unit<2, -2, 1> J = unit<2, -2, 1>(1);

int main(int argc, char const* argv[])
{
    auto d = 2 * m;     // 2 meters away
    cout << "d = " << d << endl;
    auto v = 0.1 * m/s; // 0.1 m/s
    cout << "v = " << v << endl;
    auto t = d / v;     // ok
    cout << "t = " << t << endl;
    auto t1 = 10 * s;   // ok
    cout << "t1 = " << t1 << endl;
    auto t2 = t1 + t;   // ok
    cout << "t2 = " << t2 << endl;
    //auto x = d + v;   // compile error
    return 0;
}

Unit.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Unit where

import qualified Prelude as P
import Prelude hiding ((+), (*), (/), (-), Int, pi)

data Int = Zero | Succ Int | Pred Int

type family   Plus (a::Int) (b::Int) :: Int
type instance Plus a Zero     = a
type instance Plus Zero b     = b
type instance Plus (Succ a) (Pred b) = Plus a b
type instance Plus (Pred a) (Succ b) = Plus a b
type instance Plus (Succ a) (Succ b) = Succ (Succ (Plus a b))
type instance Plus (Pred a) (Pred b) = Pred (Pred (Plus a b))

type family   Negate (a::Int) :: Int
type instance Negate Zero  = Zero
type instance Negate (Succ a) = Pred (Negate a)
type instance Negate (Pred a) = Succ (Negate a)

data Unit :: Int -> Int -> Int -> * where
    U :: Double -> Unit m s kg

data Proxy a = Proxy

class IntRep (n :: Int) where
    natToInt :: Proxy (n::Int) -> Integer

instance IntRep Zero where
    natToInt _ = 0
instance (IntRep n) => IntRep (Succ n) where
    natToInt _ = 1 P.+ (natToInt (Proxy :: Proxy n))
instance (IntRep n) => IntRep (Pred n) where
    natToInt _ = (natToInt (Proxy :: Proxy n)) P.- 1

instance (IntRep m, IntRep s, IntRep kg) => Show (Unit m s kg) where
    show (U a) = unwords [show a, "m^" ++ u0, "s^" ++ u1, "kg^" ++ u2]
        where u0 = show $ natToInt (Proxy :: Proxy m)
              u1 = show $ natToInt (Proxy :: Proxy s)
              u2 = show $ natToInt (Proxy :: Proxy kg)

(+) :: Unit m s kg -> Unit m s kg -> Unit m s kg
(U a) + (U b) = U (a P.+ b)

(-) :: Unit m s kg -> Unit m s kg -> Unit m s kg
(U a) - (U b) = U (a P.- b)

(*) :: Unit m1 s1 kg1 -> Unit m2 s2 kg2 -> Unit (Plus m1 m2) (Plus s1 s2) (Plus kg1 kg2)
(U a) * (U b) = U (a P.* b)

(/) :: Unit m1 s1 kg1 -> Unit m2 s2 kg2 -> Unit (Plus m1 (Negate m2)) (Plus s1 (Negate s2)) (Plus kg1 (Negate kg2))
(U a) / (U b) = U (a P./ b)

{-| some constants |-}
pi, e :: Unit Zero Zero Zero
pi = U 3.14
e = U 2.72

c :: Double -> Unit Zero Zero Zero
c = U

{-| some units |-}
-- length unit
m :: Unit (Succ Zero) Zero Zero
m = U 1

-- time unit
s :: Unit Zero (Succ Zero) Zero
s = U 1

-- mass unit
kg :: Unit Zero Zero (Succ Zero)
kg = U 1

main :: IO ()
main = do
    let distance  = c 100  * m -- 100 meters away
    let startTime = c 2000 * s -- start at 2000 second
    let endTime   = c 3000 * s -- end at 3000 sencond
    let deltaTime = endTime - startTime -- cost 1000 senconds
    let velocity  = distance / deltaTime -- 0.1 m/s
    -- let foo = velocity + distance -- error
    print $ velocity