Details

Autor(en) / Beteiligte

• Pearce, David J.

Titel

On declarative rewriting for sound and complete union, intersection and negation types

Ist Teil von

• Journal of computer languages (Online), 2019-02, Vol.50, p.84-101

Ort / Verlag

Elsevier Ltd

Erscheinungsjahr

2019

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• •We detail an implementation using declarative rewrite rules of a subtype operator involving union, intersection and negation types.•We report experiment results over a range of range of benchmarks comparing this with an ad-hoc existing implementation.•We detail the implementation of our system in the Rascal meta-programming framework.•We discuss an approach to supporting recursive types via coinductive rewriting. Implementing the type system of a programming language is a critical task that is often done in an ad-hoc fashion. Whilst this makes it hard to ensure the system is sound, it also makes it difficult to extend as the language evolves. We are interested in describing type systems using rewrite rules from which an implementation can be automatically generated. Whilst not all type systems are easily expressed in this manner, those involving unions, intersections and negations are well-suited for this. For example, subtyping in such systems is naturally expressed as a maximal reduction over the intersection of types involved. In this paper, we consider a relatively complex type system involving unions, intersections and negations developed previously in the context of type checking. This system was not developed with rewriting in mind, though clear parallels are immediately apparent from the original presentation. For example, the system presented required types be first converted into a variation on Disjunctive Normal Form. However, some aspects of the original system are more challenging to express with rewrite rules. We identify that the original system can, for the most part, be reworked to enable a natural expression using rewrite rules. We present an implementation of our rewrite rules in the Whiley Rewrite Language (WyRL), and report performance results compared with a hand-coded solution. We also present an implementation of our system in the Rascal rewriting system, and find different trade offs.