I am wondering whether it is a bad style to use "exception". For example, in Ocaml, the exception does not appear as the .mli file. So it appears to me that "exception" is something that cannot be tracked by a type system.
So my question in general is, is using exception a bad style because it hides information against the type system?
Concretely, I am trying to implement a type checker for an imperative language, say, Pascal. The essential judgment should have been of this signature,
well-typed_1: environment -> statement -> unit
But this seems to be insufficient because the environment would be modified due to a local variable declaration, thus a more reasonable interface for typechecker would be
well-typed_2: environment -> statement -> environment
An alternative would be use the former one, well-typed_1, dealing with local variables declaration through an exception Var_declaration (e : environment) which returns the updated environment to the type checker for its other recursion.
So, my question for this concrete example is , should I use the well-typed_1 + exception for variable declaration, or well-typed_2?
The disadvantage of well-typed_2 seems to be that, for most statement there are no side effect with regard to environment of types, thus that signature of well-typed_2 seems to be a bit redundant. The disadvantage of well_typed_2 + exception seems to reveal a general issue: the the signature of well-typed_1 in does not tell the whole story. (it does not tell the potential exception)