Doesn’t a negative approach to exception tracking require a much stronger “closed world” assumption than the original one? I know this bit of code can’t throw exception Y - but why is that a useful fact, given that any number of possible exceptions could exist, including some that were semantically equivalent to Y?
Better to treat exceptions as ordinary types and apply the same rules about those escaping their scopes. What do you do with code that looks like (apologies for syntax):
let
type X
val x: X
in
x
end
Can’t we handle the raise X example exactly the same way?
I don’t know the answer to your question, my guess is that the SML world, which is pretty closed, would be sufficient, as one will be able to enumerate all exceptions that can be thrown at compile time. In Ocaml, there is a dynlink module which means things can be loaded at runtime which would be a chink in this armour.
Doesn’t a negative approach to exception tracking require a much stronger “closed world” assumption than the original one? I know this bit of code can’t throw
exception Y- but why is that a useful fact, given that any number of possible exceptions could exist, including some that were semantically equivalent toY?Better to treat exceptions as ordinary types and apply the same rules about those escaping their scopes. What do you do with code that looks like (apologies for syntax):
Can’t we handle the
raise Xexample exactly the same way?I don’t know the answer to your question, my guess is that the SML world, which is pretty closed, would be sufficient, as one will be able to enumerate all exceptions that can be thrown at compile time. In Ocaml, there is a dynlink module which means things can be loaded at runtime which would be a chink in this armour.