Re: [Caml-list] Dimensional Analysis question

[Octachron <octa@polychoron.fr>]

[-- Attachment #1: Type: text/plain, Size: 7239 bytes --]

Hello,
As far as I know it is possible to do some kind of basic dimensional 
analysis.

The idea is to encode natural number at the type level as
0 :: 'a -> 'a
1:: 'a -> 'a succ
n :: 'a -> 'a succ .... succ  (with n succ)

In other words, we are encoding translation on natural numbers rather 
than the natural numbers themselves.
The free parameter 'a allows to type addition and substraction. We can 
then define numbers with unit as a phantom type

type 'a t = float

and for instance a meter function as

let m : float ->  < m : 'a -> 'a > t = fun x -> x

where the row type is merely used to have nice label for the type name.

Addition and substraction then preserve the phantom type
val + : 'a t -> 'a t -> 'a t

whereas  multiplication and division use the free type parameter in the 
natural encoding to perform the addition

let ( * ) : <m : 'inf -> 'mid > t -> <m: 'mid -> 'sup> t -> <m: 'inf -> 
'sup> t = *.
let (/):  < m: inf->sup > t -> <m:inf->mid> t -> <m: mid-> sup>  t = ( /. )

This solution works for basic use but falls apart in complex use due to 
the lack of second-rank polymorphism.
For instance,

      let y = m 2. * m 3.

works but

     let x = m 2. in
     let y = x * x

doe not. Even worse

let () =
     let x = m 1. in
     let y = m 2. in
     let w = x * y in
     ()

works but

let () =
     let x = m 1. in
     let y = m 2. in
     let w = x * y in
     let z = x + y in
     ()

triggers a compilation error.
And unfortunately, I am not aware of any way to avoid these quirky 
behaviors.

Regards,
octachron.

Le 10/16/14 18:37, Shayne Fletcher a écrit :
> Dear OCamlers,
>
> In 1994, Barton and Nackman in their book 'Scientific Engineering in
> C++' [1] demonstrated how one could encode the rules of Dimensional
> Analysis [2] into the C++ type system enabling compile-time checking
> (no runtime-cost) of the plausibility (at least up to the dimensional
> correctness) of computations.
>
> In 2004, Abrahams & Gurtovy in 'C++ Template Metaprogramming' [3]
> showed the Barton Nackman technique to be elegantly implementable
> using compile time type sequences encoding integer constants. At the
> end of this post, I provide a complete listing of their example
> program [4].
>
> The key properties of the system (as I see it) are:
>   - Encoding of integers as types;
>   - Compile time manipulation of sequences of these integer encodings
>     to deduce/produce new derived types.
>
> Now, it is not immediately obvious to me how to approach this problem
> in OCaml. It irks me some that I can't immediately produce a yet more
> elegant OCaml program for this problem and leaves me feeling like C++
> has "got something over on us" here ;)
>
> My question therefore is: Does anyone have suggestions/pointers
> on how to approach automatic dimensional analysis via the OCaml type
> system?
>
> Best,
>
> -- 
> Shayne Fletcher
>
> [1] John J. Barton and Lee R. Nackman. Scientific and Engineering C++:
>     an Introduction with Advanced Techniques and Examples. Reading,
>     MA: Addison Wesley. ISBN 0-201-53393-6. 1994.
>
> [2] Wikipedia http://en.wikipedia.org/wiki/Dimensional_analysis
>
> [3] David Abrahams and Aleksey Gurtovy C++ Template Metaprogramming:
>     Concepts, Tools, and Techniques from Boost and Beyond (C++ in
>     Depth Series), Addison-Wesley Professional. ISBN:0321227255. 2004.
>
> [4] Code listing:
>
>     //"c:/program files (x86)/Microsoft Visual Studio 
> 10.0/vc/vcvarsall.bat" x64
>     //cl /Fedimension.exe /EHsc /I d:/boost_1_55_0 dimension.cpp
>     #include <boost/mpl/vector_c.hpp>
>     #include <boost/mpl/transform.hpp>
>     #include <boost/mpl/placeholders.hpp>
>     #include <boost/mpl/equal.hpp>
>     #include <boost/mpl/plus.hpp>
>     #include <boost/mpl/minus.hpp>
>     #include <boost/static_assert.hpp>
>     typedef boost::mpl::vector_c<int,1,0,0,0,0,0,0> mass;
>     typedef boost::mpl::vector_c<int,0,1,0,0,0,0,0> length;
>     typedef boost::mpl::vector_c<int,0,0,1,0,0,0,0> time;
>     typedef boost::mpl::vector_c<int,0,0,0,1,0,0,0> charge;
>     typedef boost::mpl::vector_c<int,0,0,0,0,1,0,0> temperature;
>     typedef boost::mpl::vector_c<int,0,0,0,0,0,1,0> intensity;
>     typedef boost::mpl::vector_c<int,0,0,0,0,0,0,1> angle;
>     typedef boost::mpl::vector_c<int,0,1,-1,0,0,0,0> velocity;   // l/t
>     typedef boost::mpl::vector_c<int,0,1,-2,0,0,0,0> acceleration; // 
> l/(t2)
>     typedef boost::mpl::vector_c<int,1,1,-1,0,0,0,0> momentum;   // ml/t
>     typedef boost::mpl::vector_c<int,1,1,-2,0,0,0,0> force;    // ml/(t2)
>     typedef boost::mpl::vector_c<int,0,0,0,0,0,0,0> scalar;
>     template <class T, class Dimensions>
>     class quantity
>     {
>     public:
>       explicit quantity (T val)
>         : val (val)
>       {}
>       template <class OtherDimensions>
>       quantity (quantity<T, OtherDimensions> const& other)
>         : val (other.value ()) {
>         BOOST_MPL_ASSERT( (boost::mpl::equal<Dimensions, 
> OtherDimensions>));
>       }
>       T value () const { return val; }
>     private:
>       T val;
>     };
>     template <class T, class D>
>     quantity<T, D>
>     operator + (quantity<T, D> x, quantity<T, D> y )
>     {
>       return quantity<T, D>(x.value () + y.value ());
>     }
>     template <class T, class D>
>     quantity<T, D>
>     operator - (quantity<T, D> x, quantity<T, D> y )
>     {
>       return quantity<T, D>(x.value () - y.value ());
>     }
>     template <class T, class D1, class D2>
>     quantity <
>       T
>     , typename boost::mpl::transform<
>         D1, D2, boost::mpl::plus<
>                   boost::mpl::placeholders::_1
>                 , boost::mpl::placeholders::_2> >::type
>     >
>     operator* (quantity<T, D1> x, quantity <T, D2> y)
>     {
>       typedef typename boost::mpl::transform<
>         D1, D2, boost::mpl::plus<
>                   boost::mpl::placeholders::_1
>                   , boost::mpl::placeholders::_2> >::type D;
>       return quantity<T, D> (x.value () * y.value ());
>     }
>     template <class T, class D1, class D2>
>     quantity <
>       T
>     , typename boost::mpl::transform<
>         D1, D2, boost::mpl::minus<
>                   boost::mpl::placeholders::_1
>                 , boost::mpl::placeholders::_2> >::type
>     >
>     operator/ (quantity<T, D1> x, quantity <T, D2> y)
>     {
>       typedef typename boost::mpl::transform<
>         D1, D2, boost::mpl::minus<
>                   boost::mpl::placeholders::_1
>                   , boost::mpl::placeholders::_2> >::type D;
>       return quantity<T, D> (x.value () / y.value ());
>     }
>     // -- test
>     #include <iostream>
>   #include <limits>
>   #include <cassert>
>     int main ()
>     {
>       quantity<float, mass> m (5.0f);
>       quantity<float, acceleration> a(9.8f);
>       quantity<float, force> f = m * a;
>       quantity<float, mass> m2 = f / a;
>       assert ((std::abs ((m2 - m).value ())) <= 
> std::numeric_limits<double>::epsilon ());
>       return 0;
>     }
>


[-- Attachment #2: Type: text/html, Size: 26392 bytes --]