Explanation Of Success Typing Violations In Erlang Programs

Abstract

Although type systems do detect type errors in programs, they often produce uninformative error messages, that hardly give information about the underlying source of the error. For Erlang, which is dynamically typed, there is Dialyzer, a static analysis tool that identifies software discrepancies such as definite type errors, code which has become dead or unreachable due to some programming error, unnecessary tests or other reasons in single Erlang modules or entire (sets of) applications. Dialyzer uses a type inference algorithm to determine the success typings of the program functions and afterwards a defect detection mechanism to report any violation of the inferred types. Discrepancies detected by Dialyzer are presented to the user in the form of 1-2 line warnings. As in many functional languages these warnings are not very clear and the users often complain for incomprehensible error messages. The present thesis deals with the problem of providing the user with explanation to the roots of these warnings, whenever the user demands it. The explanation that we provide actually determines why the variables, expressions or even functions that appear in the erroneous part of code have a particular type. Additionally, we provide a separate explanation of the inferred success typing of functions.