Re: [Caml-list] Compiler feature - useful or not?

[Fernando Alegre <fernando@gatech.edu>]

On Fri, Nov 16, 2007 at 07:18:18PM -0000, David Allsopp wrote:

> optimisation but permission_of_int (or whatever conversion construct you
> came up with) would need to raise an exception on invalid input.

And that is why "permission_of_int" would not be considered part of
the core language.

However, things like what I proposed earlier, such as

(x :> n finite), whenever x and n are known at compile-time

or

(int :> even), if the encoding of an even number 2*n is given by n

will never raise an exception, are sound and could be part of the core
language. The first case is straightforward, but extending it safely
(i.e. no code, only type equations) is not obvious. The second case
needs some way to specify the encoding along with a proof that it is
sound, and this is not trivial either. However, both extensions seem
theoretically possible and in line with the philosophy of the Caml type
system.

> Consider string_of_int (error-free - all ints can be represented as strings)
> vs. int_of_string which raises an exception if the string is not a
> recognised representation of an int.
> 
> > While exceptions are needed for I/O, no core expression should raise an
> > exception.
> 
> compare = compare;;
> 
> (though cf. SML equality types)
> 
> Good code using permission_of_int (as with good code using int_of_string)
> would ensure that the int is valid before ever calling permission_of_int but
> the permission_of_int itself needs to be able to raise the exception to
> fulfil the contract of its type (int -> permission).

Exactly. And that is the reason why, IMHO, we may never see such an
extension to OCaml language, since it is primarily a research language
for type checking. (And so run-time "usefulness", or hacks, are
secondary to the OCaml team.)

Thanks,
Fernando