From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 3F762BC57 for ; Mon, 2 Aug 2010 10:03:02 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArQCAJkYVkzRVdY2mGdsb2JhbACgCQgVAQEBAQEICQwHESKlSYkEghCFIy6IVAEBAwWFNASIf4JLhSA X-IronPort-AV: E=Sophos;i="4.55,302,1278280800"; d="scan'208";a="67196675" Received: from mail-bw0-f54.google.com ([209.85.214.54]) by mail4-smtp-sop.national.inria.fr with ESMTP; 02 Aug 2010 10:03:01 +0200 Received: by bwz12 with SMTP id 12so2155209bwz.27 for ; Mon, 02 Aug 2010 01:03:01 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:mime-version:sender:received :in-reply-to:references:from:date:x-google-sender-auth:message-id :subject:to:cc:content-type:content-transfer-encoding; bh=Fs6HjH73htxj9rKO/sFxBhV/0e3vZqZDw8CzKgIdf5A=; b=p+g2RBiY6FOIy3FxH/8QEt2icE5FcL2fgwUAntXryvQfsh1wrc6nisHsex2MaloMHe ajQ3xngRIKCA4nrX91JtCY/82b9WJSBO4ARfEBZj5O7auz079YcvMobMrVb3NfgX+aTr SnYdp9UfieEFLVjtz4sFk80kgMd5ykYxxZxVE= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type :content-transfer-encoding; b=CiqRvAWPMtZofzhHMmb9/jG6oQoCeyBLblA6/APKdiu2RvwEHtBw9tVeOX1f8E9sFy yS2ycu6tmghJNidQ6HpRBm+b71THSuB+qqzSIU53Hv9fgTOM4EWOzV4VPj6nEPARCcSF c58rFnkOTXFoTHsZoCf+1DrQ8K/FRvuFenZEE= Received: by 10.204.33.86 with SMTP id g22mr3970013bkd.26.1280736181458; Mon, 02 Aug 2010 01:03:01 -0700 (PDT) MIME-Version: 1.0 Sender: gabriel.scherer@gmail.com Received: by 10.204.22.82 with HTTP; Mon, 2 Aug 2010 01:02:41 -0700 (PDT) In-Reply-To: References: From: bluestorm Date: Mon, 2 Aug 2010 10:02:41 +0200 X-Google-Sender-Auth: ldF1ntJLnoNuslhmUqWeJ-5lkkA Message-ID: Subject: Re: [Caml-list] Conditionals based on phantom types To: Lukasz Stafiniak Cc: Joseph Young , caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; conditionals:01 lukasz:01 val:01 typecheck:01 assertion:01 bug:01 lukasz:01 val:01 printf:01 printf:01 runtime:01 sig:01 struct:01 runtime:01 polymorphic:01 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 wrote= : > =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.