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

[Marco Kesseler]

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

I must admit that I also have to get used to the right terminology in 
this area.

In a pure functional language, I mean by "result" the value that a 
function application returns. When exceptions are involved, it may be 
better to more carefully talk about the "value" of an expression.

In either case, I am not referring to some internal representation.

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