From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id B80CC7EFCD for ; Thu, 16 Oct 2014 19:35:38 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of mario.alvarez739@gmail.com) identity=pra; client-ip=209.85.223.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mario.alvarez739@gmail.com"; x-sender="mario.alvarez739@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of mario.alvarez739@gmail.com designates 209.85.223.169 as permitted sender) identity=mailfrom; client-ip=209.85.223.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mario.alvarez739@gmail.com"; x-sender="mario.alvarez739@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ie0-f169.google.com) identity=helo; client-ip=209.85.223.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mario.alvarez739@gmail.com"; x-sender="postmaster@mail-ie0-f169.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AuMEAFgBQFTRVd+pgGdsb2JhbABbg2FND4MCxzCBboZ5VAKBEAcWAREBARQoLoQDAQECAQESER0BGx0BAwELBgMCCy0KAgIhAQERAQUBDg4GEyKIBwEDCQgNmQKQMW6LMIFygxCIeAoZJw1nhVsBAQEBBgEBAQEBARYBBQ6OC4IwBAeCd4FUBYUVik6GYoUBghGPRoRkGCmFKjsvAQEBgkcBAQE X-IPAS-Result: AuMEAFgBQFTRVd+pgGdsb2JhbABbg2FND4MCxzCBboZ5VAKBEAcWAREBARQoLoQDAQECAQESER0BGx0BAwELBgMCCy0KAgIhAQERAQUBDg4GEyKIBwEDCQgNmQKQMW6LMIFygxCIeAoZJw1nhVsBAQEBBgEBAQEBARYBBQ6OC4IwBAeCd4FUBYUVik6GYoUBghGPRoRkGCmFKjsvAQEBgkcBAQE X-IronPort-AV: E=Sophos;i="5.04,733,1406584800"; d="scan'208";a="83521845" Received: from mail-ie0-f169.google.com ([209.85.223.169]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 16 Oct 2014 19:35:33 +0200 Received: by mail-ie0-f169.google.com with SMTP id tp5so3960302ieb.0 for ; Thu, 16 Oct 2014 10:35:32 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=DXplIyKivHMf4/nz7Q3p8ljFOW/AHMMA5Y4hoZLMWZM=; b=hBlmrqCI6SE9Setx/mJ1k1fbhphryAWtsS5qpoAyOKCpY8G52Q0rwcoaf1Gp897iH+ 2i2QaZqmczXPil8r2kRRWfWU5b6XH4XDLzUMwutpeUMazgXFgCc3eT+eIC1JwDXkUhK4 HailTT3tQcWEsKOwwSgRGilUjltap3dglEyTPB0MtRBS1x6f7wFQN16AobBzDQ7xQxcm keVXy2xhgkiRCmw5skKx3NJLcVcdvQhJ9kcFM7OyjkkPA3orks1oint1NKJXJos0JWyr QZsWSnCusfoECvlr9Cqvm5EnX50rhKiS5UHHHX1cPMDu+zW6Pc/mTxjxSLgUkrbf2Ogd kR3w== MIME-Version: 1.0 X-Received: by 10.50.61.226 with SMTP id t2mr6694084igr.27.1413480932254; Thu, 16 Oct 2014 10:35:32 -0700 (PDT) Received: by 10.64.147.101 with HTTP; Thu, 16 Oct 2014 10:35:32 -0700 (PDT) In-Reply-To: References: Date: Thu, 16 Oct 2014 19:35:32 +0200 Message-ID: From: Mario Alvarez Picallo To: Shayne Fletcher Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=047d7bdc0c84dd2a8a05058dac36 Subject: Re: [Caml-list] Dimensional Analysis question --047d7bdc0c84dd2a8a05058dac36 Content-Type: text/plain; charset=UTF-8 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 > #include > #include > #include > #include > #include > #include > > typedef boost::mpl::vector_c mass; > typedef boost::mpl::vector_c length; > typedef boost::mpl::vector_c time; > typedef boost::mpl::vector_c charge; > typedef boost::mpl::vector_c temperature; > typedef boost::mpl::vector_c intensity; > typedef boost::mpl::vector_c angle; > typedef boost::mpl::vector_c velocity; // l/t > typedef boost::mpl::vector_c acceleration; // > l/(t2) > typedef boost::mpl::vector_c momentum; // ml/t > typedef boost::mpl::vector_c force; // > ml/(t2) > typedef boost::mpl::vector_c scalar; > > template > class quantity > { > public: > explicit quantity (T val) > : val (val) > {} > template > quantity (quantity const& other) > : val (other.value ()) { > BOOST_MPL_ASSERT( (boost::mpl::equal OtherDimensions>)); > } > T value () const { return val; } > private: > T val; > }; > > template > quantity > operator + (quantity x, quantity y ) > { > return quantity(x.value () + y.value ()); > } > > template > quantity > operator - (quantity x, quantity y ) > { > return quantity(x.value () - y.value ()); > } > > template > quantity < > T > , typename boost::mpl::transform< > D1, D2, boost::mpl::plus< > boost::mpl::placeholders::_1 > , boost::mpl::placeholders::_2> >::type > > > operator* (quantity x, quantity y) > { > typedef typename boost::mpl::transform< > D1, D2, boost::mpl::plus< > boost::mpl::placeholders::_1 > , boost::mpl::placeholders::_2> >::type D; > > return quantity (x.value () * y.value ()); > } > > template > quantity < > T > , typename boost::mpl::transform< > D1, D2, boost::mpl::minus< > boost::mpl::placeholders::_1 > , boost::mpl::placeholders::_2> >::type > > > operator/ (quantity x, quantity y) > { > typedef typename boost::mpl::transform< > D1, D2, boost::mpl::minus< > boost::mpl::placeholders::_1 > , boost::mpl::placeholders::_2> >::type D; > > return quantity (x.value () / y.value ()); > } > > // -- test > > #include > #include > #include > > int main () > { > quantity m (5.0f); > quantity a(9.8f); > quantity f = m * a; > quantity m2 = f / a; > > assert ((std::abs ((m2 - m).value ())) <= > std::numeric_limits::epsilon ()); > > return 0; > } > > --047d7bdc0c84dd2a8a05058dac36 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Hello Shayne,

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

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

=
It seems to be solid enough to pass the tests that Octachron tried, b= ut 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 d= imensional analysis, where each part of the program can introduce its own d= imensions.

Regards,
Mario A.

On Thu, Oc= t 16, 2014 at 6:37 PM, Shayne Fletcher <shayne.fletcher.50@gmai= l.com> wrote:
Dear OCamlers,

In 1994, Barton and Nackman in the= ir book 'Scientific Engineering in
C++' [1]=C2=A0demonstrated=C2=A0= how one could encode the rules of Dimensional
Analysis [2] into the C++ typ= e system enabling compile-time checking
(no runtime-cost) of the=C2=A0plaus= ibility=C2=A0(at least up to the dimensional
correctness) of computations.<= /font>
=
In 2004, Abrahams & Gurtovy in 'C++ Template Metaprogramming&#= 39; [3]
showed the Barton Nackman technique to be elegantly implementable
u= sing compile time type sequences encoding integer constants. At the<= /div>
end of = this post, I provide a complete listing of their example
program [4].

<= /font>
= The key properties of the system (as I see it) are:
=C2=A0 - Encoding of i= ntegers as types;=C2=A0
=C2=A0 - Compile time manipulation of sequences of = these integer encodings
=C2=A0 =C2=A0 to deduce/produce new derived types.<= /font>
=
Now, it is not immediately obvious to me how to approach this problem<= /font>
= in OCaml. It irks me some that I can't immediately produce a yet more
e= legant OCaml program for this problem and leaves me feeling like C++=
has &q= uot;got something over on us" here ;)

My question therefore is: D= oes anyone have suggestions/pointers
on how to approach automatic dimension= al analysis via the OCaml type
system?=C2=A0

Best,

--=C2=A0
Shayne Fletcher
<= div class=3D"gmail_default">
[1] John J. Barton and Lee R. Nackman. Scientific= and Engineering C++:
=C2=A0 =C2=A0 an Introduction with Advanced Techniq= ues and Examples. Reading,
=C2=A0 =C2=A0 MA: Addison Wesley. ISBN 0-201-533= 93-6. 1994.

[2] Wikipedia http://en.wikipedia.org/wiki/Dimensiona= l_analysis

[3] David Abrahams and Aleksey Gurtovy C++ Template Met= aprogramming:
=C2=A0 =C2=A0 Concepts, Tools, and Techniques from Boost and = Beyond (C++ in
=C2=A0 =C2=A0 Depth Series), Addison-Wesley Professional. IS= BN:0321227255. 2004.

[4] Code listing:

=C2=A0 =C2=A0 //"c:/p= rogram files (x86)/Microsoft Visual Studio 10.0/vc/vcvarsall.bat" x64<= /font>
= =C2=A0 =C2=A0 //cl /Fedimension.exe /EHsc /I d:/boost_1_55_0 dimension.cpp<= /font>
= =C2=A0 =C2=A0=C2=A0
=C2=A0 =C2=A0 #include <boost/mpl/vector_c.hpp>
= =C2=A0 =C2=A0 #include <boost/mpl/transform.hpp>
=C2=A0 =C2=A0 #inclu= de <boost/mpl/placeholders.hpp>
=C2=A0 =C2=A0 #include <boost/mpl/= equal.hpp>
=C2=A0 =C2=A0 #include <boost/mpl/plus.hpp>
=C2=A0 =C2= =A0 #include <boost/mpl/minus.hpp>
=C2=A0 =C2=A0 #include <boost/s= tatic_assert.hpp>
=C2=A0 =C2=A0=C2=A0
=C2=A0 =C2=A0 typedef boost::mpl::= vector_c<int,1,0,0,0,0,0,0> mass;
=C2=A0 =C2=A0 typedef boost::mpl::v= ector_c<int,0,1,0,0,0,0,0> length;
=C2=A0 =C2=A0 typedef boost::mpl::= vector_c<int,0,0,1,0,0,0,0> time;
=C2=A0 =C2=A0 typedef boost::mpl::v= ector_c<int,0,0,0,1,0,0,0> charge;
=C2=A0 =C2=A0 typedef boost::mpl::= vector_c<int,0,0,0,0,1,0,0> temperature;
=C2=A0 =C2=A0 typedef boost:= :mpl::vector_c<int,0,0,0,0,0,1,0> intensity;
=C2=A0 =C2=A0 typedef = boost::mpl::vector_c<int,0,0,0,0,0,0,1> angle;
=C2=A0 =C2=A0 typedef = boost::mpl::vector_c<int,0,1,-1,0,0,0,0> velocity; =C2=A0 =C2=A0 // l= /t
=C2=A0 =C2=A0 typedef boost::mpl::vector_c<int,0,1,-2,0,0,0,0> acc= eleration; // l/(t2)
=C2=A0 =C2=A0 typedef boost::mpl::vector_c<int,1,1,= -1,0,0,0,0> momentum; =C2=A0 =C2=A0 // ml/t
=C2=A0 =C2=A0 typedef boost:= :mpl::vector_c<int,1,1,-2,0,0,0,0> force; =C2=A0 =C2=A0 =C2=A0 =C2=A0= // ml/(t2)
=C2=A0 =C2=A0 typedef boost::mpl::vector_c<int,0,0,0,0,0,0,0&= gt; scalar;
=C2=A0 =C2=A0=C2=A0
=C2=A0 =C2=A0 template <class T, class D= imensions>
=C2=A0 =C2=A0 class quantity
=C2=A0 =C2=A0 {
=C2=A0 =C2=A0 pu= blic:
=C2=A0 =C2=A0 =C2=A0 explicit quantity (T val)=C2=A0
=C2=A0 =C2=A0 = =C2=A0 =C2=A0 : val (val)
=C2=A0 =C2=A0 =C2=A0 {}
=C2=A0 =C2=A0 =C2=A0 temp= late <class OtherDimensions>
=C2=A0 =C2=A0 =C2=A0 quantity (quantity&= lt;T, OtherDimensions> const& other)
=C2=A0 =C2=A0 =C2=A0 =C2=A0 : v= al (other.value ()) {
=C2=A0 =C2=A0 =C2=A0 =C2=A0 BOOST_MPL_ASSERT( (boos= t::mpl::equal<Dimensions, OtherDimensions>));
=C2=A0 =C2=A0 =C2=A0 }=
=C2=A0 =C2=A0 =C2=A0 T value () const { return val; }
=C2=A0 =C2=A0 privat= e:
=C2=A0 =C2=A0 =C2=A0 T val;
=C2=A0 =C2=A0 };
=C2=A0 =C2=A0=C2=A0<= /div>
=C2=A0 = =C2=A0 template <class T, class D>
=C2=A0 =C2=A0 quantity<T, D>=
=C2=A0 =C2=A0 operator + (quantity<T, D> x, quantity<T, D> y )=
=C2=A0 =C2=A0 {
=C2=A0 =C2=A0 =C2=A0 return quantity<T, D>(x.value (= ) + y.value ());
=C2=A0 =C2=A0 }
<= font face=3D"tahoma, sans-serif">=C2=A0 =C2=A0=C2=A0
=C2=A0 =C2=A0 template= <class T, class D>
=C2=A0 =C2=A0 quantity<T, D>
=C2=A0 =C2=A0 = operator - (quantity<T, D> x, quantity<T, D> y )
=C2=A0 =C2=A0 = {
=C2=A0 =C2=A0=C2=A0
=C2=A0 =C2=A0 template <class T, c= lass D1, class D2>
=C2=A0 =C2=A0 quantity <
=C2=A0 =C2=A0 =C2=A0 T=
=C2=A0 =C2=A0 , typename boost::mpl::transform<
=C2=A0 =C2=A0 =C2=A0 = =C2=A0 D1, D2, boost::mpl::plus<
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 boost::mpl::placeholders::_1
=C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 , boost::mpl::placeholders::_2> >:= :type=C2=A0
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 operator* (quantity<T, D1&g= t; x, quantity <T, D2> y)
=C2=A0 =C2=A0 {
=C2=A0 =C2=A0 =C2=A0 typede= f typename boost::mpl::transform<
=C2=A0 =C2=A0 =C2=A0 =C2=A0 D1, D2, bo= ost::mpl::plus<
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 boost::mpl::placeholders::_1
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 , boost::mpl::placeholders::_2> >::type D;
= =C2=A0 =C2=A0=C2=A0
=C2=A0 =C2=A0 =C2=A0 return quantity<T, D> (x.val= ue () * y.value ());
=C2=A0 =C2=A0 }
=C2=A0 =C2=A0=C2=A0
=C2=A0 =C2=A0 temp= late <class T, class D1, class D2>
=C2=A0 =C2=A0 quantity <=
=C2=A0= =C2=A0 =C2=A0 T
=C2=A0 =C2=A0 , typename boost::mpl::transform<<= /div>
=C2=A0 = =C2=A0 =C2=A0 =C2=A0 D1, D2, boost::mpl::minus<
=C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 boost::mpl::placeholders::_1
=C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 , boost::mpl::placehol= ders::_2> >::type=C2=A0
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 operator/ (q= uantity<T, D1> x, quantity <T, D2> y)
=C2=A0 =C2=A0 {
=C2=A0 = =C2=A0 =C2=A0 typedef typename boost::mpl::transform<
=C2=A0 =C2=A0 =C2= =A0 =C2=A0 D1, D2, boost::mpl::minus<
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= =C2=A0 =C2=A0 =C2=A0 =C2=A0 boost::mpl::placeholders::_1
=C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 , boost::mpl::placeholders::_= 2> >::type D;
=C2=A0 =C2=A0=C2=A0
=C2=A0 =C2=A0 =C2=A0 return quantit= y<T, D> (x.value () / y.value ());
=C2=A0 =C2=A0 }
=C2=A0 =C2=A0=C2= =A0
=C2=A0 =C2=A0 // -- test
=C2=A0 =C2=A0=C2=A0
=C2=A0 =C2=A0 #include <= ;iostream>
=C2=A0 =C2=A0 #include <limit= s>
=C2=A0 =C2=A0 #include <cassert>
=C2=A0 =C2=A0=C2=A0
= =C2=A0 =C2=A0 int main ()
=C2=A0 =C2=A0 {
=C2=A0 =C2=A0 =C2=A0 quantity<= float, mass> m (5.0f);
=C2=A0 =C2=A0 =C2=A0 quantity<float, accelerat= ion> a(9.8f);
=C2=A0 =C2=A0 =C2=A0 quantity<float, force> f =3D m = * a;
=C2=A0 =C2=A0 =C2=A0 quantity<float, mass> m2 =3D f / a;<= /div>
=C2=A0 = =C2=A0=C2=A0
=C2=A0 =C2=A0 =C2=A0 assert ((std::abs ((m2 - m).value ())) &l= t;=3D std::numeric_limits<double>::epsilon ());
=C2=A0 =C2=A0=C2=A0
= =C2=A0 =C2=A0 =C2=A0 return 0;
=C2=A0 =C2=A0 }


--047d7bdc0c84dd2a8a05058dac36--