[Caml-list] Phantom types
Thomas Braibant
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...@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...@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
>
_______________________________________________
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
Rabih CHAAR
type s= {l:float}
followed by
type 'a t = s
everything goes well
I am unable to give you an explanation about this (the need of the
intermediay type s). I hope someone can shed some light on this.
Sincerely
Thomas Braibant <thomas....@gmail.com>
Sent by: caml-lis...@yquem.inria.fr
17/05/10 04:59 PM
Subject
[Caml-list] Phantom types
Hi list,
type p1
type p2
Any thoughts ?
thomas
*************************************************************************
This message and any attachments (the "message") are confidential, intended solely for the addressee(s), and may contain legally privileged information.
Any unauthorised use or dissemination is prohibited. E-mails are susceptible to alteration.
Neither SOCIETE GENERALE nor any of its subsidiaries or affiliates shall be liable for the message if altered, changed or
falsified.
************
Ce message et toutes les pieces jointes (ci-apres le "message") sont confidentiels et susceptibles de contenir des informations couvertes
par le secret professionnel.
Ce message est etabli a l'intention exclusive de ses destinataires. Toute utilisation ou diffusion non autorisee est interdite.
Tout message electronique est susceptible d'alteration.
La SOCIETE GENERALE et ses filiales declinent toute responsabilite au titre de ce message s'il a ete altere, deforme ou falsifie.
*************************************************************************
Philippe Veber
not a type definition. I don't know about the actual typing rules but this
would be reasonable, I guess.
Philippe.
2010/5/17 Rabih CHAAR <rabih...@lyxor.com>
>
> if you define the intermediate type
> type s= {l:float}
> followed by
> type 'a t = s
> everything goes well
>
> I am unable to give you an explanation about this (the need of the
> intermediay type s). I hope someone can shed some light on this.
>
> Sincerely
>
>
>
> *Thomas Braibant <thomas....@gmail.com>*
Dawid Toton
> type 'a t = {l: float}
>
I think the crucial question is when new record types are born. Here is
my opinion:
The "=" sign in the above type mapping definition is what I would call
"delayed binding". "Early binding" would be equivalent to
type tmp = {lab : float}
type 'a s = tmp
(evaluate the right-hand side first, then define the mapping).
The "early binding" creates only one record type, so lab becomes
ordinary record label.
In the given example of the "delayed binding" the t becomes a machine
producing new record types.
Hence, the identifier l is not an ordinary record label. It is shared by
whole family of record types. We can see it this way:
# type 'a t = { la : float } ;;
type 'a t = { la : float; }
# {la = 0.};;
- : 'a t = {la = 0.}
So OCaml interpreter doesn't know the exact type of the last expression,
but it is clever enough to give it a generalized type.
We can use la to construct records of incompatible types:
# type 'a t = { la : float } ;;
type 'a t = { la : float; }
# let yy = ({la = 0.} : int t) ;;
val yy : int t = {la = 0.}
# let xx = ({la = 0.} : string t);;
val xx : string t = {la = 0.}
# xx = yy;;
Error: This expression has type int t but an expression was expected of type
string t
I suppose my jargon may be not mainstream, apologies.
Dawid
Goswin von Brederlow
> 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*)
This is actualy a problem, at least for me. Because that is a type error
you usualy want to specifically catch through the use of phantom types.
But ocaml knows that 'a t = float and all floats are compatible. So it
accepts all 'a t as the same.
To make the phantom type checking work for you you need to move the
definition of your phantom type into a submodule and make the type
abstract through its signature. Any functions converting from one 'a t
to 'b t also need to be in there. To avoid having to use the submodule
name all the time you can use something like
module M : sig type 'a t = private float val make : float -> 'a t end = struct
type 'a t = float
let make f = f
end
include M
# let x : p1 t = make 0.0;;
val x : p1 t = 0.
# let id : p2 t -> p2 t = fun x -> x;;
val id : p2 t -> p2 t = <fun>
# let _ = id x;;
Error: This expression has type p1 t = p1 M.t
but an expression was expected of type p2 t = p2 M.t
The "private" tells the type system that nobody (outside the module) is
to create a value of that type. Only inside the module, where the type
isn't private can you create one.
> 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 *)
Why it works correctly here is explained nicely in the other mailss in
this thread.
> Any thoughts ?
>
> thomas
MfG
Goswin