Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Re: RE: reference initialization
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: bdb-as-camluser@n...
Subject: Re: RE: reference initialization
Hello, wrote:
) type 'a ptr = a' option ref
) exception NullPointer
) let new () = ref None
) let get x = match !x with Some y -> y | None -> raise NullPointer
) let set x y = x := Some y 
) ML, of course, lacks the syntactic support to use these pointers as
) gracefully as Java can. On the other hand, the problem with _Java_ is
) efficiency loss, as the programmer cannot syntactically enforce that the
) reference is initialized -- requiring a null check at every use.

Well, I am sorry but 'get' is also performing a null check at every use, isn't it?

To me, neither approach (ML/Java/C) is satisfying. I have the strong feeling that the _only_ way that maximum efficiency and safeness can be achieved is to let the programmer specify _proofs_ of safeness when it is not obvious at the syntaxic or type level.

Are there any languages in which the programmer can indicate proofs of safeness (regardless of fitness for a particular purpose) of the program he is writing, and let the compiler use these proofs?

Benoît de Boursetty.

----- La messagerie itinérante sans abonnement NetCourrier -----
Web :     Minitel : 3615 et 3623 NETCOURRIER
                  Tél : 08 36 69 00 21