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 yquem.inria.fr (Postfix) with ESMTP id D7F3DBC57 for ; Tue, 3 Aug 2010 05:12:06 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiwBAKIlV0xCbwQZkWdsb2JhbACgCBUBAQEBCQsKBxEEHsR2BYU5 X-IronPort-AV: E=Sophos;i="4.55,307,1278280800"; d="scan'208";a="55038234" Received: from out1.smtp.messagingengine.com ([66.111.4.25]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 03 Aug 2010 05:12:05 +0200 Received: from compute2.internal (compute2.internal [10.202.2.42]) by gateway1.messagingengine.com (Postfix) with ESMTP id 79F691A3022 for ; Mon, 2 Aug 2010 23:10:56 -0400 (EDT) Received: from heartbeat2.messagingengine.com ([10.202.2.161]) by compute2.internal (MEProxy); Mon, 02 Aug 2010 23:11:18 -0400 DKIM-Signature: v=1; a=rsa-sha1; c=relaxed/relaxed; d=messagingengine.com; h=date:from:to:subject:in-reply-to:message-id:references:mime-version:content-type; s=smtpout; bh=gDZj98yvFyB/ZXHy7pCYs4BR5uc=; b=tu+FFnwSwIM+J1J5qQ0HPoPXvcDcULmEe+ihs+tkfcBl0GBRlKFfsuR6FoyyZdUK7xOaedWvmkNGlILHNZibFWPZ0ulhWpaDGa1PCAs1XR9xIXkS6T1/pfv8VaehtpzG9hLAKP+YFtzLeuzCkj3tBvd0PMbs4bXs/EmyW2l5Mgc= X-Sasl-enc: NwrW/1SP1pl4D3wU4tQ8IbS8mBJOi9HAtL9xDbM9004h 1280805035 Received: from [192.168.0.2] (69.49.171.211.swcp.com [69.49.171.211]) by mail.messagingengine.com (Postfix) with ESMTPSA id 787055B620 for ; Mon, 2 Aug 2010 23:10:35 -0400 (EDT) Date: Tue, 3 Aug 2010 04:46:55 +0200 (CEST) From: Joseph Young X-X-Sender: josyoun@myhome To: caml-list@inria.fr Subject: Re: [Caml-list] Conditionals based on phantom types In-Reply-To: Message-ID: References: MIME-Version: 1.0 Content-Type: MULTIPART/MIXED; BOUNDARY="0-1677318110-1280803609=:1541" X-Spam: no; 0.00; ocaml:01 conditionals:01 unreadable:01 mime-aware:01 printf:01 printf:01 variants:01 lukasz:01 val:01 typecheck:01 assertion:01 bug:01 lukasz:01 val:01 runtime:01 This message is in MIME format. The first part should be readable text, while the remaining parts are likely unreadable without MIME-aware tools. --0-1677318110-1280803609=:1541 Content-Type: TEXT/PLAIN; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: QUOTED-PRINTABLE =09I appreciate the reply and the suggestions. After looking over=20 your responses, could everything be simplified by removing the phantom=20 types? In other words, is there a draw back to using the definition: type units=3D[`Feet | `Meters];; let to_feet x : [`Feet]*float=3D`Feet,x;; let to_meters x : [`Meters]*float=3D`Meters,x;; let add (u,x:'a*float) (_,y:'a*float) =3D u,x +. y;; let unit_to_string=3Dfunction | `Feet -> "ft" | `Meters -> "m" ;; let print (u,x:[< units]*float) =3D Printf.printf "%f (%s)" x =09(unit_to_string u);; which instead of phantom types relies on polymorphic variants that contain= =20 only a single value? Joe On Mon, 2 Aug 2010, bluestorm wrote: > Two remarks on Lukasz suggestion : > >> =A0 val add : 'a t -> 'a t -> 'a t >> [..] >> =A0 let add (_,x) (_,y) =3D x +. y > > This does not typecheck. I suggest the following : > > let add (ux, x) (uy, y) =3D > assert (ux =3D uy); > (ux, x +. y) > > While the assertion does not seem necessary at first (correct units > are guaranteed by typing !), it may be helpful in case of bug inside > the Units module or signature, wich breaks the typing invariant. If > you're planning to do relatively elaborate things inside the Units, I > strongly recommend to use any kind of dynamic checking available, at > least during development. This is something is understood late in my > own phantom-type project (Macaque), and would have been very useful > for debugging. > > > > On Mon, Aug 2, 2010 at 9:49 AM, Lukasz Stafiniak wro= te: >> =A0 val print : 'a t -> unit >> [..] >> =A0 type 'a t =3D 'a * float >> =A0 let print (u,x) =3D Printf.printf "%f %s" x (to_string u) > > Lukasz doesn't give a to_string function. Assuming this one, there is > a typing problem here. > > let to_string =3D function > | `Feet -> "feet" > | `Meters -> "meters" > > Values do not match: > val print : [< `Feet | `Meters ] * float -> unit > is not included in > val print : 'a t -> unit > > The issue is that, with Lukasz definition, 'a is now coupled to the > concrete values (type 'a t =3D 'a * float), and the to_string function > is *not* polymorphic in 'a as advertised by the interface. I see two > solutions : > > 1) restrict print to only print the units you directly support : > > val print : [ `Feet | `Meters ] * float -> unit > > 2) make 'a a phantom type parameter again by decoupling the type > information (the polymoprhic variant) and the runtime information > (another, value-level, variant) : > > odule Units : sig > type 'a t > val to_feet : float -> [`Feet ] t > val to_meters : float -> [`Meters] t > val add : 'a t -> 'a t -> 'a t > val print : 'a t -> unit > end =3D struct > type unit =3D Feet | Meters > let string_of_unit =3D function > | Feet -> "feet" > | Meters -> "meters" > > type 'a t =3D unit * float > > let to_feet x =3D Feet, x > let to_meters x =3D Meters, x > > let add (ux, x) (uy, y) =3D > assert (ux =3D uy); > (ux, x +. y) > > let print (u, x) =3D > Printf.printf "%f (%s)" x (string_of_unit u) > end;; > > I would rather go the second way, wich allows for more flexibility in > what runtime informations keep, and what type information you expose. > --0-1677318110-1280803609=:1541--