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;
>     }
>
>