Re: [Caml-list] Re: '_a

[skaller <skaller@users.sourceforge.net>]

On Fri, 2005-01-28 at 01:13, Vincenzo Ciancia wrote:
> skaller wrote:
> 
> > An exception free implementation of List.hd would
> > always produce the correct typing:
> > 
> > let hd x = function
> > | [] -> None
> > | h :: _ -> Some h
> > 
> > In effect, Ocaml first pretends unsound typing is actually sound,
> > and then enforces this at run time by throwing an exception
> > where one would otherwise accuse the type system of unsoundness,
> > but claims the error is not a type error.
> 
> What about the possibility to include possible exceptions into a function
> signature (a la java)? Does this have problems with type inference? 

Well I doubt the Java technique is any more meaningful
than the C++ one. There are three meanings of exceptions:

(a) the function domain was mis-specified, there is actually
an unstated constraint on it: the correct signature
for division is:

	divide: integer - { 0 } -> integer

(b) the codomain is mis-specified, we actually have

	List.hd: 'a list -> Some 'a

but enforce codomain 'a instead by throwing in the None case

(c) The function depends on some complex details
not considered part of the program, which can fail,
for example status of a file.

Documenting the exception instead of the constraint
on the signature doesn't seem very nice.

> Also,
> there is the ocamlexc tool:
> 
> http://caml.inria.fr/ocamlexc/ocamlexc.htm
> 
> what about it? 
> 

If I recall, this is a superb tool backed by some very smart
theory -- but in practice the output is extremely hard
to interpret.

Exceptions are often used where the constraint is expected
to be satisfied -- I myself say:

	.. Hashtbl.find table key ...

without any try/with wrapper when I 'know' the key is in
the table, and I may write 

	.. List.hd l ...

instead of 

	match l with | [] -> assert false | h :: _ -> h

However these uses of cast 'magic' are distinct from
alternate returns, where one sometimes has to cheat
the type system in the opposite direction, adding a dummy
value to code that will never be used just to get the type
right:

let x = 
	let rec f l -> | [] -> raise Not_found 
	| h :: t -> if h == v then (raise Found; 0) else f t
	in try f l with Found -> 1 | Not_found -> 2
in print_endline (string_of_int x)
;;

where the compiler doesn't know f l cannot return,
so it needs a useless '0' after the Found case
to get the typing correct. (Or you could add it after 
the 'try f l', either way it's equivalent to a safe use
of Obj.magic, safe since the cast will never be applied).

I guess some of these cases would be better handled
with a monadic technique, static exceptions, or just
doing the nasty testing: in many ways, exceptions
are *worse* than gotos, since at least the latter
in ISO C require the target to be visible.

BTW: Felix actually uses goto to replace exceptions,
and makes you pass handler into the code if necessary:

	proc error() { goto endoff; }
	fun g(e:unit->void) { ... error(); ... }
	...
	endoff:> // error found ..

Thus if you can't see the handler target in the code,
you can pass a closure which can. This guarrantees
you cannot fail to catch an exception. It is still
flawed though.

-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net