Why doesn't ocamlopt detect a missing ; after failwith statement?

Why doesn't ocamlopt detect a missing ; after failwith statement?

[Richard Jones]

[-- Attachment #1: Type: text/plain, Size: 831 bytes --]


--------------------------------------------------------------- t.ml --
let () =
  if false then
    failwith "Failed ..." (* ; *)
  prerr_endline "OK"
----------------------------------------------------------------------

Compiled with ocamlopt.opt:

$ ocamlopt.opt t.ml
$ ./a.out 
$

(it prints nothing).  If I uncomment/add the ';', then it prints the
OK message:

$ ocamlopt.opt t.ml
$ ./a.out 
OK

All well and good, but I don't understand why it doesn't warn me about
the missing ';' in the first case.

Rich.

-- 
Richard Jones.  http://www.annexia.org/  http://www.j-london.com/
>>>   http://www.team-notepad.com/ - collaboration tools for teams   <<<
Merjis Ltd. http://www.merjis.com/ - improving website return on investment
http://execellence.co.uk/ - Interim and executive recruitment

[-- Attachment #2: Digital signature --]
[-- Type: application/pgp-signature, Size: 189 bytes --]

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Nicolas Cannasse]

> All well and good, but I don't understand why it doesn't warn me about
> the missing ';' in the first case.

val failwith : string -> 'a

so failwith "error" prerr_endline "OK";

is a valid call since 'a unify with (string -> unit) -> string -> unit

Nicolas

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[skaller]

On Fri, 2004-11-26 at 08:14, Nicolas Cannasse wrote:
> > All well and good, but I don't understand why it doesn't warn me about
> > the missing ';' in the first case.
> 
> val failwith : string -> 'a
> 
> so failwith "error" prerr_endline "OK";
> 
> is a valid call since 'a unify with (string -> unit) -> string -> unit

.. a problem which could not occur were there a void type
which couldn't unify with 'a, and prerr_endline had
type string-> void.

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

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Jacques Garrigue]

From: skaller <skaller@users.sourceforge.net>
> On Fri, 2004-11-26 at 08:14, Nicolas Cannasse wrote:
> > > All well and good, but I don't understand why it doesn't warn me about
> > > the missing ';' in the first case.
> > 
> > val failwith : string -> 'a
> > 
> > so failwith "error" prerr_endline "OK";
> > 
> > is a valid call since 'a unify with (string -> unit) -> string -> unit
> 
> .. a problem which could not occur were there a void type
> which couldn't unify with 'a, and prerr_endline had
> type string-> void.

But by definition 'a unifies with everything, including your void
type, or you get a noncommutative notion of unification...

The real problem here is the type of failwith, which is not
informative enough. Or to be more precise, it is informative enough,
but for this you must realize that 'a occurs only once, and so that
any further application is meaningless. The type checker is not that
clever (not good at detecting lone occurences.)

Jacques Garrigue

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[skaller]

On Fri, 2004-11-26 at 11:44, Jacques Garrigue wrote:

> But by definition 'a unifies with everything, including your void
> type, or you get a noncommutative notion of unification...

Can you give an example? I presume you mean that 
the invariant U(t1,t2) == U(t2,t1) would break?

[I actually don't implement that constraint in Felix,
but it uses extensional polymorphism]

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

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[skaller]

On Fri, 2004-11-26 at 11:44, Jacques Garrigue wrote:

> But by definition 'a unifies with everything, including your void
> type, or you get a noncommutative notion of unification...

BTW: I still don't have a clear understanding of exactly
how problems arise with void with intensional polymorphism.
The typing with a distributive category is clearly sound.
AFAIK this extends to a cartesion closed category.

One might think that extra checks would be needed
which would have to be done at run time with intensional
polymorphism. For example:

let snd (x,y) = y

Here, 'a * 'b is isomorphic to void if 'a or 'b is void.
The definition of snd then doesn't make sense.
The actual problem, however, isn't void, but the incorrect
assumption that a pair can represent a polymorphic tuple:
it isn't the typing that is unsound, but the
choice of canonical representation of product.

The problem would go away if the pointer to the heap
block was NULL for void, but this would require
extra NULL checks at run time.

