[Caml-list] Dimensional Analysis question

[Caml-list] Dimensional Analysis question

[Shayne Fletcher]

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

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: 17886 bytes --]

Re: [Caml-list] Dimensional Analysis question

[Octachron]

[-- 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 --]

Re: [Caml-list] Dimensional Analysis question

[Mario Alvarez Picallo]

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

Hello Shayne,

I was at first convinced that this could not be done, but you can in fact
encode it (in a verbose way) with phantom types,
using a smart typelevel representation of integers (
http://www.kb.ecei.tohoku.ac.jp/ml2008/slides/lindley.pdf).

I've written a small proof of concept that seems to work just fine (but, of
course, there may be errors), that you can find
here: https://gist.github.com/m-alvarez/b1e42b7b42cbeed7d1f0

It seems to be solid enough to pass the tests that Octachron tried, but
there probably are some other corner cases for which
it breaks down. Otherwise, it would be interesting to coalesce both
representations, using Octachron's idea of row types instead
of tuples to have extensible dimensional analysis, where each part of the
program can introduce its own dimensions.

Regards,
Mario A.

On Thu, Oct 16, 2014 at 6:37 PM, Shayne Fletcher <
shayne.fletcher.50@gmail.com> wrote:

> 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: 18488 bytes --]

Re: [Caml-list] Dimensional Analysis question

[Thomas Gazagnaire]

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

You might be interested by http://akabe.github.io/slap/

Thomas

On 16 Oct 2014, at 17:37, Shayne Fletcher <shayne.fletcher.50@gmail.com> wrote:

> 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: 20288 bytes --]

Re: [Caml-list] Dimensional Analysis question

[Shayne Fletcher]

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

On Thu, Oct 16, 2014 at 12:37 PM, Shayne Fletcher <
shayne.fletcher.50@gmail.com> wrote:

> My question therefore is: Does anyone have suggestions/pointers
> on how to approach automatic dimensional analysis via the OCaml type
> system?
>

​Thanks Octachron, Mario, Thomas... Great help. I've got some study to do!

-- 
Shayne Fletcher

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

Re: [Caml-list] Dimensional Analysis question

[Octachron]

Le 10/16/14 19:35, Mario Alvarez Picallo wrote:
> Hello Shayne,
>
> I was at first convinced that this could not be done, but you can in 
> fact encode it (in a verbose way) with phantom types,
> using a smart typelevel representation of integers 
> (http://www.kb.ecei.tohoku.ac.jp/ml2008/slides/lindley.pdf).
>
> I've written a small proof of concept that seems to work just fine 
> (but, of course, there may be errors), that you can find
> here: https://gist.github.com/m-alvarez/b1e42b7b42cbeed7d1f0
>
> It seems to be solid enough to pass the tests that Octachron tried, 
> but there probably are some other corner cases for which
> it breaks down. Otherwise, it would be interesting to coalesce both 
> representations, using Octachron's idea of row types instead
> of tuples to have extensible dimensional analysis, where each part of 
> the program can introduce its own dimensions.
>
> Regards,
> Mario A.
>

I forget to add variance annotation in my test so my examples broke down 
due to the presence of monomorphic types. With the right implementation 
(i.e. Mario's),
problems appear within functions. For instance,

let f x = x* x

works only for adimensional variable (i.e f : ('a*'a) t -> ('a*'a) t ) 
which is maybe not surprising.
However, the same thing  also happens to

let f x y = (x+y)*x*y .

because the type of x and y are unified during the addition "x+y".

Regards,
Octachron.

Re: [Caml-list] Dimensional Analysis question

[Roberto Di Cosmo]

Dear Shayne,
   you might have a look at the thread answering a similar question
I asked last june on the list, here:

https://sympa.inria.fr/sympa/arc/caml-list/2014-06/msg00066.html

Notice that the very first viable experiment of a variant of CamlLight
with full dimension types (non encodings) was announced by Bruno Blanchet back in 1995
http://caml.inria.fr/pub/ml-archives/caml-list/1995/12/2c6fa7b3b2b429cf39f10b60d2230850.fr.html

--
Roberto

On Thu, Oct 16, 2014 at 12:37:19PM -0400, Shayne Fletcher wrote:
> 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;
>     }
> 

-- 
Roberto Di Cosmo
 
------------------------------------------------------------------
Professeur               En delegation a l'INRIA
PPS                      E-mail: roberto@dicosmo.org
Universite Paris Diderot WWW  : http://www.dicosmo.org
Case 7014                Tel  : ++33-(0)1-57 27 92 20
5, Rue Thomas Mann       
F-75205 Paris Cedex 13   Identica: http://identi.ca/rdicosmo
FRANCE.                  Twitter: http://twitter.com/rdicosmo
------------------------------------------------------------------
Attachments:
MIME accepted, Word deprecated
      http://www.gnu.org/philosophy/no-word-attachments.html
------------------------------------------------------------------
Office location:
 
Bureau 3020 (3rd floor)
Batiment Sophie Germain
Avenue de France
Metro Bibliotheque Francois Mitterrand, ligne 14/RER C
-----------------------------------------------------------------
GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3                        

Re: [Caml-list] Dimensional Analysis question

[David MENTRE]

Hello Thomas,

Le 16/10/2014 20:10, Thomas Gazagnaire a écrit :
> You might be interested by http://akabe.github.io/slap/

As far as I understand it, slap checks dimensions with the meaning 
*size* (of matrices, vectors). But slap does not help for checking 
*physical* dimensions (meters, seconds, m*s^-2, ...).

Best regards,
david

Re: [Caml-list] Dimensional Analysis question

[Shayne Fletcher]

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

On Thu, Oct 16, 2014 at 1:35 PM, Mario Alvarez Picallo <
mario.alvarez739@gmail.com> wrote:

> I've written a small proof of concept that seems to work just fine (but,
> of course, there may be errors), that you can find
> here: https://gist.github.com/m-alvarez/b1e42b7b42cbeed7d1f0
>

​Mario, thanks for the links and this, this is truly a beautiful little
program.


>
>
> It seems to be solid enough to pass the tests that Octachron tried, but
> there probably are some other corner cases for which
> it breaks down. Otherwise, it would be interesting to coalesce both
> representations, using Octachron's idea of row types instead
> of tuples to have extensible dimensional analysis, where each part of the
> program can introduce its own dimensions.


​Mario, Octachron, thanks again. Really helped me out. Mind blowing stuff!
:)​

-- 
Shayne Fletcher

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