From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 75218BC57 for ; Wed, 4 Aug 2010 05:05:02 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhABAAZ1WExCbwQZkWdsb2JhbACTQIxcFQEBAQEHDQoHEQQew1IFhTk X-IronPort-AV: E=Sophos;i="4.55,313,1278280800"; d="scan'208";a="65011955" Received: from out1.smtp.messagingengine.com ([66.111.4.25]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 04 Aug 2010 05:05:01 +0200 Received: from compute2.internal (compute2.internal [10.202.2.42]) by gateway1.messagingengine.com (Postfix) with ESMTP id 2FC7B1A2EBA for ; Tue, 3 Aug 2010 23:04:55 -0400 (EDT) Received: from heartbeat1.messagingengine.com ([10.202.2.160]) by compute2.internal (MEProxy); Tue, 03 Aug 2010 23:04:55 -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=/lQgUTcP3F7VypdQqVTeRIfIr+U=; b=D+84Fvnwp7+yyxUoupxKngZkAD2Ta8jxaPWcb/Ti+utgaeUEFlc1oJ6rQ4Gfwgmm7AVMU1NV9BjSOoPcwiiCvSjixP6XnlxdhX8SN28AOYrqbT4sqKfkxt3uEpOdBChWvij0TRZJTHpcmGNNGpMc44wa8CssjakiV2URo8RI+zA= X-Sasl-enc: EveyMDr/BRQQBx7M4K3xiTAe7iun3jO+CU+r2/LGCZWw 1280891094 Received: from [192.168.0.2] (69.49.171.211.swcp.com [69.49.171.211]) by mail.messagingengine.com (Postfix) with ESMTPSA id 913EA4E07FA for ; Tue, 3 Aug 2010 23:04:54 -0400 (EDT) Date: Wed, 4 Aug 2010 04:41:15 +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-297206644-1280889670=:7258" X-Spam: no; 0.00; ocaml:01 conditionals:01 unreadable:01 mime-aware:01 ocaml:01 sig:01 val:01 val:01 sig:01 struct:01 printf:01 printf:01 checker:01 checker: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-297206644-1280889670=:7258 Content-Type: TEXT/PLAIN; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: QUOTED-PRINTABLE On Tue, 3 Aug 2010, bluestorm wrote: > On Tue, Aug 3, 2010 at 8:15 AM, Joseph Young wrote: >> module Units : sig >> =A0 =A0type t >> =A0 =A0val to_feet : float -> [`Feet]*t >> =A0 =A0val to_meters : float -> [`Meters]*t >> [..] >> end > > With this type, the value representation of units is not abstract > anymore (and it is not very useful to have still t abstract). The user > can analyse the values you give him and access the unit member. This > is the difference with the ('a t) representation were the relation > between 'a and values is hidden outside the module. > > For example, your user can write something like that, wich could be > indesirable : > > let convert [ `Feet ] * Units.t -> [ `Meters ] * Units.t =3D > function (`Feet, t) -> (`Meters, t) > =09You are correct and that could be problematic. Combining the two=20 ideas from above gives: type units=3D[`Feet | `Meters];; let unit_to_string=3Dfunction | `Feet -> "ft" | `Meters -> "m" ;; module Units : sig type 'a t val to_feet : float -> ([`Feet] as 'a)*'a t val to_meters : float -> ([`Meters] as 'a)*'a t val add : (([ 'b -> 'b val print : ([ unit end =3D struct type 'a 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 which hopefully insures that the exposed and hidden unit are required to=20 be the same in order to use these functions. To be sure, functions such=20 as: let convert (u,x:[ `Feet ] * 'a Units.t) : [ `Meters ] * 'a Units.t =3D=20 `Meters,x are possible. However, I believe that the type checker should throw an=20 error if the above functions are called on converted values. Mostly, I'm= =20 trying to force the type checker to insure there are valid values without= =20 using runtime assertions as you suggested above. =09Thanks again for the help. Joe --0-297206644-1280889670=:7258--