Towards Tree Automata-based Success Types

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.