However, this particular example cannot ever lead
to a problem, since you can't actually create a variable
of void type (there's no value to put in it) so no
possible instantiation of 'snd' can fail.

[There is a clearly related issue with unit: the
types 'a and 1 * 'a are isomorphic, but the definition
of numbered projections prevents the useless unit
being optimised away -- the language guarrantees
not to apply this isormorphism simply because it
would break the run time representation.]

However I don't know if this argument can be extended
in the presence of function types. It would seem that
without a primitive function returning void, there's
no way to encode one that returns void either.

However if you have a primitive f:'a-> void you can
obviously create new functions returning void, for
example:

let g f x = f x
let h x = g f x

However I still don't see how you can ever call such a function
in a way that actually tries to pass a value of type void.
That value has to come from somewhere and there is no way
to make one: a call 

   f x

is manifestly of type void, and so, for example,

	(f x, 99)

is manifestly of type void.

My thinking is that if you can't catch an improper use
of void at compile time, then there can't be one
at run time either (in other words its quite sound).

I would like to see an example where this is not the case.
I'm suspicious, because void is the categorical initial,
and a fundamental part of many of the models for computing
I've seen based on category theory -- and my understanding
is that the CT approach is just an alternative to lambda calculus
(i.e. they're equivalent).

So it looks to me that not providing an algebraic void
is a way to simplify the representation -- not a matter
of unsoundness.

BTW: Ocaml unification must already handle void: it supports
intersection types internally, and int & float is void.
How is it that this also doesn't lead to non-commutative unification?

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

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Jacques Garrigue]

From: skaller <skaller@users.sourceforge.net>
> > But by definition 'a unifies with everything, including your void
> > type, or you get a noncommutative notion of unification...
> 
> Can you give an example? I presume you mean that 
> the invariant U(t1,t2) == U(t2,t1) would break?

Not exactly, I rather meant that unification steps would not commute.
This happens sometimes when you allow unification between specialized
forms, but not with type variables.
However, I do not understand completely what you mean by void type,
and how they would relate to type variables, so it is not clear
whether this is the problem.

For instance, you say that (void * t) should be void, which suggests
that void is really the type with 0 elements (i.e. not unit.)
However, from a logical point of view (i.e. intuitionistic logic), no
function can be allowed to return such a type. It may accept it as
input, but this just means it is unusable.
Note that void in C is definitely not zero. You cannot have variables
of type void, but you can have non-null pointers to void. If void were
really zero, then a void pointer would necessarily be NULL.
It looks more like an existential type, (\exists a.a), which is
actually equivalent to unit, with special rules to deal with the fact
its physical representation is unknown.

Concerning intersection types in ocaml, int&bool is not a type by
itself.  It may only appear as a variant argument. In that case this
just means that this variant case cannot be used. In the past, [ ] was
a valid variant type, and would have been zero, but I removed it as it
does not make sense, and may delay some type errors. Types with only
one variant may not be conjunctive either. So the closest you can get
to zero now is a polymorphic type like [< `A of int&bool | `B of int&bool].
Even with [ ] there was no problem of commutation, because
unification with 'a was allowed, i.e. ([ ] * int) and [ ] were
different types; which was why it was clumsy to have
zero in the language: there is nothing as stupid as moving provably
non-existing data around, as it means that the code will never be used
anyway.

Jacques Garrigue

P.S.
I believe the problem with failwith is solvable, albeit rather
complicated. The idea is that you want to be warned when you apply a
function of type (\forall 'a. 'a) to something, because no such
function may exist, so that this application will never actually take
place.
This could be done attempting to generalize the type of the function,
once we now it is a type variable.
I'll have a try.

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Nicolas Cannasse]

> P.S.
> I believe the problem with failwith is solvable, albeit rather
> complicated. The idea is that you want to be warned when you apply a
> function of type (\forall 'a. 'a) to something, because no such
> function may exist, so that this application will never actually take
> place.
>
> This could be done attempting to generalize the type of the function,
> once we now it is a type variable.
> I'll have a try.

Wouldn't that break Obj.magic ? I can't see a clear solution to this
problem, unless enabling arity specification into polymorphic variables :
'a.0 for example, but this would also break something like :

let f x = if x then failwith "error" else fun() -> x

I guess it's more like a syntax problem. For example having parenthesis for
function calls à la C would disable any ambiguity.

Nicolas

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Richard Jones]

