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 21F9E7EC6E for ; Fri, 13 Jun 2014 11:52:27 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=pra; client-ip=131.111.8.141; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=mailfrom; client-ip=131.111.8.141; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@ppsw-41.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.141; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="postmaster@ppsw-41.csi.cam.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiQBAFzJmlODbwiNnGdsb2JhbABarhgGmR8BgQUWDwEBAQEBCAsJCRQohAMBAQQBJxM/BQsLISUPAQRJiE0IBMxmhS8XFoVGiQAHhEEEsUc X-IPAS-Result: AiQBAFzJmlODbwiNnGdsb2JhbABarhgGmR8BgQUWDwEBAQEBCAsJCRQohAMBAQQBJxM/BQsLISUPAQRJiE0IBMxmhS8XFoVGiQAHhEEEsUc X-IronPort-AV: E=Sophos;i="5.01,470,1400018400"; d="scan'208";a="67011627" Received: from ppsw-41.csi.cam.ac.uk ([131.111.8.141]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 13 Jun 2014 11:52:26 +0200 X-Cam-AntiVirus: no malware found X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from host31-50-138-167.range31-50.btcentralplus.com ([31.50.138.167]:42136 helo=netbook) by ppsw-41.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.157]:587) with esmtpsa (PLAIN:lpw25) (TLSv1.2:DHE-RSA-AES128-SHA:128) id 1WvO9p-0006fe-Qd (Exim 4.82_3-c0e5623) (return-path ); Fri, 13 Jun 2014 10:52:25 +0100 From: Leo White To: Roberto Di Cosmo Cc: caml-list@inria.fr References: X-Face: "XWxb[u_Z\PA_Y?9@|IA!!+jTb(/290-*ea/Un$I0B98.$n%eL.;2w*,z]WR#T:,p[ NBd++M7l]#7zj7!{~iw $W-"/=|dVjhT[D{4~gE}gK<2`.6fs!;uqqud]vs2N/3^m7{aS1V, Date: Fri, 13 Jun 2014 10:52:23 +0100 In-Reply-To: (Roberto Di Cosmo's message of "Fri, 13 Jun 2014 11:10:24 +0200") Message-ID: <868up1kug8.fsf@cam.ac.uk> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Subject: Re: [Caml-list] Adding Dimensions to types > 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 This successfully tracks the dimension of quatities: # open Unit;; # let m10 = mul (of_float 10.) metre;; val m10 : ('a, 'a Unit.suc) Unit.quantity = # let sum = add m10 m10;; val sum : ('a, 'a Unit.suc) Unit.quantity = # let sq = mul m10 m10;; val sq : ('a, 'a Unit.suc Unit.suc) Unit.quantity = # let cube = mul m10 (mul m10 m10);; val cube : ('a, 'a Unit.suc Unit.suc Unit.suc) Unit.quantity = # let _ = add (mul sq (inv cube)) (inv m10);; - : ('a Unit.suc, 'a) Unit.quantity = and it will give errors if they are used incorrectly: # let _ = add sq cube;; Characters 15-19: let _ = add sq cube;; ^^^^ Error: This expression has type ('a, 'a Unit.suc Unit.suc Unit.suc) Unit.quantity but an expression was expected of type ('a, 'a Unit.suc Unit.suc) Unit.quantity The type variable 'a occurs inside 'a Unit.suc # let _ = add m10 (mul m10 m10);; Characters 16-29: let _ = add m10 (mul m10 m10);; ^^^^^^^^^^^^^ Error: This expression has type ('a, 'a Unit.suc Unit.suc) Unit.quantity but an expression was expected of type ('a, 'a Unit.suc) Unit.quantity The type variable 'a occurs inside 'a Unit.suc 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;; and apply it like so: # module AppSq = Sq(struct type 'a t = 'a suc end);; # let x = AppSq.sq {AppSq.x = m10};; val x : ('a, 'a Unit.suc Unit.suc) Unit.quantity = It is also worth noting that -rectypes breaks this encoding: #rectypes;; # let _ = add sq cube;; - : ('a Unit.suc as 'a, 'a Unit.suc Unit.suc) Unit.quantity = Regards, Leo