A type system for embedded rewriting languages with associative pattern matching: from theory to practice

Programmers are often interested in a way to write error-free programs, i.e. to avoid undesired behaviors. In this context, a type system was conceived as the formal method for speci cation and proof of programs written in the Tom rewriting language. The Tom programming language is an extension of Java that adds pattern matching, more particularly associative pattern matching, and reduction strategies. Accordingly, we aim to make the static typing of the Tom constructs, in particular matching constructs, compatible with the features of Java. This paper presents a type system with nominal subtyping for Tom, that is compatible with the Java type system, and that performs both type inference. We adopted the idea that type inference is a form of type checking and included equality and subtyping constraints inside typing judgments. We propose a constraint-based type inference system to infer types of variables occurring in algebraic terms. Then, we de fine rules to solve equality constraints by uni cation. For the resolution of subtyping constraints, we introduce rules for a combination of constraint propagation, generation of solution and garbage collecting of remaining constraints.