From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr 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 8DD1E7EC6E for ; Fri, 13 Jun 2014 11:10:26 +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.219.46; 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.219.46 as permitted sender) identity=mailfrom; client-ip=209.85.219.46; 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-oa0-f46.google.com) identity=helo; client-ip=209.85.219.46; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="postmaster@mail-oa0-f46.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtMEAMq+mlPRVdsulGdsb2JhbABag19SB4JsgmCnII0JigwIFg8BAQEBBwsLCRIqg3wMFBEdARQlAw0FAw03AiQSAQUBNQgBGYUngmUDEQgFliiNAYMSaosnhQGUACcNhhcBBQyRTIFMBIUfPpRZgUOMF4QJGCmBaYMFOy8B X-IPAS-Result: AtMEAMq+mlPRVdsulGdsb2JhbABag19SB4JsgmCnII0JigwIFg8BAQEBBwsLCRIqg3wMFBEdARQlAw0FAw03AiQSAQUBNQgBGYUngmUDEQgFliiNAYMSaosnhQGUACcNhhcBBQyRTIFMBIUfPpRZgUOMF4QJGCmBaYMFOy8B X-IronPort-AV: E=Sophos;i="5.01,470,1400018400"; d="scan'208";a="67003626" Received: from mail-oa0-f46.google.com ([209.85.219.46]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 13 Jun 2014 11:10:25 +0200 Received: by mail-oa0-f46.google.com with SMTP id m1so2504868oag.5 for ; Fri, 13 Jun 2014 02:10:24 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:date:message-id:subject:from:to:content-type; bh=uhoPdRjAbvBY7LC9cx0MLlq3/fIPyvekoo3A1VlHcPQ=; b=TM48ba7PeEpB4jgqVmL+S3/9jQCwUz9TM2ZmrCX0ptFS9AhZC+yZZ84GnIsb6cD3mO W90rPr0rwqJz2jg6mcH8HhKJgzlBmIN4lz/I3bQcMLiJNNUy/6C53825EdUYq7lXwyV6 phUZdTen2vNNSY6yXTfZB/iVz2TgSTG+oZh5qNGIssFs7nH3+dkKnDs8AlW3E7q99SJj PvVORD/GhuEabzKNOT8eSfDrUjhFrULTuojUB3F/1nzHW5q8vtglP+oGeMiGTHUq+Waq 3ybF62B8QFLgrwOPt6nzMsr0/oczPGnZ+waEwTcvA5GDLben+GEGS82k3Nq5FySMX8gt dzWQ== MIME-Version: 1.0 X-Received: by 10.182.72.167 with SMTP id e7mr1415960obv.28.1402650624232; Fri, 13 Jun 2014 02:10:24 -0700 (PDT) Sender: rdicosmo@gmail.com Received: by 10.60.48.68 with HTTP; Fri, 13 Jun 2014 02:10:24 -0700 (PDT) Date: Fri, 13 Jun 2014 11:10:24 +0200 X-Google-Sender-Auth: b3TP539VXJFSllD3HSWdahd6xhA Message-ID: From: Roberto Di Cosmo To: caml-list@inria.fr Content-Type: multipart/alternative; boundary=001a11c2f43433939204fbb40cd0 Subject: [Caml-list] Adding Dimensions to types --001a11c2f43433939204fbb40cd0 Content-Type: text/plain; charset=UTF-8 Dear friends OCamlers, in a meeting yesterday I had the occasion to listen to a talk by Frederic Boniol (search for his name in the proceedings below [1]), who went through some considerable gymnastics to add dimension checking to the Lustre programming language. This is work that was quite well pioneered some 20 years ago by Mitch Wand, Andrew Kennedy and Jean Goubault for our beloved ML paradigm, and you can still find on Bruno Blanchet's web page [2] a fully functional version of Caml-light extended to add dimensions, and you can play with it. More recently, you can find support for physical dimensions incorporated into F# [3]. Now the question that arose yesterday, and that we could not answer right away, is whether it is possible to encode such dymension checking in OCaml today using only the existing type-system features, so I am passing it over to the list :-) -- Roberto P.S.: yes, we know that you can somehow play tricks with phantom types to distinguish a meter from a foot, but checking dimensions is more tricky than that, consider the issue at stake when you multiply or divide quantities involving multiple dimensions (like computing an acceleration, or an energy). [1] http://afadl2014.lacl.fr/actes_AFADL2014-HAL.pdf [2] http://prosecco.gforge.inria.fr/personal/bblanche/cldim.html [3] http://blogs.msdn.com/b/andrewkennedy/archive/2008/08/29/units-of-measure-in-f-part-one-introducing-units.aspx ------------------------------------------------------------------ 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 320 (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 --001a11c2f43433939204fbb40cd0 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Dear friends OCamlers,
=C2=A0=C2=A0=C2= =A0 in a meeting yesterday I had the occasion to listen to a talk by Freder= ic Boniol (search for his name in the proceedings below [1]), who went thro= ugh some considerable gymnastics to add dimension checking to the Lustre pr= ogramming language.

This is work that was quite well pioneered some 20 years ago= by Mitch Wand, Andrew Kennedy and Jean Goubault
for our belo= ved ML paradigm, and you can still find on Bruno Blanchet's web page [2= ] a fully functional version of Caml-light extended to add dimensions, and = you can play with it. More recently, you can find support for physical dime= nsions incorporated into F# [3].

Now the question that arose yesterday, and that we could not= answer right away, is whether it is possible to encode such dymension chec= king in OCaml today using only the existing type-system features, so I am p= assing it over to the list :-)

--
Roberto

P.S.: yes, we know that you= can somehow play tricks with phantom types to=20 distinguish a meter from a foot, but checking dimensions is more tricky=20 than that, consider the issue at stake when you multiply or divide=20 quantities involving multiple dimensions (like computing an=20 acceleration, or an energy).

[1] http://afadl2014.lacl.fr/actes_AFADL2014-H= AL.pdf
[2] http://prosecco.gforge.inria.fr/per= sonal/bblanche/cldim.html
[3] http://blogs.msdn.com/b= /andrewkennedy/archive/2008/08/29/units-of-measure-in-f-part-one-introducin= g-units.aspx
=C2=A0
-----------------------------------------------------= -------------
Professeur =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 En delegation a l'INRIA
PPS =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0E-mail: roberto@dicosmo.org
Universite Paris Diderot WWW =C2=A0: http://www.dicosmo.org
Case 7014 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Tel =C2=A0: ++33-(0)1-57 27= 92 20
5, Rue Thomas Mann =C2=A0 =C2=A0 =C2=A0=C2=A0
F-75205 Paris Cedex 13 =C2=A0 Identica: http://identi.ca/rdicosmo
FRANCE. =C2=A0= =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Twitter: http://twitter.com/rdicosmo=
------------------------------------------------------------------
Attachments:
MIME accepted, Word deprecated
------------------------------------------------------------------
Office location:
=C2=A0
Bureau 320 (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=C2=A0
--001a11c2f43433939204fbb40cd0--