From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr 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 53EE9BBAF for ; Mon, 17 May 2010 17:00:13 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvIEABX38EvRVdvhe2dsb2JhbACRUYwoCBUBARYiAx+rWoIAhQwuiE4BAQMFhQsE X-IronPort-AV: E=Sophos;i="4.53,247,1272837600"; d="scan'208";a="62955603" Received: from mail-ew0-f225.google.com ([209.85.219.225]) by mail4-smtp-sop.national.inria.fr with ESMTP; 17 May 2010 17:00:12 +0200 Received: by ewy25 with SMTP id 25so1731240ewy.7 for ; Mon, 17 May 2010 08:00:12 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:mime-version:received:from:date :message-id:subject:to:content-type:content-transfer-encoding; bh=dKfNVHwLxFd8KmuotMrF7rDLxSuwhNDVWQ+LiU9xwcc=; b=bjYNY/y0L3Jw+nyOVon4m9Mf+S90YGiOlwQJawcFYEPyM8nNCAeFRxuE3zNET7qK8x vLGchqUtAK2lSY4CvB3R6FdwHOerVRzYVW6EGCsVhZEXI/vOOz6dffNInQarYolsJNNI fhT+vjVrzZLdpH4Q1KL4iw/3GglUHcdGG+dvs= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:from:date:message-id:subject:to:content-type :content-transfer-encoding; b=bIlrowmEHl4jc9AK/Rpj1QyyHJdroRLu6Y7N7qrZXpAaRWI2cxIY3QbaFejw6Ww5gc y/I3WsKmtSD+zfnW/2UzSaahI2DoL33kCfyDU2/IokqOA0TiXV5von5jFi1kbA9uU/8z BBrF2spgibvx8Jr822/SYdPx5VdJyXOHZuvRM= Received: by 10.213.51.138 with SMTP id d10mr2364436ebg.75.1274108412153; Mon, 17 May 2010 08:00:12 -0700 (PDT) MIME-Version: 1.0 Received: by 10.213.3.74 with HTTP; Mon, 17 May 2010 07:59:52 -0700 (PDT) From: Thomas Braibant Date: Mon, 17 May 2010 16:59:52 +0200 Message-ID: Subject: Phantom types To: caml-list@yquem.inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; subtyping:01 acceleration:01 annotations:01 mult:01 multiplying:01 explicitely:01 annotations:01 constructors:01 runtime:01 acceleration:01 structurally:01 ocaml:01 subtypes:01 subtypes:01 structurally:01 Hi list, Following on the thread "Subtyping structurally-equivalent records, or something like it?", I made some experimentations with phantom types. Unfortunately, I turns out that I do not understand the results I got. Could someone on the list explain why the first piece of code is well typed, while the second one is not ? type p1 type p2 type 'a t =3D float let x : p1 t =3D 0.0 let id : p2 t -> p2 t =3D fun x -> x let _ =3D id x (* type checks with type p2 t*) type 'a t =3D {l: float} let x : p1 t =3D {l =3D 0.0} let id : p2 t -> p2 t =3D fun x -> x let _ =3D id x (* ill typed *) Any thoughts ? thomas 2010/5/1 St=E9phane Lescuyer : > Hi Anthony, > I think that maybe using phantom types could do the trick : consider > defining empty types for all the different "kinds" of similar > constructs that you have, and then define the kinematic record with a > phantom parameter type. > > type position > type acceleration > type force > > type 'a kinematic =3D {lin : Vec.t; ang: Vec.t} > > By adding some extra typing annotations, you can then constraint your > functions to accept (or produce) only a given kind of construct, say > for example a position kinematic : > > let pos_0 : position kinematic =3D {lin =3D Vec.origin; ang =3D Vec.origi= n } > > let double_force (v : force kinematic) : force kinematic =3D {lin =3D > Vec.mult 2. v.lin; ang =3D v.ang } > > double_force pos_0 -> does not type check > > You can write generic functions as add, norm, products, etc : they are > just polymorphic with respect to the phantom type parameter. By the > way you ensure that you are not multiplying apples and carrots : > let plus (v : 'a kinematic) (v' : 'a kinematic) : 'a kinematic =3D ... > > Of course, the overhead is that you have to explicitely write some > type annotations, especially for constructors, but the runtime > overhead is exactly 0. And also, one limitation is that you can't use > different projection names for the different cosntructs, since it is > really always the same record type that you are using. > > I hope this helps, > > St=E9phane L. > > On Sat, May 1, 2010 at 6:04 PM, Anthony Tavener > wrote: >> I have this: >> >> =A0 type kinematic =3D { lin: Vec.t; ang: Vec.t } >> >> Which I've been using to represent a medley of physical attributes (forc= e, >> momentum, velocity, etc.). >> >> As the physics code becomes increasingly substantial I'm running into >> possible human-error, like passing a momentum where a force is expected,= or >> a mass instead of inverse-mass (mass is also a record though different, = but >> inv-mass has the same structure as mass). So I'd like to make distinct >> types, such as: >> >> =A0 type position =3D { r: Vec.t; theta: Vec.t } >> =A0 type acceleration =3D { a: Vec.t; alpha: Vec.t } >> =A0 type force =3D { f: Vec.t; tau: Vec.t } >> >> They are structurally equivalent, and ideally I'd like to be able to tre= at >> these as 'kinematic' too, since that is how I would express the arithmet= ic >> and common functions on these types (add, mul, etc). >> >> >> I'm sure I've seen posts on this before but I can't find them now (thoug= h >> what I remember are questions about having distinct 'float' types, such = as >> for degrees vs radians, rather than records). >> >> I know OCaml doesn't have subtypes for records, which is effectively wha= t >> I'm looking for. Though this case is a bit more specialized that that...= all >> the subtypes and base type are structurally equivalent. Code for one of >> these types would technically work on any... but is there a way to infor= m >> the type system of my intentions? >> >> >> I hope someone has a better option than those I've considered, or that I >> have a grave misunderstanding somewhere and one of these options is actu= ally >> good: >> >> 1. Objects. Subtyping makes these a natural fit, but in this case I don'= t >> need anything else which objects provide, and a certainly don't need the >> poor performance or method-calling mixed in with my computational code >> (aesthetically... yucky, to me). Again, each type is structurally >> equivalent. Just some functions want certain types. >> >> 2. Using distinct records for each type, but no 'kinematic' base type, s= o >> all common operations are duplicated for each new type. No performance h= it. >> But the redundant code is horrible -- makes extensions a pain, and a >> potential bug-source. >> >> 2b. Same as above, but putting the common code in a functor which we app= ly >> on all the different types. I think this will add some overhead, since t= he >> signature of the types (below) would demand accessor functions for the >> record fields, in order to uniformly get the fields from the different t= ypes >> (again, even though they are structurally equivalent) -- these calls >> probably wouldn't get optimized out. But maybe there is a better way to = do >> this? >> >> =A0 module type KINEMATIC =3D sig >> =A0=A0=A0 type t >> =A0=A0=A0 val lin : t -> Vec.t >> =A0=A0=A0 val ang : t -> Vec.t >> =A0 end >> >> 3. Making all the other types different aliases of 'kinematic'; then usi= ng >> explicit type declarations in function parameters and coercion to >> 'kinematic' when needed. This makes some ugly code, and the added-typesa= fety >> is almost illusory. This is kind-of like 'typesafe' C code doing typecas= ting >> gymnastics. >> >> 4. Adapter functions: 'kinematic_of_force: force -> kinematic', etc. as = a >> way to use the common set of 'kinematic' functions. This is clunky and c= omes >> with a big performance hit unless these functions became like >> type-coercions. If there is a way this can be done with zero runtime cos= t, >> I'd accept the clunkiness. :) >> >> Any thoughts? >> >> >> I've been using OCaml for a few years now, but this is my first post. I = feel >> many of you are familiar online personae through reading archives, blogs= , >> and websites. Thank-you for all the help I've absorbed through those var= ious >> channels. And thanks to those making the language I favor for most tasks= ! >> >> Briefly introducing myself: I've been a professional video-game develope= r >> for 15 years, most recently specializing in AI. I quit my last job almos= t >> two years ago to travel and program (95% in OCaml!), and am developing a >> game now. I've seen indications over the years of other game developers >> taking the plunge and then parting ways with OCaml, surely back to C++. = I >> see OCaml as viable and certainly more pleasurable, even with avoiding >> mutation. But within a pressure-cooker environment (working for $$ from >> someone else) people fall back on what they are most familiar with... al= so >> you can't go too rogue while still being part of a team. :) >> >> -Anthony Tavener >> >> _______________________________________________ >> Caml-list mailing list. Subscription management: >> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list >> Archives: http://caml.inria.fr >> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners >> Bug reports: http://caml.inria.fr/bin/caml-bugs >> >> > > > > -- > I'm the kind of guy that until it happens, I won't worry about it. - > R.H. RoY05, MVP06 > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs >