[Re: [Re: [clean-list] Clean in the Real World]]

Olivier Lefevre olefevre@usa.net
Wed, 17 Dec 2003 23:15:08 +0100


> There is no law however that says that the output type of a function 
> should be interpreted as the union of its "actual" type and some 
> exception type. I like the idea that the type that I write down for 
> a function result is actually the type it has.

Something that is not clear in this discussion between you and Fergus 
is what you mean by "result". Do you mean the result according to
the "official" semantics of a language, in which case I agree with you 
that a function returning an int is still that even when it can throw
an exception, at least in the languages I know [*], or the result in 
some mental model of the program's execution in the head of the compiler 
writer, which might actually be expressed in a formal intermediate 
compilation language in which the function in question _would_ have 
such a discriminated union as its return type?

-- O.L.

[*] But note that, e.g., in Java, thrown exceptions can be part of a
method signature, so in a sense they are part of its "return type".
Is there any good work on how exceptions can be meshed with a type 
system? This discussion makes me realize that this is not obvious 
at all...