Re: [Caml-list] Phantom types [NC]

[Philippe Veber <philippe.veber@googlemail.com>]

[-- Attachment #1: Type: text/plain, Size: 10518 bytes --]

It seems that the expressions typecheck when t is a type abbreviation and
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.chaar@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.braibant@gmail.com>*
> Sent by: caml-list-bounces@yquem.inria.fr
>
> 17/05/10 04:59 PM
>    To
> caml-list@yquem.inria.fr
> cc
>   Subject
> [Caml-list] 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
> >
>
> _______________________________________________
> 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
>
> *************************************************************************
> 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.
> *************************************************************************
>
>
> _______________________________________________
> 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
>
>

[-- Attachment #2: Type: text/html, Size: 14815 bytes --]