Fernando Alegre wrote:
> > permission and back.  And automatically generated runtime checks to
> > ensure that you don't try to convert ( 37 :> permission ).  1 remains an
>
> No, no. Run-time checks are evil :-) I mean, OCaml is supposed to be
> a static type-safe system, so that programs that typecheck are guaranteed
> to run (maybe forever...) and never segfault.

This isn't a runtime type-check - it's a runtime domain check and it's
necessary in the absence of a much more exotic type system that includes
information on the domain and range of a function as well as it's "raw"
type. Getting an int from a permission is an error-free process (because all
permissions are ints) but getting a permission from an int can fail because
only some ints are permissions. You need to have a runtime check (or a proof
- which isn't how O'Caml works) that the int is valid. Spotting and
eliminating conversion of constants would of course be a good compiler
optimisation but permission_of_int (or whatever conversion construct you
came up with) would need to raise an exception on invalid input.
 
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).


David