TypEr: a type annotator of Erlang code

ABSTRACT

We describe and document the techniques used in TOOL, a fully automatic type annotator for Erlang programs based on constraint-based type inference of success typings (a notion closely related to principal typings). The inferred typings are fine-grained and the type system currently includes subtyping and subtype polymorphism but not parametric polymorphism. In particular, we describe and illustrate through examples a type inference algorithm tailored to Erlang's characteristics which is modular, reasonably fast, and appears to scale well in practice.

REFERENCES

• 1: Alexander Aiken , Edward L. Wimmers, Type inclusion constraints and type inference, Proceedings of the conference on Functional programming languages and computer architecture, p.31-41, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165188]
• 2: Joe Armstrong , Robert Virding , Claes Wikström , Mike Williams, Concurrent programming in ERLANG (2nd ed.), Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1996
• 3: Robert Bruce Findler , John Clements , Cormac Flanagan , Matthew Flatt , Shriram Krishnamurthi , Paul Steckler , Matthias Felleisen, DrScheme: a programming environment for Scheme, Journal of Functional Programming, v.12 n.2, p.159-182, March 2002 [doi>10.1017/S0956796801004208]
• 4: Trevor Jim, What are principal typings and what are they good for?, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-53, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237728]
• 5: T. Lindahl and K. Sagonas. Detecting software defects in telecom applications through lightweight static analysis: A war story. In C. Wei-Ngan, editor, Programming Languages and Systems: Proceedings of the Second Asian Symposium (APLAS'04), volume 3302 of LNCS, pages 91--106. Springer, Nov. 2004.
• 6: Simon Marlow , Philip Wadler, A practical subtyping system for Erlang, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.136-149, June 09-11, 1997, Amsterdam, The Netherlands
• 7: Sven-Olof Nyström, A soft-typing system for Erlang, Proceedings of the 2003 ACM SIGPLAN workshop on Erlang, p.56-71, August 29-29, 2003, Uppsala, Sweden [doi>10.1145/940880.940888]
• 8: J. B. Wells, The Essence of Principal Typings, Proceedings of the 29th International Colloquium on Automata, Languages and Programming, p.913-925, July 08-13, 2002

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.7 Distribution, Maintenance, and Enhancement
          Subjects: Documentation

General Terms:
Languages, Theory

Keywords:
Erlang, constraint-based type inference, principal typings, subtyping, success typings