[-- Attachment #1: Type: text/plain, Size: 726 bytes --]

Thanks everyone for the explanation, and the rather convoluted
discussion of the type system, which I don't really understand.

I'd just like to add that this error bit me in a real program, and it
would be nice if OCaml detected this common case and warned about it:

  if cond then (
    ...
    raise Exn
  )
  next_stmt       <-- catastrophic failure, because this statement
                      is silently ignored

Rich.

-- 
Richard Jones.  http://www.annexia.org/  http://www.j-london.com/
>>>   http://www.team-notepad.com/ - collaboration tools for teams   <<<
Merjis Ltd. http://www.merjis.com/ - improving website return on investment
http://youunlimited.co.uk/ - Personal improvement courses

[-- Attachment #2: Digital signature --]
[-- Type: application/pgp-signature, Size: 189 bytes --]

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[skaller]

On Fri, 2004-11-26 at 20:01, Richard Jones wrote:
> Thanks everyone for the explanation, and the rather convoluted
> discussion of the type system, which I don't really understand.
> 
> I'd just like to add that this error bit me in a real program, and it
> would be nice if OCaml detected this common case and warned about it:
> 
>   if cond then (
>     ...
>     raise Exn
>   )
>   next_stmt       <-- catastrophic failure, because this statement
>                       is silently ignored


This happens too, and seems harder to catch with the
intertwined procedural/functional coding style:

if cond then
   x ..
   y ... <-- woops, executed unconditionally
;
next

In Felix I do this:

if cond then something else something_else endif;

where the 'else' and 'endif' are both mandatory. For procedural
conditionals I have distinct syntax:

if cond do foo; bah; done;

Both constructions are LALR1 and unambiguous.
Note the if/then/else/endif is purely functional,
the displayed statement is equivalent to

val f: unit -> void = 
  if cond then something else something_else endif
;
f();

The ocaml notation is more compact but less safe.
Camlp4 could fix this I think, perhaps the 
revised syntax already does?

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

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Ville-Pertti Keinonen]

Richard Jones wrote:

>I'd just like to add that this error bit me in a real program, and it
>would be nice if OCaml detected this common case and warned about it:
>
>  if cond then (
>    ...
>    raise Exn
>  )
>  next_stmt       <-- catastrophic failure, because this statement
>                      is silently ignored
>  
>
It may help to realize that as a (mostly) functional language, OCaml 
doesn't have statements, only expressions (although expressions of the 
type 'unit' could be considered equivalent of statements).

The question to ask isn't "why isn't the missing semicolon detected?"  
Instead, you should think about what the entire expression looks like in 
the absence of the semicolon - it looks like a function application 
(i.e. that you're applying the result of "raise Exn" to whatever follows).

There is no reasonable way to detect such "special cases" (in this case, 
functions that don't return) without a way for the type system to 
express them (you don't e.g. want to special-case "raise" explicitly by 
making it a keyword, as it wouldn't help in the case of "failwith" in 
your original example).

Currently, the type of functions that don't return is expressed as a 
type variable (e.g. 'a) that is not present in the function arguments, 
meaning that it's compatible with any type.  This ensures that when you 
write e.g. "if x then raise Exn else y", the types of "raise Exn" and 
"y" are compatible and can be unified.  It's also compatible with a 
function taking as an argument any expression that may follow it.

Such functions could, instead, return a special type in order to avoid 
cases such as this.  I haven't thought about it in detail, nor have I 
tried to fully understand the suggestions of others, but intuitively, 
I'd think it would have to be unifiable with other types but not capable 
of being used as a value (only valid as a return type of a function) 
until it was unified with (in effect, changed to) some other type on a 
different branch of control flow.  As type inference doesn't have a 
concept of control flow, this could be pretty messy, but it might be 
possible to make it work.

BTW: Hindley-Milner type inference is extremely straightforward, and 
understanding it helps better understand OCaml and other similar languages.

The rules for type inference should pretty much be self-evident if you 
just think about it, but it may help to know the actual basic algorithm, 
described informally as:

We have two namespaces; one binding variables to types (globals to 
actual types, lexically bound variables to type variables), which I'll 
express using '::', and another linking type variables to types (which 
can be other type variables), which I'll express using '=>'.

To infer the type of an expression:

 - Variable x: If there exists x :: t, the type is t (otherwise the 
variable is not visible at this point, which is an error)

 - Literal: The type is immediately known

 - Function abstraction (fun x -> e): Create a new type variable 'a. 
Infer the type of e (call it E) with x :: 'a. The type of the expression 
is 'a -> E

 - Function application (f x): Infer the types of f (F) and x (X).  
Create a new type variable 'a.  Unify (X -> 'a) and F.  The type of the 
expression is 'a

(Most other things can basically be expressed equivalently to functions)

Unification of t1 and t2:

With t1 and t2 normalized, do one of:
 - If t1 and t2 are equal, do nothing
 - If t1 is a type variable, link t1 => t2
 - If t2 is a type variable, link t2 => t1
 - If t1 and t2 are both functions (a1 -> b1, a2 -> b2), unify a1 and 
a2, unify b1 and b2
 - Otherwise fail with a type mismatch

To normalize t:
 - If there exists t => t', repeat with t'
 - Otherwise just return t

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Jacques Garrigue]

From: "Nicolas Cannasse" <warplayer@free.fr>

> > P.S.
> > I believe the problem with failwith is solvable, albeit rather
> > complicated. The idea is that you want to be warned when you apply a
> > function of type (\forall 'a. 'a) to something, because no such
> > function may exist, so that this application will never actually take
> > place.
> >
> > This could be done attempting to generalize the type of the function,
> > once we now it is a type variable.
> > I'll have a try.
> 
> Wouldn't that break Obj.magic ? I can't see a clear solution to this
> problem, unless enabling arity specification into polymorphic variables :

No, because we only look at whether we are applying a function of type
(\forall 'a. 'a), while Obj.magic is of type (\forall 'a 'b. 'a -> 'b)

I've tried, and this seems to work. Actually the code is pretty short.

        Objective Caml version 3.09+dev8 (2004-11-24)

# raise Exit 3;;
             ^
Warning X: this argument is passed to a never returning function.

There is indeed a problem with Obj.magic, but it concerns uses of the
form (Obj.magic f x), which are rather dangerous. Still, this is used
quite a bit in the distribution, and for this reason I disabled the
warning in applications of Obj.magic.
Eventhough, the changes are not so small, so the commit
will have to wait a bit.

     Jacques Garrigue

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Damien Doligez]

On Nov 26, 2004, at 06:25, Jacques Garrigue wrote:

> I believe the problem with failwith is solvable, albeit rather
> complicated. The idea is that you want to be warned when you apply a
> function of type (\forall 'a. 'a) to something, because no such
> function may exist, so that this application will never actually take
> place.

More generally, you want to output a warning whenever the computation
of such a value is not immediately followed by a join in the control
flow graph, because at that point you know you're compiling dead code.

Then you would also get a warning for things like this:

   failwith "foo";
   print_string "hello world"

or

   f (a, b, failwith "foo", c, d)

etc.

Don't ask me to implement it, though.

-- Damien

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Alain Frisch]

Jacques Garrigue wrote:
> # raise Exit 3;;
>              ^
> Warning X: this argument is passed to a never returning function.

In my opinion, the text of the warning is misleading. "Exit" is passed 
to a never returning function, and this is ok. The problem is that 
"raise Exit" is applied to an argument but it cannot evaluate to a function.


-- Alain

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Brian Hurt]

On 26 Nov 2004, skaller wrote:

> On Fri, 2004-11-26 at 08:14, Nicolas Cannasse wrote:
> > > All well and good, but I don't understand why it doesn't warn me about
> > > the missing ';' in the first case.
> > 
> > val failwith : string -> 'a
> > 
> > so failwith "error" prerr_endline "OK";
> > 
> > is a valid call since 'a unify with (string -> unit) -> string -> unit
> 
> .. a problem which could not occur were there a void type
> which couldn't unify with 'a, and prerr_endline had
> type string-> void.
> 
> 

There is one- it's called unit.  And prerr_endline probably already uses
it. The problem isn't with prerr_endline, the "problem" is with failwith.

failwith needs to return 'a, as it doesn't return.  If it returned some 
other type, I couldn't write code like:
    if some_test then
        failwith "some_test"
    else
        some_value

To make the above expression type correctly, failwith has to return the 
same type as some_value- which could be anything.  Therefor, failwith 
needs to return 'a, a value which can unify with (be the same type as) 
anything else.

The next problem comes in how Ocaml decides when and to what to apply 
arguments.  Consider the expression:
    f [1;2;3]
Fairly obvious, right?  We're calling f with an argument of an int list.  
Not necessarily.  Consider:
    List.map f [1;2;3]
Now f, instead of being the function we're passing arguments into, is now 
an argument itself.

So now, this is exactly the problem we're running into- prerr_endling is 
being treated exactly like f above- one minor change, and it's getting 
turned into an argument when it's meant to be a function call.

Does this help?

Brian

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Michal Moskal]

On Fri, 26 Nov 2004 08:08:57 +0100, Nicolas Cannasse <warplayer@free.fr> wrote:
> > P.S.
> > I believe the problem with failwith is solvable, albeit rather
> > complicated. The idea is that you want to be warned when you apply a
> > function of type (\forall 'a. 'a) to something, because no such
> > function may exist, so that this application will never actually take
> > place.
> >
> > This could be done attempting to generalize the type of the function,
> > once we now it is a type variable.
> > I'll have a try.
> 
> Wouldn't that break Obj.magic ? I can't see a clear solution to this
> problem, unless enabling arity specification into polymorphic variables :
> 'a.0 for example, but this would also break something like :
> 
> let f x = if x then failwith "error" else fun() -> x

No, because here you're applying functional type that got unified with
the variable, and not the ununified type variable itself.

> I guess it's more like a syntax problem. For example having parenthesis for
> function calls à la C would disable any ambiguity.

And this is why an empty word as an function application is wrong :-)

-- 
: Michal Moskal ::: http://nemerle.org/~malekith/ :: GCS !tv h e>+++ b++
: ::: Logic is a nice contrast to the Real World. :: UL++++$ C++ E--- a?

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Hendrik Tews]

Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> writes:

   Note that void in C is definitely not zero. You cannot have variables

C++ standard, 3.9.1.9: The void type has an empty set of values. ...

So I would say void is zero. On the other side you have functions
returning void. Therefore I would conclude that the type theory
of C++ is unsound.

Bye,

Hendrik

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[skaller]

On Sat, 2004-11-27 at 09:24, Hendrik Tews wrote:
> Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> writes:
> 
>    Note that void in C is definitely not zero. You cannot have variables
> 
> C++ standard, 3.9.1.9: The void type has an empty set of values. ...
> 
> So I would say void is zero. On the other side you have functions
> returning void. Therefore I would conclude that the type theory
> of C++ is unsound.

I'm not sure I quite understand (not that I disagree with 
the conclusion..)

void in C++ is initial. However, this function:

	int f();

is NOT a function

	void -> int

because in C/C++ you have a list of arguments:

	g(a,b,c)

If you construe the list as a product, so that the function

	int g(int,float,long)

has type

	int * float * long -> int

then you must construe the type of f as

	unit -> int

since the product of an empty list is unit, and NOT void.
The notation for application:

	f ()

even looks like f is being applied to an Ocaml empty tuple :)

In particular in C++ you will note that this does NOT
type correctly:

	void f();
	f( f() );

because the type of f() is void, and the type of the argument
is actually unit.

This means C/C++ has stronger typing in this respect
than Ocaml :)

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

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Jacques Garrigue]

From: Hendrik Tews <tews@tcs.inf.tu-dresden.de>
> Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> writes:
> 
>    Note that void in C is definitely not zero. You cannot have variables
> 
> C++ standard, 3.9.1.9: The void type has an empty set of values. ...
> 
> So I would say void is zero. On the other side you have functions
> returning void. Therefore I would conclude that the type theory
> of C++ is unsound.

Which is almost the same thing as saying that the definition
contradicts itself...
My point was just that, looking at the way void is used in C, it
clearly does not have the usual proporties of zero, and among them the
fact no function should be able to return zero, or that all pointers
to void should be NULL.

For this reason it seems to me at first that the actual semantics of
void in C is that of (\exists a. a) aka unit (i.e. a value we know
nothing about), not that of (\forall a.a) aka zero (the impossibility).
You can safely cast any pointer to a void pointer, but not the
opposite. Additionaly, for representation reasons, you cannot copy or
allocate values of type void, so that they are non-existent in
practice, but this looks more like a consequence than a definition.
Another meaning of void seems to be the empty product, which again is
unit, with the extract constraint that you cannot store such a value
in C.

