Towards Tree Automata-based Success Types

TL;DR

This paper introduces an advanced static analysis method using tree automata and model checking to improve success typings in dynamic languages, addressing limitations of previous approaches like Lindahl and Sagonas' success typings.

Contribution

It extends pattern-matching recursion schemes with context-aware ranked tree automata to enhance success typing detection in a constructor-based language.

Findings

Improved detection of nested tuple errors

Enhanced success typings for recursive patterns

Addresses limitations of previous success typing approaches

Abstract

Error detection facilities for dynamic languages are often based on unit testing. Thus, the advantage of rapid prototyping and flexibility must be weighed against cumbersome and time consuming test suite development. Lindahl and Sagonas' success typings provide a means of static must-fail detection in Erlang. Due to the constraint-based nature of the approach, some errors involving nested tuples and recursion cannot be detected. We propose an approach that uses an extension of model checking for pattern-matching recursion schemes with context-aware ranked tree automata to provide improved success typings for a constructor-based first-order prototype language.