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