This is just my personal take on the question. I just don't think that
there is any serious model theory behind C's void, just a bunch of
practical constraints.

Jacques Garrigue

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Jacques Garrigue]

From: Damien Doligez <damien.doligez@inria.fr>
> > I believe the problem with failwith is solvable, albeit rather
> > complicated. The idea is that you want to be warned when you apply a
> > function of type (\forall 'a. 'a) to something, because no such
> > function may exist, so that this application will never actually take
> > place.
> 
> More generally, you want to output a warning whenever the computation
> of such a value is not immediately followed by a join in the control
> flow graph, because at that point you know you're compiling dead code.
> 
> Then you would also get a warning for things like this:
> 
>    failwith "foo";
>    print_string "hello world"
> 
> or
> 
>    f (a, b, failwith "foo", c, d)
> 
> etc.
> 
> Don't ask me to implement it, though.

This is not specially hard to implement case by case.
The problem is rather that the technique I use, based on type
inference, is not foolproof (you can avoid the warning with a type
annotation for instance) and is wrong in presence of Obj.magic.
So the question is in which cases having a warning is worth the
inconvenience and the extra code in the compiler.

I would say your first example is reasonable (this may be a consequence
of a dangling then), but much less the second one (where is the
ambiguity?)

Jacques Garrigue

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Marcin 'Qrczak' Kowalczyk]

Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> writes:

> My point was just that, looking at the way void is used in C, it
> clearly does not have the usual proporties of zero, and among them
> the fact no function should be able to return zero, or that all
> pointers to void should be NULL.

Rules of void in C are special. In particular it makes no sense to
draw conclusions about "the number of values of type void" from the
semantics of pointers to void.

There are no values of type void, no variables of type void,
and no function arguments of type void. You can't write
   void deref(void *p) {return *p;}
and this is valid only in C++, not in C:
   void f();
   void g() {return f();}

There are no values of type void. A C function either produces a value
or not. If it does not, it's written by putting 'void' instead of its
return type.

A pointer to void holds an address of some value, not an address of
a value of type void.

Trying to treat 'void' analogously to other types will show
inconsistencies and lead to contradictions.

