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 343907F057 for ; Fri, 17 Oct 2014 08:50:24 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of rdicosmo@gmail.com) identity=pra; client-ip=209.85.212.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="rdicosmo@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of rdicosmo@gmail.com designates 209.85.212.177 as permitted sender) identity=mailfrom; client-ip=209.85.212.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="rdicosmo@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-wi0-f177.google.com) identity=helo; client-ip=209.85.212.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="postmaster@mail-wi0-f177.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AisDAHS7QFTRVdSxm2dsb2JhbABbg2FTBcI+iXCBW4cCFgERAQEBAQEGCwsJFC6EAwEBBBIgAQ0BFCQBAwwBBQUYCSUPBSABBQEBDRQTCRmICQMRBAEDBalobpAyiHonDYZCAQEBAQEFAQEBARgBBQ6Tc4EeBYUVgRiQGYRBglGBQiuNXYRhQYFsgz5qAQGCSQEBAQ X-IPAS-Result: AisDAHS7QFTRVdSxm2dsb2JhbABbg2FTBcI+iXCBW4cCFgERAQEBAQEGCwsJFC6EAwEBBBIgAQ0BFCQBAwwBBQUYCSUPBSABBQEBDRQTCRmICQMRBAEDBalobpAyiHonDYZCAQEBAQEFAQEBARgBBQ6Tc4EeBYUVgRiQGYRBglGBQiuNXYRhQYFsgz5qAQGCSQEBAQ X-IronPort-AV: E=Sophos;i="5.04,737,1406584800"; d="scan'208";a="83566962" Received: from mail-wi0-f177.google.com ([209.85.212.177]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 17 Oct 2014 08:50:23 +0200 Received: by mail-wi0-f177.google.com with SMTP id fb4so380382wid.16 for ; Thu, 16 Oct 2014 23:50:23 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-type:content-disposition:content-transfer-encoding :in-reply-to:user-agent; bh=b8EPv31+lJ+rdmHse4BtfsxwyxoREKQiAR3Pn8m+jWE=; b=tVKcLsn3xd/x5qXhDXlYI9x3Xv1ivxqshLPjBX2OMHaPXGHVVsK3pEtJd2FcehnXIw AshtOz3kq5hSsbvVW3bPnrAblMEQ5P4ddslToG7SDO/X8FDTkKiTVCFJDwAzlsKktKNJ H118TOpCcM9jz7XwQHE0K9tYRt7uTwt4Z/M/DjVHhu5pBMJm4NoWOgjIIGulXZDo2PPV 2x3Q2QAp3WjUGzIbeq+srclyfli/VGn+52LXqimWS0kWe7Hr0NMuaUevpvvbH31CtsPb ZyfaPUTtmAvt/kKGkVIyFsdvqFNiP1ILb8DEzjxC03782Y4S3mUrwKqXni6EmyluGvMT fC9g== X-Received: by 10.194.158.33 with SMTP id wr1mr7728107wjb.112.1413528623077; Thu, 16 Oct 2014 23:50:23 -0700 (PDT) Received: from traveler (bny92-3-81-56-44-163.fbx.proxad.net. [81.56.44.163]) by mx.google.com with ESMTPSA id cw6sm539882wjb.18.2014.10.16.23.50.21 for (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 16 Oct 2014 23:50:22 -0700 (PDT) Sender: Roberto Di Cosmo Received: from dicosmo by traveler with local (Exim 4.82_1-5b7a7c0-XX) (envelope-from ) id 1Xf1Mj-0006so-83; Fri, 17 Oct 2014 08:50:21 +0200 Date: Fri, 17 Oct 2014 08:50:21 +0200 From: Roberto Di Cosmo To: Shayne Fletcher Cc: "caml-list@inria.fr users" Message-ID: <20141017065021.GB25775@traveler> References: MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) Subject: Re: [Caml-list] Dimensional Analysis question 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 >     #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; >     } > -- 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