A Type System For Call-By-Name Exceptions

TL;DR

This paper extends System F with call-by-name exceptions, introducing union and corruption types to analyze exception behavior, and proves properties like confluence and normalization.

Contribution

It develops a novel type system for call-by-name exceptions with formal semantics and proves key properties, including normalization and correct computation.

Findings

Well-typed programs are weakly normalizing.

Programs with natural number types compute natural numbers without exceptions.

The system maintains confluence despite exceptions.

Abstract

We present an extension of System F with call-by-name exceptions. The type system is enriched with two syntactic constructs: a union type for programs whose execution may raise an exception at top level, and a corruption type for programs that may raise an exception in any evaluation context (not necessarily at top level). We present the syntax and reduction rules of the system, as well as its typing and subtyping rules. We then study its properties, such as confluence. Finally, we construct a realizability model using orthogonality techniques, from which we deduce that well-typed programs are weakly normalizing and that the ones who have the type of natural numbers really compute a natural number, without raising exceptions.