Re: [Caml-list] '_a

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

On Thu, 2005-01-27 at 11:51, Jacques Garrigue wrote:

> There is no deep magic, no heuristics. There is just a type system
> which guarantees type soundness (i.e. "well typed programs cannot
> produce runtime type errors").

Unfortunately, 'soundness' as described is somewhat weaker
than one would like, since it depends on the expressivity
of the type system how useful soundness actually is.

Ocaml can still produce run time errors for situations
that 'should' have been considered type errors, except
the typing is not strong enough to allow it.

In the extreme, a fully dynamic type system in
which everything has type 'object' has a fully sound
static type system behind it, and there cannot be
any run time 'type' errors in the sense of 
the static type.

For less extreme circumstances, C++ programmers would
express surprise the typing is so weak that array length
is not part of an array type, so that a bounds violation
is technically not a type error in Ocaml whereas in a
language where the length was part of type information
the very same error would indicate unsound typing.

There are in fact quite a few incorrectly typed functions
as well, for example List.hd and List.tl can fail at 
run time, but this isn't considered a type error simply
because the function typing is actually wrong.

Thus, 'soundness' being ensured must be taken with a grain
of salt. The fact that 'well typed programs can't produce
runtime *type* errors' doesn't really tell you as much as
you'd like -- other errors can still occur which aren't
technically type errors, but in a less 'technical' interpretation
certainly are.

Exceptions are part of the evil here, since they permit
blatant uncontrolled lying about type. The 'real' type
of List.hd is

	hd: 'a list -> 'a option

considering it as a total function. The type

	hd: 'a stream -> 'a

is correct but only applies to streams, which lists are not.
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.

It isn't clear whether this trick is enough to say the type
system is genuinely sound. One could argue dereferencing
a null pointer in C is, or is not, a type error -- either
way it is a nasty error which can't be easily tracked down
except by 'binary chop' on your code with diagnostics,
or a debugger -- and Ocaml is no different in character
when you find your code terminated with an uncaught
Not_found exception.

[A really nasty one is that polymorphic compare is not
polymorphic .. it can't handle abstract types eg BigInt
or functions .. but you'll only find out at run time ..]

In practice, Ocaml really does help detect errors early
that weaker languages like C++ would not, so this isn't
a criticism so much as a warning: it is still possible
to have a significant number of 'technical' errors in
an Ocaml program (quite apart from just getting your
encoding of some algorithm entirely wrong) -- and it 
is easy to be lulled into a false sense of security by
the very fact the basic typing is both expressive and
sound.

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