From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 7CE64BC57 for ; Tue, 3 Aug 2010 08:39:05 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiwBAJ5WV0xCbwQZkWdsb2JhbACgCRUBAQEBBw0KBxEEHsMABYU5 X-IronPort-AV: E=Sophos;i="4.55,308,1278280800"; d="scan'208";a="56676043" Received: from out1.smtp.messagingengine.com ([66.111.4.25]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 03 Aug 2010 08:39:04 +0200 Received: from compute1.internal (compute1.internal [10.202.2.41]) by gateway1.messagingengine.com (Postfix) with ESMTP id 0208318217E for ; Tue, 3 Aug 2010 02:39:03 -0400 (EDT) Received: from heartbeat1.messagingengine.com ([10.202.2.160]) by compute1.internal (MEProxy); Tue, 03 Aug 2010 02:39:03 -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:content-id; s=smtpout; bh=IcLOcJHXpDRidgL6yQ67Nz0XHts=; b=er5bvT6sv2F8pgAiFon6EAp3TGpCgGKBJ9p3hQwUde6S8gdUoM6AhZzQWELv/BGmt3gtw3hGxep0AFy/NkpTTgIFt8yGgluspE7yAnTQpJLko8oiIC6PNjHeaDSD8wMMLQ9XsPLOaECQsjlW75sbnJZO2xaH2eUlYvtHk3KpxVE= X-Sasl-enc: gkO3s5/FLvhlm6mGTQPnEoo9svMJ459qLfHZ/QEt9jco 1280817542 Received: from [192.168.0.2] (69.49.171.211.swcp.com [69.49.171.211]) by mail.messagingengine.com (Postfix) with ESMTPSA id 65A0C4AD62B for ; Tue, 3 Aug 2010 02:39:02 -0400 (EDT) Date: Tue, 3 Aug 2010 08:15:28 +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-1791650127-1280815973=:4144" Content-ID: X-Spam: no; 0.00; ocaml:01 conditionals:01 unreadable:01 mime-aware:01 sig:01 val:01 val:01 struct:01 printf:01 printf:01 variants:01 lukasz:01 typecheck:01 assertion:01 bug: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-1791650127-1280815973=:4144 Content-Type: TEXT/PLAIN; CHARSET=ISO-8859-1; FORMAT=flowed Content-Transfer-Encoding: QUOTED-PRINTABLE Content-ID: =09I had someone point out that add (`Meters, 0.5) (`Feet, 0.5);; will type check by instantiating 'a as [`Feet | `Meters]. Hiding the type= =20 in a module may fix the example: type units=3D[`Feet | `Meters];; let unit_to_string=3Dfunction | `Feet -> "ft" | `Meters -> "m" ;; module Units : sig type t val to_feet : float -> [`Feet]*t val to_meters : float -> [`Meters]*t val add : ([ 'a -> 'a val print : [ unit end =3D struct type t=3Dfloat let to_feet x=3D`Feet,x;; let to_meters x=3D`Meters,x;; let add (u,x) (_,y) =3D u,x +. y;; let print (u,x)=3DPrintf.printf "%f (%s)" x (unit_to_string u);; end Then, expressions as the one above can not be written. Joe On Tue, 3 Aug 2010, Joseph Young wrote: > =09I appreciate the reply and the suggestions. After looking over your= =20 > responses, could everything be simplified by removing the phantom types? = In=20 > 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 contai= n=20 > only a single value? > > Joe > > On Mon, 2 Aug 2010, bluestorm wrote: > >> Two remarks on Lukasz suggestion : >>=20 >> > =A0 =A0 val add : 'a t -> 'a t -> 'a t >> > [..] >> > =A0 =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. >>=20 >>=20 >> >> On Mon, Aug 2, 2010 at 9:49 AM, Lukasz Stafiniak >> wrote: >> > =A0 =A0 val print : 'a t -> unit >> > [..] >> > =A0 =A0 type 'a t =3D 'a * float >> > =A0 =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. >>=20 > --0-1791650127-1280815973=:4144--