define incompatible type

define incompatible type

[Grégoire Seux]

[-- 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 --]

Re: [Caml-list] define incompatible type

[David Rajchenbach-Teller]

[-- 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 --]

Re: [Caml-list] define incompatible type

[Grégoire Seux]

[-- 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 --]

RE: [Caml-list] define incompatible type

[David Allsopp]

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

Re: [Caml-list] define incompatible type

[Guillaume Yziquel]

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/

Re: [Caml-list] define incompatible type

[abau]

On Fri, 12 Feb 2010 13:13:33 +0530
Grégoire Seux <kamaradclimber@gmail.com> wrote:

> too bad it does not exist !

>From ocaml language definition:

> The optional type equation "= typexpr" makes the defined type
> equivalent to the type expression "typexpr" on the right of the "="
> sign: one can be substituted for the other during typing.

When "type foo = int" then foo is just a type alias for int and
therefor it can/will be substituted by int.

_____________________________________________
HTWK Leipzig FbIMN Webmail, https://webmail.imn.htwk-leipzig.de