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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 211547EC6E for ; Fri, 13 Jun 2014 22:08:14 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of edwin+ml-ocaml@etorok.net) identity=pra; client-ip=62.113.205.31; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="edwin+ml-ocaml@etorok.net"; x-sender="edwin+ml-ocaml@etorok.net"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of edwin+ml-ocaml@etorok.net designates 62.113.205.31 as permitted sender) identity=mailfrom; client-ip=62.113.205.31; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="edwin+ml-ocaml@etorok.net"; x-sender="edwin+ml-ocaml@etorok.net"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of postmaster@mx.etorok.net designates 62.113.205.31 as permitted sender) identity=helo; client-ip=62.113.205.31; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="edwin+ml-ocaml@etorok.net"; x-sender="postmaster@mx.etorok.net"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhIFALVZm1M+cc0f/2dsb2JhbABagw1SwxRRAYEFFnWEAwEBAwEBJxk4AgQLCxgJEwMPCQMCAQIBRRMIAog2DAmxf4V+mhcRBo49KYRBijmQAoFDkhSDQTovAQE X-IPAS-Result: AhIFALVZm1M+cc0f/2dsb2JhbABagw1SwxRRAYEFFnWEAwEBAwEBJxk4AgQLCxgJEwMPCQMCAQIBRRMIAog2DAmxf4V+mhcRBo49KYRBijmQAoFDkhSDQTovAQE X-IronPort-AV: E=Sophos;i="5.01,473,1400018400"; d="scan'208";a="79970116" Received: from mx.etorok.net ([62.113.205.31]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 13 Jun 2014 22:08:13 +0200 Received: by mx.etorok.net (OpenSMTPD) with ESMTP id a2ad330e; for ; Fri, 13 Jun 2014 23:08:10 +0300 (EEST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed/relaxed; d=etorok.net; h= message-id:date:from:mime-version:to:references:in-reply-to :content-type:content-transfer-encoding; s=ml; l=3175; bh=L9ZeyJ hx974ZRoNohX1PqjWymbg=; b=MsZuMFGFlSr8urJUY5RIQayIsSewhRBN+Lp3sH MeZh2chA2E5KShHsC3e0g1V/Nriv8TVtKB57pVeqxXK6T/bWxmIbe/PSpA8JWhQ7 gXUiL06tqD2jO1e2ciY+y0tY0datjW/yi4kx8pxLvqFcRcJCDBvbT19BMNcpPW4B RDeMo= Received: by mx.etorok.net (OpenSMTPD) with ESMTPSA id 0e1d7200; TLS version=TLSv1/SSLv3 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NO; for ; Fri, 13 Jun 2014 23:08:09 +0300 (EEST) Message-ID: <539B5A29.9050900@etorok.net> Date: Fri, 13 Jun 2014 23:08:09 +0300 From: =?ISO-8859-1?Q?T=F6r=F6k_Edwin?= User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:30.0) Gecko/20100101 Icedove/30.0 MIME-Version: 1.0 To: caml-list@inria.fr References: <868up1kug8.fsf@cam.ac.uk> In-Reply-To: <868up1kug8.fsf@cam.ac.uk> Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Adding Dimensions to types On 06/13/2014 12:52 PM, Leo White wrote: >> 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 :-) > > You can do something reasonable using difference lists to encode a > dimension in a phantom type. For example, the following module (based on > an initial version by Stephen Dolan): > > module Unit : sig > type +'a suc > type (+'a, +'b) quantity > > val of_float : float -> ('a, 'a) quantity > val metre : ('a, 'a suc) quantity > val mul : ('a, 'b) quantity -> ('b, 'c) quantity -> ('a, 'c) quantity > val add : ('a, 'b) quantity -> ('a, 'b) quantity -> ('a, 'b) quantity > val neg : ('a, 'b) quantity -> ('a, 'b) quantity > val inv : ('a, 'b) quantity -> ('b, 'a) quantity > end = struct > type 'a suc = unit > type ('a, 'b) quantity = float > let of_float x = x > let metre = 1. > let mul x y = x *. y > let add x y = x +. y > let neg x = 0. -. x > let inv x = 1. /. x > end For some more information on how this works I found these presentations useful: http://www.kb.ecei.tohoku.ac.jp/ml2008/slides/lindley.pdf http://homepages.inf.ed.ac.uk/slindley/papers/many-holes.pdf With your representation '('a,'b) quantity' could be thought of as representing quantity ** ('b - 'a), or quantity ** 'b / (quantity ** 'a). I think it still works if you use ('a * 'b) instead of ('a, 'b), so then one could write SI units using something like (maybe with an 8th unit for scale): val of_float: float -> ('a * 'a, 'b * 'b, 'c * 'c, 'd * 'd, 'e * 'e, 'f * 'f, 'g* 'g) t val m: float -> ('metre * 'metre s, 'b * 'b, 'c * 'c, 'd * 'd, 'e * 'e, 'f * 'f, 'g* 'g) t val kg: float -> ('a * 'a s, 'kilogram * 'kilogram s, 'c * 'c, 'd * 'd, 'e * 'e, 'f * 'f, 'g* 'g) t val s: float -> ('a * 'a, 'b * 'b, 'second * 'second s, 'd * 'd, 'e * 'e, 'f * 'f, 'g* 'g) t val a: float -> ('a * 'a, 'b * 'b, 'c * 'c, 'ampere * 'ampere s, 'e * 'e, 'f * 'f, 'g* 'g) t val k: float -> ('a * 'a, 'b * 'b, 'c * 'c, 'd * 'd, 'kelvin * 'kelvin s, 'f * 'f, 'g* 'g) t val mol: float -> ('a * 'a, 'b * 'b, 'c * 'c, 'd * 'd, 'e * 'e, 'mole * 'mole s, 'g* 'g) t val cd: float -> ('a * 'a, 'b * 'b, 'c * 'c, 'd * 'd, 'e * 'e, 'f * 'f,'candela * 'candela s) t The error messages might get hard to understand at some point though, although that might be solved by pretty-printing / post-processing the compiler's error message somehow. > However, it will infer too restrictive types for some things: > > # let sq x = mul x x;; > val sq : ('a, 'a) Unit.quantity -> ('a, 'a) Unit.quantity = > > The "real" type of `sq` requires higher-kinded and higher-rank > polymorphism. Using functors you can encode `sq` thus: > > # module Sq (X : sig type 'a t end) = struct > type arg = {x: 'a. ('a, 'a X.t) quantity} > let sq {x} = mul x x > end;; That is interesting, but I'm worried that if for something as simple as x^2 you need to write that how would it look like when you need to write the type for a real equation? Best regards, --Edwin