User:Hakerh400/Types of exceptions

In this article we discuss various types of exceptions and how they can be used in some practical situations.

Hard exception

Hard exception is used to terminate the program immediately. It cannot be caught in any way. It is used when a fatal error occurs, such as a failed assertion or an invalid value of some invariant. In Haskell it is called error. This type of exception can be used in the following situations:

• A part of the program that is not implemented yet. The exception acts as a placeholder.
• Unreachable part of the program.
• To satisfy the syntax/semantic rules of the compiler/interpreter. In some situations, certain patterns are forced by the semantics of the language. For instance, in Haskell in order to use the + operator, we need to implement the Num instance, even though other operators, such as - or * may not always have a good implementation, so they can be left as error expressions.
• To terminate the program early in the process of debugging/logging.

Choice exception

We also call it a "soft exception". When implementing a parser, we can use the choice operator to pick one of the multiple choices. Raising a choice exception terminates the current branch and switches to the next one. Essentially, it allows backtracking. In haskell, it is most similar to MonadFail. Use cases:

• Parsing. It allows picking one of multiple choices.
• Regex matching. It allows multiple choices and backtracking.
• Performing a collection of tests. If any test raises a soft exception, the testing fails and the rest of tests will not be performed.
• Filtering a container, such as a list or a set. For each element we perform tests, if any raises a soft exception, the element is discarded.

Semantic exception

It lies between hard exception and choice exception. When it occurs, it terminates the entire computation, but not the entire program. It can be caught using certain functions. In Haskell, it can be simulated using a newtype around ExceptT with a custom MonadFail instance (because the default instance delegates the fail to the inner monad). Use cases:

• Parsing. If we want to parse a term or a type, we use choice branching. But once we know that we are parsing a type, we should no longer backtrack, because there is no point of doing so. If we then parse an identifier that is not a type, we raise a semantic exception. It terminates the entire parsing.

Continuation exception

Similar to the semantic exception, but allows reconstructing the control flow alongside the state. In Haskell it can be achieved using ContT transformer (again, a custom MonadFail instance is necessary). Use Cases:

• Traversing a Trie data structure, while modifying an underlying state.
• Automatic simplification of an object. Suppose we have a number of simplification rules that we can apply to an object by matching sub-patterns in the object recursively. The rules are not perfect, so they may fail in some situations, and we just do not care, but we want to try to apply every rule if possible. We apply a rule and then we test if the rest of the simplification works. If an error occurs in any of the subsequent non-simplifying steps, we backtrack to the last simplification and we undo it. A concrete example: reconstructing the tactic-monadical proof from a raw kernel proof in a theorem prover.