Miguel Jimenez
ABSTRACT
We propose a small extension of the Erlang language that allows programmers to specify contracts with type information at the level of individual functions. Such contracts are optional and they document the intended uses of functions. Contracts allow automatic documentation tools such as Edoc to generate better documentation and defect detection tools such as Dialyzer to detect more type clashes. Since the Erlang/OTP system already contains components which perform automatic type inference of success typings, we also describe how contracts interact with success typings and can often provide some key information to the inference process.
- R. Cartwright and M. Fagan. Soft typing. In Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation, pages 278--292. ACM Press, 1991. Google Scholar
Digital Library
- R. B. Findler, J. Clements, C. Flanagan, M. Flatt, S. Krishnamurthi, P. Steckler, and M. Felleisen. DrScheme: A programming environment for Scheme. Journal of Functional Programming, 12(2):159--182, Mar. 2002. Google ScholarDigital Library
- M. V. Hermenegildo, G. Puebla, F. Bueno, and P. López-García. Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor). Sci. Comput. Programming, 58(1-2):115--140, 2005. Google ScholarDigital Library
- 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.Google Scholar
- T. Lindahl and K. Sagonas. Typer: a type annotator of erlang code. In Proceedings of the 2005 ACM SIGPLAN Erlang Workshop, pages 17--25, New York, NY, USA, 2005. ACM Press. Google ScholarDigital Library
- T. Lindahl and K. Sagonas. Practical type inference based on success typings. In Proceedings of the 8th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, pages 167--178, New York, NY, USA, 2006. ACM Press. Google ScholarDigital Library
- S. Marlow and P. Wadler. A practical subtyping system for Erlang. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming, pages 136--149. ACM Press, June 1997. Google ScholarDigital Library
- K. Sagonas. Experience from developing the Dialyzer: A static analysis tool detecting defects in Erlang applications. In ACM SIGPLAN Workshop on the Evaluation of Defect Detection Tools (Bugs'05), June 2005.Google Scholar
- M. Serrano. Bigloo: A practical Scheme compiler, May 2007. User manual for version 3.0a.Google Scholar
- Z. Somogyi, F. Henderson, and T. Conway. The execution algorithm of Mercury, an efficient purely declarative logic programming language. Journal of Logic Programming, 26(1-3):17--64, Oct./Dec. 1996.Google ScholarCross Ref
- G. L. Steele. Common Lisp: The Language. Digital Press, 2nd edition, 1990. Google ScholarDigital Library
Index Terms
- A language for specifying type contracts in erlang and its interaction with success typings
Recommendations
Bidirectional typing for Erlang
Erlang 2021: Proceedings of the 20th ACM SIGPLAN International Workshop on ErlangErlang is a strict, dynamically typed functional programming language popular for its use in distributed and fault-tolerant applications. The absence of static type checking allows ill-typed programs to cause type errors at run time. The benefits of ...
Practical type inference based on success typings
PPDP '06: Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programmingIn languages where the compiler performs no static type checks, many programs never go wrong, but the intended use of functions and component interfaces is often undocumented or appears only in the form of comments which cannot always be trusted. This ...
TypEr: a type annotator of Erlang code
ERLANG '05: Proceedings of the 2005 ACM SIGPLAN workshop on ErlangWe 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 ...
Comments