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

[Ville-Pertti Keinonen <will@exomi.com>]

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