From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 9D58D7EFCD for ; Thu, 16 Oct 2014 19:21:59 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of octa@polychoron.fr) identity=pra; client-ip=217.70.183.195; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="octa@polychoron.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of octa@polychoron.fr) identity=mailfrom; client-ip=217.70.183.195; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="octa@polychoron.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@relay3-d.mail.gandi.net) identity=helo; client-ip=217.70.183.195; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="postmaster@relay3-d.mail.gandi.net"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiwEAKb9P1TZRrfDm2dsb2JhbABbg2FZA4MChVuvbQaTUIdNAoEXFgERAQEBAQEGCwsJFC6EAwEBBCMEUREJAiEWAQEJAgIJAwIBAgE3DhMIAQEXiCMECZkHnE+VPoYiijKCd4FUBYUVjXCDQIlZhSGQBgEBAYIkgjKBAgEBAQ X-IPAS-Result: AiwEAKb9P1TZRrfDm2dsb2JhbABbg2FZA4MChVuvbQaTUIdNAoEXFgERAQEBAQEGCwsJFC6EAwEBBCMEUREJAiEWAQEJAgIJAwIBAgE3DhMIAQEXiCMECZkHnE+VPoYiijKCd4FUBYUVjXCDQIlZhSGQBgEBAYIkgjKBAgEBAQ X-IronPort-AV: E=Sophos;i="5.04,733,1406584800"; d="scan'208,217";a="101524813" Received: from relay3-d.mail.gandi.net ([217.70.183.195]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 16 Oct 2014 19:21:58 +0200 Received: from mfilter12-d.gandi.net (mfilter12-d.gandi.net [217.70.178.129]) by relay3-d.mail.gandi.net (Postfix) with ESMTP id A5D7BA80DF for ; Thu, 16 Oct 2014 19:21:58 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at mfilter12-d.gandi.net Received: from relay3-d.mail.gandi.net ([217.70.183.195]) by mfilter12-d.gandi.net (mfilter12-d.gandi.net [10.0.15.180]) (amavisd-new, port 10024) with ESMTP id lMb-ArqjXgFS for ; Thu, 16 Oct 2014 19:21:56 +0200 (CEST) X-Originating-IP: 146.232.92.127 Received: from [146.232.92.127] (unknown [146.232.92.127]) (Authenticated sender: octa@polychoron.fr) by relay3-d.mail.gandi.net (Postfix) with ESMTPSA id E4091A80CE for ; Thu, 16 Oct 2014 19:21:55 +0200 (CEST) Message-ID: <543FFEB1.2030400@polychoron.fr> Date: Thu, 16 Oct 2014 19:21:53 +0200 From: Octachron User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.1.2 MIME-Version: 1.0 To: caml-list@inria.fr References: In-Reply-To: Content-Type: multipart/alternative; boundary="------------040902000105070004030202" Subject: Re: [Caml-list] Dimensional Analysis question This is a multi-part message in MIME format. --------------040902000105070004030202 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: quoted-printable Hello, As far as I know it is possible to do some kind of basic dimensional=20 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=20 than the natural numbers themselves. The free parameter 'a allows to type addition and substraction. We can=20 then define numbers with unit as a phantom type type 'a t =3D float and for instance a meter function as let m : float -> < m : 'a -> 'a > t =3D 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=20 natural encoding to perform the addition let ( * ) : 'mid > t -> 'sup> t -> =20 'sup> t =3D *. let (/): < m: inf->sup > t -> mid> t -> sup> t =3D ( /.= ) This solution works for basic use but falls apart in complex use due to=20 the lack of second-rank polymorphism. For instance, let y =3D m 2. * m 3. works but let x =3D m 2. in let y =3D x * x doe not. Even worse let () =3D let x =3D m 1. in let y =3D m 2. in let w =3D x * y in () works but let () =3D let x =3D m 1. in let y =3D m 2. in let w =3D x * y in let z =3D x + y in () triggers a compilation error. And unfortunately, I am not aware of any way to avoid these quirky=20 behaviors. Regards, octachron. Le 10/16/14 18:37, Shayne Fletcher a =C3=A9crit : > 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, > > --=20 > 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=20 > 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; //=20 > 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 =3D m * a; > quantity m2 =3D f / a; > assert ((std::abs ((m2 - m).value ())) <=3D=20 > std::numeric_limits::epsilon ()); > return 0; > } > --------------040902000105070004030202 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
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=C2=A0 (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 =3D float

and for instance a meter function as

let m : float ->=C2=A0 < m : 'a -> 'a > t =3D 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=C2=A0 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 =3D *.
let (/):=C2=A0 < m: inf->sup > t -> <m:inf->mid>= t -> <m: mid-> sup>=C2=A0 t =3D ( /. )
=C2=A0=C2=A0 =C2=A0
This solution works for basic use but falls apart in complex use due to the lack of second-rank polymorphism.
For instance,

=C2=A0=C2=A0=C2=A0=C2=A0 let y =3D m 2. * m 3. =C2=A0

works but

=C2=A0=C2=A0=C2=A0 let x =3D m 2. in
=C2=A0=C2=A0=C2=A0 let y =3D x * x

doe not. Even worse

let () =3D
=C2=A0=C2=A0=C2=A0 let x =3D m 1. in
=C2=A0=C2=A0=C2=A0 let y =3D m 2. in
=C2=A0=C2=A0=C2=A0 let w =3D x * y in
=C2=A0=C2=A0=C2=A0 ()

works but=C2=A0

let () =3D
=C2=A0=C2=A0=C2=A0 let x =3D m 1. in
=C2=A0=C2=A0=C2=A0 let y =3D m 2. in
=C2=A0=C2=A0=C2=A0 let w =3D x * y in
=C2=A0=C2=A0=C2=A0 let z =3D x + y in
=C2=A0=C2=A0=C2=A0 ()

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 =C3=A9crit=C2=A0:
Dear OCamlers,

In 1994, Barton and Nackman in their book 'Scientific Engineering in
C++' [1]=C2=A0demonstrated=C2=A0how one could enc= ode the rules of Dimensional
Analysis [2] into the C++ type system enabling compile-time checking
(no runtime-cost) of the=C2=A0plausibility=C2=A0(= 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:
=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
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?=C2=A0

Best,

--=C2=A0
Shayne Fletcher

[1] John J. Barton and Lee R. Nackman. Scientific and Engineering C++:
=C2=A0 =C2=A0 an Introduction with Advanced Techn= iques 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_analysis

[3] David Abrahams and Aleksey Gurtovy C++ Template Metaprogramming:
=C2=A0 =C2=A0 Concepts, Tools, and Techniques fro= m 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= Visual Studio 10.0/vc/vcvarsall.bat" x64
=C2=A0 =C2=A0 //cl /Fedimension.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.hp= p>
=C2=A0 =C2=A0 #include <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/static_assert.hp= p>
=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::vector_c<int,0,1,0,0,0,0,0> length;<= /div>
=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;<= /div>
=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> acceleration; // 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> scalar;<= /div>
=C2=A0 =C2=A0=C2=A0
=C2=A0 =C2=A0 template <class T, class Dimensi= ons>
=C2=A0 =C2=A0 class 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 OtherDime= nsions>
=C2=A0 =C2=A0 =C2=A0 quantity (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>));
=C2=A0 =C2=A0 =C2=A0 }
=C2=A0 =C2=A0 =C2=A0 T value () const { return va= l; }
=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 quantity<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>
=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 <class T, class D1, cla= ss 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::p= lus<
=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 <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::p= lus<
=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 template <class T, class D1, cla= ss 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::m= inus<
=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 <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::m= inus<
=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);
=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;
=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 }


--------------040902000105070004030202--