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 AF0D77EC6E for ; Fri, 13 Jun 2014 12:12:37 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of rdicosmo@gmail.com) identity=pra; client-ip=209.85.212.173; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="rdicosmo@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of rdicosmo@gmail.com designates 209.85.212.173 as permitted sender) identity=mailfrom; client-ip=209.85.212.173; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wi0-f173.google.com) identity=helo; client-ip=209.85.212.173; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="postmaster@mail-wi0-f173.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AokCALzNmlPRVdStlGdsb2JhbABaDoJbdlLEERYPAQEBAQcLCwkSKoQDAQEBBBIVEwYBFCQBAwwBBQUOCgklDwUgAQUBASETCRmIDAMRAQQDBaZBapAolAMnDYYGEQEFDJICgRYEhV2UWIFEjBeECUGBaYJDQmo X-IPAS-Result: AokCALzNmlPRVdStlGdsb2JhbABaDoJbdlLEERYPAQEBAQcLCwkSKoQDAQEBBBIVEwYBFCQBAwwBBQUOCgklDwUgAQUBASETCRmIDAMRAQQDBaZBapAolAMnDYYGEQEFDJICgRYEhV2UWIFEjBeECUGBaYJDQmo X-IronPort-AV: E=Sophos;i="5.01,470,1400018400"; d="scan'208";a="79873365" Received: from mail-wi0-f173.google.com ([209.85.212.173]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 13 Jun 2014 12:12:37 +0200 Received: by mail-wi0-f173.google.com with SMTP id cc10so593820wib.0 for ; Fri, 13 Jun 2014 03:12:37 -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=8Z+xCjRNNW+Peti2W1lrLYOt5TBrL88aAhrQpzcqCvE=; b=uObLAcqNwjnEz1kMAi2JtdQtHNkQkBlKlZbSgc20AYDPINqAIH2X8JnMzTQwX6oj8V 9Qbsnsus514UQfSQo/OsEJqfZMbglaHMgR0s16P7NesJEcQqfGDz5uEGuRjiLJ7DjPeq hczq8FpwYvQVieJovyBc9WrOKcWMRO16xdaP9cpoE+hhbs3kR1rbMbKtLNganCpO983E Mq9BOmGpPIcJ4XJ+aemAt3EfKrUKRg6PJ6T2vRg59A+E4PEKRr23/qwiWGVSSjEbmMbL 9076L0ul+d2vnn3xJMr/MYjla+uMkTfI6vfbUJ49IDbZWL10cZaMv1oMfgGA80GDYS6g KkaA== X-Received: by 10.194.92.176 with SMTP id cn16mr2729994wjb.43.1402654357119; Fri, 13 Jun 2014 03:12:37 -0700 (PDT) Received: from traveler ([2002:805d:3c4f:0:7e7a:91ff:fe72:2d29]) by mx.google.com with ESMTPSA id o3sm1582449wiz.24.2014.06.13.03.12.35 for (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 13 Jun 2014 03:12:36 -0700 (PDT) Sender: Roberto Di Cosmo Received: from dicosmo by traveler with local (Exim 4.82_1-5b7a7c0-XX) (envelope-from ) id 1WvOTJ-00057W-V9; Fri, 13 Jun 2014 12:12:33 +0200 Date: Fri, 13 Jun 2014 12:12:33 +0200 From: Roberto Di Cosmo To: Leo White Cc: caml-list@inria.fr Message-ID: <20140613101233.GE18158@traveler> References: <868up1kug8.fsf@cam.ac.uk> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <868up1kug8.fsf@cam.ac.uk> User-Agent: Mutt/1.5.23 (2014-03-12) Subject: Re: [Caml-list] Adding Dimensions to types Thanks Leo for this answer: basically, following your code, if I want n dimension, I will need a phantom type with 2*n variables, and define the units by putting a difference in the right 'field', right? It is not really readable, and has limitations, but it is a nice encoding nonetheless. On Fri, Jun 13, 2014 at 10:52:23AM +0100, 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 > > 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 -- 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