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 D0B117EFCD for ; Thu, 16 Oct 2014 18:37:42 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of shayne.fletcher.50@gmail.com) identity=pra; client-ip=209.85.192.42; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="shayne.fletcher.50@gmail.com"; x-sender="shayne.fletcher.50@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of shayne.fletcher.50@gmail.com designates 209.85.192.42 as permitted sender) identity=mailfrom; client-ip=209.85.192.42; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="shayne.fletcher.50@gmail.com"; x-sender="shayne.fletcher.50@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-qg0-f42.google.com) identity=helo; client-ip=209.85.192.42; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="shayne.fletcher.50@gmail.com"; x-sender="postmaster@mail-qg0-f42.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtgBAEvzP1TRVcAqm2dsb2JhbABbg2FcgwLHLoFuiF8HFgERAQEBAQEGCwsJFC6EGxEdARseAxIDDS0KAiQBEQEFAQ4UNYgHAQMRDZh8jRSDHW6LMIFygxCIewoZJw1nhV0BBQ6TPYFUBYUVkTCHEpQqGCmDBIJAIS+CSgEBAQ X-IPAS-Result: AtgBAEvzP1TRVcAqm2dsb2JhbABbg2FcgwLHLoFuiF8HFgERAQEBAQEGCwsJFC6EGxEdARseAxIDDS0KAiQBEQEFAQ4UNYgHAQMRDZh8jRSDHW6LMIFygxCIewoZJw1nhV0BBQ6TPYFUBYUVkTCHEpQqGCmDBIJAIS+CSgEBAQ X-IronPort-AV: E=Sophos;i="5.04,733,1406584800"; d="scan'208";a="83517157" Received: from mail-qg0-f42.google.com ([209.85.192.42]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 16 Oct 2014 18:37:41 +0200 Received: by mail-qg0-f42.google.com with SMTP id z60so2853531qgd.15 for ; Thu, 16 Oct 2014 09:37:40 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:from:date:message-id:subject:to:content-type; bh=NaeO7VgILULLJHLkrXIDVAjYPLQ7QyMbPGjj49L9N80=; b=LLv7MO6RagWLbjYXIImXdqIedcxsM7kq0IS/xMcFpY9ryUZwJKGLH2ZKBWc9FyH5u3 p4V/S5hBo1mEKPp4wCwF/k8y5TKwrdT4wny2bv8PcgkvrRzn1d4+7zifimFf+kjrlsAQ PHcW2FZf3Z8UxxFZrPSOZKtwFyexj8t8zBj650DEKOeUlH7Q5hSkbYMvsPkADmqWzVkI wv6eG6bxN58UnJ4RX5nTkOcdpw2OiDHW60lMbdH8Xx++sumAKKeKHSi68SvQwYjVK5V+ jlV1nbkZKC5LumIur0fmfA6hcW/3dnJNp5fjUh18IY8xZg/AJDpRwlPyr6khd9yt/AZd J2Lg== X-Received: by 10.140.91.73 with SMTP id y67mr3658795qgd.52.1413477460084; Thu, 16 Oct 2014 09:37:40 -0700 (PDT) MIME-Version: 1.0 Received: by 10.140.18.147 with HTTP; Thu, 16 Oct 2014 09:37:19 -0700 (PDT) From: Shayne Fletcher Date: Thu, 16 Oct 2014 12:37:19 -0400 Message-ID: To: "caml-list@inria.fr users" Content-Type: multipart/alternative; boundary=001a113b39dae814b305058cdd07 Subject: [Caml-list] Dimensional Analysis question --001a113b39dae814b305058cdd07 Content-Type: text/plain; charset=UTF-8 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)); } 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; } --001a113b39dae814b305058cdd07 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Dear OCamlers,

In 1994, Barton and Nackman in their book 'Scientific Engineering in=
C++' [1]=C2=A0demonstrated=C2=A0how one could encode the rules o= f Dimensional
Analysis [2] into the C++ type system enabling compile-= time checking
(no runtime-cost) of the=C2=A0plausibility=C2=A0(at lea= st up to the dimensional
correctness) of computations.

In 2004, Abrahams & Gurtovy in 'C++ Template Metaprogramming'= ; [3]
showed the Barton Nackman technique to be elegantly implementab= le
using compile time type sequences encoding integer constants. At t= he
end of this post, I provide a complete listing of their example
program [4].

The key properties of the system (as I s= ee it) are:
=C2=A0 - Encoding of integers 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.

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
has "got something over on us" here ;)

