Browse thread
Phantom types
- Thomas Braibant
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2010-05-17 (15:00) |
From: | Thomas Braibant <thomas.braibant@g...> |
Subject: | Phantom types |
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 = float let x : p1 t = 0.0 let id : p2 t -> p2 t = fun x -> x let _ = id x (* type checks with type p2 t*) type 'a t = {l: float} let x : p1 t = {l = 0.0} let id : p2 t -> p2 t = fun x -> x let _ = id x (* ill typed *) Any thoughts ? thomas 2010/5/1 Stéphane Lescuyer <stephane.lescuyer@inria.fr>: > 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 = {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 = {lin = Vec.origin; ang = Vec.origin } > > let double_force (v : force kinematic) : force kinematic = {lin = > Vec.mult 2. v.lin; ang = 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 = ... > > 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éphane L. > > On Sat, May 1, 2010 at 6:04 PM, Anthony Tavener > <anthony.tavener@gmail.com> wrote: >> I have this: >> >> type kinematic = { lin: Vec.t; ang: Vec.t } >> >> Which I've been using to represent a medley of physical attributes (force, >> 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: >> >> type position = { r: Vec.t; theta: Vec.t } >> type acceleration = { a: Vec.t; alpha: Vec.t } >> type force = { f: Vec.t; tau: Vec.t } >> >> They are structurally equivalent, and ideally I'd like to be able to treat >> these as 'kinematic' too, since that is how I would express the arithmetic >> 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 (though >> 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 what >> 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 inform >> 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 actually >> 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, so >> all common operations are duplicated for each new type. No performance hit. >> 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 apply >> on all the different types. I think this will add some overhead, since the >> signature of the types (below) would demand accessor functions for the >> record fields, in order to uniformly get the fields from the different types >> (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? >> >> module type KINEMATIC = sig >> type t >> val lin : t -> Vec.t >> val ang : t -> Vec.t >> end >> >> 3. Making all the other types different aliases of 'kinematic'; then using >> explicit type declarations in function parameters and coercion to >> 'kinematic' when needed. This makes some ugly code, and the added-typesafety >> is almost illusory. This is kind-of like 'typesafe' C code doing typecasting >> 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 comes >> with a big performance hit unless these functions became like >> type-coercions. If there is a way this can be done with zero runtime cost, >> 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 various >> channels. And thanks to those making the language I favor for most tasks! >> >> Briefly introducing myself: I've been a professional video-game developer >> for 15 years, most recently specializing in AI. I quit my last job almost >> 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... also >> 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 >