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 4FA1A7EC6E for ; Fri, 13 Jun 2014 11:44:02 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.220.176; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.220.176 as permitted sender) identity=mailfrom; client-ip=209.85.220.176; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@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-vc0-f176.google.com) identity=helo; client-ip=209.85.220.176; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-vc0-f176.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao4CAP7GmlPRVdywlGdsb2JhbABag19SB4JswBkBfQgWDwEBAQEHCwsJEiqDfAcBAQECAhIRHQEUBxYHAQMMBgULDQICJgICIgERAQUBHAYTCAEZhSeCZAEDEQgFpkJqiyeBcoMPk2AKGScNZIUiEQEFDIEejTIHgnWBTASFH5UXgUOMF4QJGCmEbjsvAQ X-IPAS-Result: Ao4CAP7GmlPRVdywlGdsb2JhbABag19SB4JswBkBfQgWDwEBAQEHCwsJEiqDfAcBAQECAhIRHQEUBxYHAQMMBgULDQICJgICIgERAQUBHAYTCAEZhSeCZAEDEQgFpkJqiyeBcoMPk2AKGScNZIUiEQEFDIEejTIHgnWBTASFH5UXgUOMF4QJGCmEbjsvAQ X-IronPort-AV: E=Sophos;i="5.01,470,1400018400"; d="scan'208";a="67010250" Received: from mail-vc0-f176.google.com ([209.85.220.176]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 13 Jun 2014 11:44:01 +0200 Received: by mail-vc0-f176.google.com with SMTP id ik5so2005210vcb.21 for ; Fri, 13 Jun 2014 02:44:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=tldyyTCfS7CNNYrgEukixk3u1ZUX7x8aBGEmQOtSd+o=; b=jFG31/pbiIm/wcy+23L8P4pNRMuuxVB9Ku33PtCYe+w+83zU8FvUEh9cMoAVbLEWhz D47T0t3pB/jxw97WGBffjQzrYe9Lj+TDQvvtUEmH2y9TAXjZT1MPRNWDY96N/BctL54J SbCD0d5ocUSkzI4Q4NZvd/XZU2lNmCobHeRraYeaz6YAZfwH2jGVCXVTcQwldoO1PHxH UDcWL74bZ2k1R3FacVr9W2xTNfK/AHhXpy9cgQTZqopVcf2bH2s6CrV+Wy+nxyB0vHpj iCeB+QtO1VMQHepJEVXcEaWdZHWLifkLoshdexBp16WoSAR/dLlr28aXR7GbBTqvhBta FTHQ== X-Received: by 10.221.63.195 with SMTP id xf3mr206338vcb.36.1402652640547; Fri, 13 Jun 2014 02:44:00 -0700 (PDT) MIME-Version: 1.0 Received: by 10.58.178.230 with HTTP; Fri, 13 Jun 2014 02:43:20 -0700 (PDT) In-Reply-To: References: From: Gabriel Scherer Date: Fri, 13 Jun 2014 11:43:20 +0200 Message-ID: To: Roberto Di Cosmo Cc: caml users Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Adding Dimensions to types 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. 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. 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