Implicit Typing

Abstract

The extension calculus provides a bridge between the typed and untyped pattern calculi, and underpins the bondi programming language. Its evaluation is type-free, but preserves typing. In turn, this requires that term matching implies type matching, so that patterns must have their most general, or principal types. For static patterns this is easily enforced, but general evaluation may increase or decrease type information, so free variables and functions in patterns are required to be linear, in the sense that they use their arguments exactly once. Central to the type discipline are the rules for typing extensions, which make delicate use of type equations and inequalities. Method specialisation is represented by extensions in which the pattern is an object pattern.