* define incompatible type
@ 2010-02-12 6:32 Grégoire Seux
2010-02-12 7:33 ` [Caml-list] " David Rajchenbach-Teller
0 siblings, 1 reply; 5+ messages in thread
From: Grégoire Seux @ 2010-02-12 6:32 UTC (permalink / raw)
To: caml-list
[-- Attachment #1: Type: text/plain, Size: 430 bytes --]
hello !
i would like to create two types and use the type checker to verify the
"meaning" of my programs:
type user_id = int
type movie_id = int
i'd like if the type checker would warn me if i write something that is
non-sense:
> let a:user_id = 57 and b:movie_id = 80 in
if a=b then ...
because this is obvioulsy a mistake
do you know if is this possible ?
thanks by advance !
--
Grégoire
[-- Attachment #2: Type: text/html, Size: 1477 bytes --]
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [Caml-list] define incompatible type 2010-02-12 6:32 define incompatible type Grégoire Seux @ 2010-02-12 7:33 ` David Rajchenbach-Teller 2010-02-12 7:43 ` Grégoire Seux 2010-02-12 10:59 ` David Allsopp 0 siblings, 2 replies; 5+ messages in thread From: David Rajchenbach-Teller @ 2010-02-12 7:33 UTC (permalink / raw) To: Grégoire Seux; +Cc: caml-list [-- Attachment #1: Type: text/plain, Size: 2249 bytes --] Hi Grégoire, It's not directly possible in OCaml, but there are at least three methods for doing what you want. The first one is to wrap your integers behind a constructor, e.g. type user_id = User of int type movie_id = Movie of int let a = User 57 and b = Movie 80 in if a = b then ... This is the technique often used by Haskellites. Variant on the topic: use singleton records instead of singleton sums. The second one is to make use of modules and abstract types, e.g. module User = struct type id = int let id_of_int x = x ... end : sig type id (*Abstract type*) val id_of_int : int -> id end (*same for b*) let a = User.id_of_int 57 and b = User.id_of_int 80 in if a = b then ... This is probably the most common technique in OCaml, as it fits well with functorization. Finally, you can use a phantom type, e.g. type 'a id = {id: int} (*Type argument used only to differentiate between various kinds of ids*) type user (*This type has no inhabitant, don't worry, it's only for coercions*) type movie (*same here*) let a = {id:57} : user id and b = {id:80}: movie id in if a = b then ... It's an elegant technique, which I personally like, but which can sometimes cause puzzling error messages if you forget coercions. I hope this helps, Regards, David On Feb 12, 2010, at 7:32 AM, Grégoire Seux wrote: > hello ! > > i would like to create two types and use the type checker to verify the "meaning" of my programs: > > type user_id = int > type movie_id = int > > i'd like if the type checker would warn me if i write something that is non-sense: > let a:user_id = 57 and b:movie_id = 80 in > if a=b then ... > > because this is obvioulsy a mistake > > do you know if is this possible ? > thanks by advance ! > > > -- > Grégoire > _______________________________________________ > 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: 4594 bytes --] ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [Caml-list] define incompatible type 2010-02-12 7:33 ` [Caml-list] " David Rajchenbach-Teller @ 2010-02-12 7:43 ` Grégoire Seux 2010-02-12 10:59 ` David Allsopp 1 sibling, 0 replies; 5+ messages in thread From: Grégoire Seux @ 2010-02-12 7:43 UTC (permalink / raw) To: David Rajchenbach-Teller; +Cc: caml-list [-- Attachment #1: Type: text/plain, Size: 92 bytes --] Thanks for your answer, i think i will try with the second one. too bad it does not exist ! [-- Attachment #2: Type: text/html, Size: 107 bytes --] ^ permalink raw reply [flat|nested] 5+ messages in thread
* RE: [Caml-list] define incompatible type 2010-02-12 7:33 ` [Caml-list] " David Rajchenbach-Teller 2010-02-12 7:43 ` Grégoire Seux @ 2010-02-12 10:59 ` David Allsopp 2010-02-12 20:26 ` Guillaume Yziquel 1 sibling, 1 reply; 5+ messages in thread From: David Allsopp @ 2010-02-12 10:59 UTC (permalink / raw) To: 'David Rajchenbach-Teller', 'Grégoire Seux' Cc: 'caml-list' David Rajchenbach-Teller wrote: > Hi Grégoire, > It's not directly possible in OCaml, but there are at least three methods for doing what you > want. > > The first one is to wrap your integers behind a constructor, e.g. <snip> You can also use (post OCaml 3.11.0) private types if you want to be able to use the ID values as integers but only explicitly. While I'm sure that the ocaml compiler eliminates calls to the identity function, I like the elegance that the conversion from id to int is a type coercion instead of a function call. In real world uses, chances are that of_int is a useful function doing actual work and not the identity function! module User : sig type id = private int val of_int : int -> id end = struct type id = int let of_int x = x end;; let a = User.of_int 57 and b = User.of_int 57;; a = b;; (* true *) a = 57;; (* type error *) (a :> int) = 57;; (* true *) David ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [Caml-list] define incompatible type 2010-02-12 10:59 ` David Allsopp @ 2010-02-12 20:26 ` Guillaume Yziquel 0 siblings, 0 replies; 5+ messages in thread From: Guillaume Yziquel @ 2010-02-12 20:26 UTC (permalink / raw) To: David Allsopp Cc: 'David Rajchenbach-Teller', 'Grégoire Seux', 'caml-list' David Allsopp a écrit : > David Rajchenbach-Teller wrote: >> Hi Grégoire, >> It's not directly possible in OCaml, but there are at least three methods > for doing what you >> want. >> >> The first one is to wrap your integers behind a constructor, e.g. > > <snip> > > You can also use (post OCaml 3.11.0) private types if you want to be able to > use the ID values as integers but only explicitly. Private types is indeed the way to go. For instance, imagine that you have value wrapping C pointers. You may want to declare something like: > type pointer > type type_1 = private pointer > type type_2 = private pointer When you write your code, you essentially use only types type_1 and type_2. The type inference system won't look into the "private" part of the type, so the type checker will cough on something like > function (x : type_1) (y : type_2) -> x = y But, you can subtype (i.e. use :> to tell the typechecker to use the private declaration). And this will be valid OCaml: > function (x : type_1) (y : type_2) -> (x :> pointer) = (y :> pointer) -- Guillaume Yziquel http://yziquel.homelinux.org/ ^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2010-02-12 20:25 UTC | newest] Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2010-02-12 6:32 define incompatible type Grégoire Seux 2010-02-12 7:33 ` [Caml-list] " David Rajchenbach-Teller 2010-02-12 7:43 ` Grégoire Seux 2010-02-12 10:59 ` David Allsopp 2010-02-12 20:26 ` Guillaume Yziquel
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).