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 232017EFCD for ; Fri, 17 Oct 2014 07:58:33 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of octa@polychoron.fr) identity=pra; client-ip=217.70.183.196; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="octa@polychoron.fr"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of octa@polychoron.fr) identity=mailfrom; client-ip=217.70.183.196; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="octa@polychoron.fr"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@relay4-d.mail.gandi.net) identity=helo; client-ip=217.70.183.196; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="postmaster@relay4-d.mail.gandi.net"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AigHAL2vQFTZRrfEnGdsb2JhbABbg2FYBIMCtDqBDgaTVoZ6VAKBExYBEQEBAQEBBg0JCRQuhAMBAQICIwQRQBELGAICBRYLAgIJAwIBAgFFEwgBAYg5BgMGthWUdQELAR+BLIR2ijIWgmGBVAWTBoNAiVqFIZItagEBAYFFgQMBAQE X-IPAS-Result: AigHAL2vQFTZRrfEnGdsb2JhbABbg2FYBIMCtDqBDgaTVoZ6VAKBExYBEQEBAQEBBg0JCRQuhAMBAQICIwQRQBELGAICBRYLAgIJAwIBAgFFEwgBAYg5BgMGthWUdQELAR+BLIR2ijIWgmGBVAWTBoNAiVqFIZItagEBAYFFgQMBAQE X-IronPort-AV: E=Sophos;i="5.04,737,1406584800"; d="scan'208";a="83562315" Received: from relay4-d.mail.gandi.net ([217.70.183.196]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 17 Oct 2014 07:58:25 +0200 Received: from mfilter25-d.gandi.net (mfilter25-d.gandi.net [217.70.178.153]) by relay4-d.mail.gandi.net (Postfix) with ESMTP id EB36D172071 for ; Fri, 17 Oct 2014 07:58:24 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at mfilter25-d.gandi.net Received: from relay4-d.mail.gandi.net ([217.70.183.196]) by mfilter25-d.gandi.net (mfilter25-d.gandi.net [10.0.15.180]) (amavisd-new, port 10024) with ESMTP id PJ6HRQwxytmx for ; Fri, 17 Oct 2014 07:58:23 +0200 (CEST) X-Originating-IP: 197.86.160.63 Received: from [192.168.1.106] (unknown [197.86.160.63]) (Authenticated sender: octa@polychoron.fr) by relay4-d.mail.gandi.net (Postfix) with ESMTPSA id 3B937172077 for ; Fri, 17 Oct 2014 07:58:22 +0200 (CEST) Message-ID: <5440AFFD.4010203@polychoron.fr> Date: Fri, 17 Oct 2014 07:58:21 +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: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Dimensional Analysis question Le 10/16/14 19:35, Mario Alvarez Picallo wrote: > Hello Shayne, > > I was at first convinced that this could not be done, but you can in > fact encode it (in a verbose way) with phantom types, > using a smart typelevel representation of integers > (http://www.kb.ecei.tohoku.ac.jp/ml2008/slides/lindley.pdf). > > I've written a small proof of concept that seems to work just fine > (but, of course, there may be errors), that you can find > here: https://gist.github.com/m-alvarez/b1e42b7b42cbeed7d1f0 > > It seems to be solid enough to pass the tests that Octachron tried, > but there probably are some other corner cases for which > it breaks down. Otherwise, it would be interesting to coalesce both > representations, using Octachron's idea of row types instead > of tuples to have extensible dimensional analysis, where each part of > the program can introduce its own dimensions. > > Regards, > Mario A. > I forget to add variance annotation in my test so my examples broke down due to the presence of monomorphic types. With the right implementation (i.e. Mario's), problems appear within functions. For instance, let f x = x* x works only for adimensional variable (i.e f : ('a*'a) t -> ('a*'a) t ) which is maybe not surprising. However, the same thing also happens to let f x y = (x+y)*x*y . because the type of x and y are unified during the addition "x+y". Regards, Octachron.