Phantom types

* Phantom types
@ 2010-05-17 14:59 Thomas Braibant
  2010-05-17 15:14 ` [Caml-list] Phantom types [NC] Rabih CHAAR
                   ` (2 more replies)
  0 siblings, 3 replies; 10+ messages in thread
From: Thomas Braibant @ 2010-05-17 14:59 UTC (permalink / raw)
  To: caml-list

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
>

^ permalink raw reply	[flat|nested] 10+ messages in thread