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 CA9187EC6E for ; Fri, 13 Jun 2014 11:54:06 +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.175; 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.175 as permitted sender) identity=mailfrom; client-ip=209.85.212.175; 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-f175.google.com) identity=helo; client-ip=209.85.212.175; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="postmaster@mail-wi0-f175.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AokCAFzJmlPRVdSvlGdsb2JhbABagml2UsQSFg8BAQEBBwsLCRIqg3wHAQEBAgEBEigGARQdBwEDAQsBBQUYCSUPBSABBQEBIRMJGYUngmUDCQgBBAMFpj5qkCiUAicNhgYRAQUMkgKBFgSFHz6UWIFEjBeECUGBaYMFagE X-IPAS-Result: AokCAFzJmlPRVdSvlGdsb2JhbABagml2UsQSFg8BAQEBBwsLCRIqg3wHAQEBAgEBEigGARQdBwEDAQsBBQUYCSUPBSABBQEBIRMJGYUngmUDCQgBBAMFpj5qkCiUAicNhgYRAQUMkgKBFgSFHz6UWIFEjBeECUGBaYMFagE X-IronPort-AV: E=Sophos;i="5.01,470,1400018400"; d="scan'208";a="67011926" Received: from mail-wi0-f175.google.com ([209.85.212.175]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 13 Jun 2014 11:54:05 +0200 Received: by mail-wi0-f175.google.com with SMTP id r20so558581wiv.8 for ; Fri, 13 Jun 2014 02:54:05 -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:in-reply-to:user-agent; bh=MMj6BYWnW2c3hkna1h/THSn+inhMvMTel6OI/88mfsQ=; b=b6KzyktsjUN0cIovc3ipnnH0B441TAzmztdqR68xGzE40F15hYr9SWqQLp/eIncw2D Z5lYDDepbmVqHn+nAHy4h6nrskgn4dQ+o/GucijRGRd4El7idDWueJEftEII42eRtdYy frtY/Nwwut5Bv9RtMBpO1unFxfc2EyMli6T9nixQGvAkY1hlpGPpiDpi0Z0A2/TKzIJL D7TOfIhaofjErUz9ONNwj8tCfzAjcb8L3aNUgz0/K10GErU1sa13+IL/+ONdqf4qjVJO wfz6AS7Ro6S5vnq87ZzEytxxmjPRvlWYm0nJl99aZCjTMbBjyjkacJNtFX371LiaPDsd iwQA== X-Received: by 10.180.109.101 with SMTP id hr5mr3093993wib.25.1402653245751; Fri, 13 Jun 2014 02:54:05 -0700 (PDT) Received: from traveler ([2002:805d:3c4f:0:7e7a:91ff:fe72:2d29]) by mx.google.com with ESMTPSA id f2sm1517173wiz.11.2014.06.13.02.54.04 for (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 13 Jun 2014 02:54:05 -0700 (PDT) Sender: Roberto Di Cosmo Received: from dicosmo by traveler with local (Exim 4.82_1-5b7a7c0-XX) (envelope-from ) id 1WvOBP-0004pQ-9b; Fri, 13 Jun 2014 11:54:03 +0200 Date: Fri, 13 Jun 2014 11:54:03 +0200 From: Roberto Di Cosmo To: Gabriel Scherer Cc: caml users Message-ID: <20140613095403.GB18282@traveler> References: MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) Subject: Re: [Caml-list] Adding Dimensions to types On Fri, Jun 13, 2014 at 11:43:20AM +0200, Gabriel Scherer wrote: > Encoding integers with addition at the type level is easy enough (it > is possible to use a technique akin to difference list where you keep > unary numbers with a unification variable at their tail, to get the > unification engine to do the addition for you). Anything below that, > in particular substraction, cannot be done *conveniently* in the > type-system. It is possible to encode arbitrary operation on > type-level numbers (unary or not), expressed relationally > (Prolog-style: ('a, 'b, 'c) add is inhabited if 'a+'b='c) by a GADT > witnessing the relation, but actually building and using these > operations then requires the programmer to provide those witness terms > that are manipulated at runtime. Actually, we want to have dimension checking at compile time, with no trace of it at runtime. > This could possibly be hidden under a layer of syntactic sugar; to > generate the correct witness terms, you however need access to the > typing environment or approximate it, so it's hard to do at the > camlp4-ppx layer, and you rather need .cmt-level processing; in fact > the new presentation of formats as GADTs does exactly this). However, > the runtime costs of witness manipulation could be prohibitive for > numerical computations. > > I suspect that if for some reason people were to absolutely need this > feature, the easiest path would probably be to extend the type-checker > with support for this. So far, it seems that nobody was interested > enough in this to do the (important) amount of work necessary. It seems that there is now a more general interest in this idea, and I wonder how important this amount of work is... in Bruno's memoire there is a detailed explanation of the changes, which seem kind of well isolated, but that was for Caml-Light of course. > On Fri, Jun 13, 2014 at 11:10 AM, Roberto Di Cosmo wrote: > > 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 -- 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