-- 
   __("<         Marcin Kowalczyk
   \__/       qrczak@knm.org.pl
    ^^     http://qrnik.knm.org.pl/~qrczak/

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; afterfailwith statement?

[Frederic van der Plancke]

Jacques Garrigue wrote:
> 
> From: Damien Doligez <damien.doligez@inria.fr>
> > > I believe the problem with failwith is solvable, albeit rather
> > > complicated. The idea is that you want to be warned when you apply a
> > > function of type (\forall 'a. 'a) to something, because no such
> > > function may exist, so that this application will never actually take
> > > place.
> >
> > More generally, you want to output a warning whenever the computation
> > of such a value is not immediately followed by a join in the control
> > flow graph, because at that point you know you're compiling dead code.
> >
> > Then you would also get a warning for things like this:
> >
> >    failwith "foo";
> >    print_string "hello world"
> >
> > or
> >
> >    f (a, b, failwith "foo", c, d)
> >
> > etc.
> >
> > Don't ask me to implement it, though.
> 
> This is not specially hard to implement case by case.
> The problem is rather that the technique I use, based on type
> inference, is not foolproof (you can avoid the warning with a type
> annotation for instance) and is wrong in presence of Obj.magic.
> So the question is in which cases having a warning is worth the
> inconvenience and the extra code in the compiler.

Why not create a special type "noreturn" or "empty" with special typing properties ? in most respect it would act like 'a; but the compiler would know the difference.
* raise : exn -> noreturn   (and hence: failwith : string -> noreturn)
  (similarly: [assert false : noreturn])
  but Obj.magic keeps its type : 'a -> 'b
* noreturn can be unified to any type t (including 'a), this yields type t
   (so [function [] -> assert false | x::_ -> x] has type ['a list -> 'a])
* a warning would be issued
   - for an "apply" node when any input term has type noreturn
   - for a ";" node when the first term has type noreturn
   - etc
* problem: one could write [Obj.magic 123 : noreturn]
  (or similarly in other cases like marshalling where a lone 'a *can*
   correspond to a value) and defeat the system.
  possible solution: forbid or restrict explicit casts (er, type annotations,
  sorry ;-) to noreturn. (i.e. since 'a annotates "a value of any type" and
  noreturn annotates "no value", there's no reason to allow "casting" 'a as
  noreturn.)

Frédéric vdP

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; afterfailwith statement?

[Frederic van der Plancke]

Jacques Garrigue wrote:
> 
> From: Damien Doligez <damien.doligez@inria.fr>
> > > I believe the problem with failwith is solvable, albeit rather
> > > complicated. The idea is that you want to be warned when you apply a
> > > function of type (\forall 'a. 'a) to something, because no such
> > > function may exist, so that this application will never actually take
> > > place.
> >
> > More generally, you want to output a warning whenever the computation
> > of such a value is not immediately followed by a join in the control
> > flow graph, because at that point you know you're compiling dead code.
> >
> > Then you would also get a warning for things like this:
> >
> >    failwith "foo";
> >    print_string "hello world"
> >
> > or
> >
> >    f (a, b, failwith "foo", c, d)
> >
> > etc.
> >
> > Don't ask me to implement it, though.
> 
> This is not specially hard to implement case by case.
> The problem is rather that the technique I use, based on type
> inference, is not foolproof (you can avoid the warning with a type
> annotation for instance) and is wrong in presence of Obj.magic.
> So the question is in which cases having a warning is worth the
> inconvenience and the extra code in the compiler.

Why not create a special type "noreturn" or "empty" with special typing properties ? in most
respect it would act like 'a; but the compiler would know the difference.
* raise : exn -> noreturn   (and hence: failwith : string -> noreturn)
  (similarly: [assert false : noreturn])
  but Obj.magic keeps its type : 'a -> 'b
* noreturn can be unified to any type t (including 'a), this yields type t
   (so [function [] -> assert false | x::_ -> x] has type ['a list -> 'a])
* a warning would be issued
   - for an "apply" node when any input term has type noreturn
   - for a ";" node when the first term has type noreturn
   - etc
* problem: one could write [Obj.magic 123 : noreturn]
  (or similarly in other cases like marshalling where a lone 'a *can*
   correspond to a value) and defeat the system.
  possible solution: forbid or restrict explicit casts (er, type annotations,
  sorry ;-) to noreturn. (i.e. since 'a annotates "a value of any type" and
  noreturn annotates "no value", there's no reason to allow "casting" 'a as
  noreturn.)

Frédéric vdP

Re: [Caml-list] Why doesn't ocamlopt detect a missing ; afterfailwith statement?

[Jacques Garrigue]

From: Frederic van der Plancke <fvdp@decis.be>

> > The problem is rather that the technique I use, based on type
> > inference, is not foolproof (you can avoid the warning with a type
> > annotation for instance) and is wrong in presence of Obj.magic.
> > So the question is in which cases having a warning is worth the
> > inconvenience and the extra code in the compiler.
> 
> Why not create a special type "noreturn" or "empty" with special typing properties ? in most respect it would act like 'a; but the compiler would know the difference.
> * raise : exn -> noreturn   (and hence: failwith : string -> noreturn)
>   (similarly: [assert false : noreturn])
>   but Obj.magic keeps its type : 'a -> 'b
> * noreturn can be unified to any type t (including 'a), this yields type t
>    (so [function [] -> assert false | x::_ -> x] has type ['a list -> 'a])

This just looks like a much higher cost in terms of changes to the
compiler. And the danger of introducing bugs in unification, just for a
warning in some strange cases. (You should realize that what you are
proposing is not a new type, but a new kind of type variables.)
The generalization technique works well. It is not surprising that it
doesn't mix that well with Obj.magic, but then Obj.magic is clearly
unsound, so you know what to expect.

        Objective Caml version 3.09+dev9 (2004-11-29)

# fun () -> raise Exit print_int 3;;
                       ^^^^^^^^^
Warning X: this argument will not be received by the function.
# fun () -> raise Exit; "Hello";;
            ^^^^^^^^^^
Warning X: this statement never returns.
# fun f -> ((Obj.magic f) 3);;
                          ^
Warning X: this argument will not be received by the function.
# fun f -> ((Obj.magic f : _ -> _) 3);;
- : 'a -> 'b = <fun>

Jacques Garrigue