My qu= estion therefore is: Does anyone have suggestions/pointers
on how to = approach automatic dimensional analysis via the OCaml type
system?=C2= =A0

Best,
<= div>
--=C2=A0
Shayne Fletcher

[1] John J. Barton and Lee R. Nackman. Scientific and Engine= ering C++:
=C2=A0 =C2=A0 an Introduction with Advanced Techniques and= Examples. Reading,
=C2=A0 =C2=A0 MA: Addison Wesley. ISBN 0-201-5339= 3-6. 1994.

[2] Wikipedia http://en.wikipedia.org/wiki/Dimensional_analy= sis

[3] David Abrahams and Aleksey Gurtovy C++ Templat= e Metaprogramming:
=C2=A0 =C2=A0 Concepts, Tools, and Techniques from= Boost and Beyond (C++ in
=C2=A0 =C2=A0 Depth Series), Addison-Wesley= Professional. ISBN:0321227255. 2004.

[4] Code listing:

=C2=A0 =C2=A0 //"c:/program files (x86)/Microsoft Visua= l Studio 10.0/vc/vcvarsall.bat" x64
=C2=A0 =C2=A0 //cl /Fedimens= ion.exe /EHsc /I d:/boost_1_55_0 dimension.cpp
=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 #include &= lt;boost/mpl/placeholders.hpp>
=C2=A0 =C2=A0 #include <boost/mp= l/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/static_assert.hpp>
=C2=A0 =C2=A0=C2=A0<= /div>
= =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::vector_c<int,0,1,0,0,0,0,0> le= ngth;
=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::vector_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::vecto= r_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 b= oost::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>= ; acceleration; // l/(t2)
=C2=A0 =C2=A0 typedef boost::mpl::vector_c&= lt;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::vect= or_c<int,0,0,0,0,0,0,0> scalar;
=C2=A0 =C2=A0=C2=A0
=C2= =A0 =C2=A0 template <class T, class Dimensions>
=C2=A0 =C2=A0 c= lass quantity
=C2=A0 =C2=A0 {
=C2=A0 =C2=A0 public:
=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 template <class OtherDimensions>
=C2=A0 =C2=A0 =C2=A0 qu= antity (quantity<T, OtherDimensions> const& other)
=C2=A0 = =C2=A0 =C2=A0 =C2=A0 : val (other.value ()) {
=C2=A0 =C2=A0 =C2=A0 = =C2=A0 BOOST_MPL_ASSERT( (boost::mpl::equal<Dimensions, OtherDimensions&= gt;));
=C2=A0 =C2=A0 =C2=A0 }
=C2=A0 =C2=A0 =C2=A0 T value () c= onst { return val; }
=C2=A0 =C2=A0 private:
=C2=A0 =C2=A0 =C2= =A0 T val;
=C2=A0 =C2=A0 };
=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 return quanti= ty<T, D>(x.value () + y.value ());
=C2=A0 =C2=A0 }
=
=C2=A0= =C2=A0=C2=A0
=C2=A0 =C2=A0 template <class T, class D><= /div>
= =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 }
=C2=A0 =C2=A0=C2=A0
=C2=A0 =C2=A0 template &l= t;class T, class D1, class D2>
=C2=A0 =C2=A0 quantity <<= /div>
= =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<<= /div>
= =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> x, quantity &= lt;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::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 retu= rn quantity<T, D> (x.value () * y.value ());
=C2=A0 =C2=A0 }<= /font>
=C2=A0 =C2=A0=C2=A0
=C2=A0 =C2=A0 template <class T, class D= 1, 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::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::m= pl::placeholders::_2> >::type=C2=A0
=C2=A0 =C2=A0 >
= =C2=A0 =C2=A0 operator/ (quantity<T, D1> x, quantity <T, D2> y)=
=C2=A0 =C2=A0 {
=C2=A0 =C2=A0 =C2=A0 typedef typename boost::m= pl::transform<
=C2=A0 =C2=A0 =C2=A0 =C2=A0 D1, D2, boost::mpl::min= us<
=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.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 <limits>
=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);<= /font>
=C2=A0 =C2=A0 =C2=A0 quantity<float, acceleration> 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;
=C2=A0 = =C2=A0=C2=A0
=C2=A0 =C2=A0 =C2=A0 assert ((std::abs ((m2 - m).value (= ))) <=3D std::numeric_limits<double>::epsilon ());
=C2=A0 = =C2=A0=C2=A0
=C2=A0 =C2=A0 =C2=A0 return 0;
=C2=A0 =C2=A0 }

--001a113b39dae814b305058cdd07--