On Tue, 2005-11-08 at 16:04 -0600, Brian Hurt wrote:

> Yes.  For example, Ocaml will reject this code:
>  	let f n =
>  		if (n > 0) && (is_prime (2*n)) then
>  			"bad idea"
>  		else
>  			false
>  	;;
> 
> despite the fact that "bad idea" will never, ever be returned (given the 
> obvious definition of is_prime, anyways).

This is an interesting case, IMHO. A related case arose
in C++ and was discussed by the committee: something like:

	int x = 1/0;

The question was: is the compiler allowed to reject the program?

I believe the current answer is: IF the compiler can prove
that this code will necessarily be executed, then the behaviour
of the program is undefined anyhow, and so the compiler is allowed
to reject the program -- but it is NOT required to.

However, IF the compiler cannot prove the code will be executed,
then it must compile the program.

The interesting thing is that 1/0 is a 'constant expression'.
However this is not:

	int a = 0; int b = 1;
	int c = b/a;

In Felix, certain constructions are *required* to be optimised
at compile time. In particular,

	1/0

is a 'constant expression' and MUST be calculated at compile time.
However, as above, the compiler is not allowed to reject the program,
just because a constant expression cannot be calculated -- it has
to generate code that aborts the program or something, in case that
expression is never elaborated (this was a pain to get right,
and probably isn't yet)

In particular this is perfectly legal Felix:

	if true then 1 else 1/0 endif

and is REQUIRED to reduce to 1. Similarly:

	if true then 1 else "Hello" endif

is perfectly legal. The 'if/then/else/endif' construction
is being reused as a macro processing construction: there
is no type error here.

So .. it all depends on exactly how the language is specified.

BTW: I am not sure I like these preprocessor reduction rules.
The idea was to 'get rid' of #if style conditional compilation.
Without these kinds of rules, constant folding is effectively
impossible.

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net