Nachiappan Valliappan
ABSTRACT
Developing a static type system suitable for Erlang has been of ongoing interest for almost two decades now. The challenge with retrofitting a static type system onto a dynamically typed language, such as Erlang, is the loss of flexibility in programming offered by the language. In light of this, many attempts to type Erlang trade sound type checking for the ability to retain flexibility. Hence, simple type errors which would be caught by the type checker of a statically typed language are easily missed in these developments. This has us wishing for a way to avoid such errors in Erlang programs.
In this paper, we develop a static type system for Erlang which strives to remain sound without being too restrictive. Our type system is based on Hindley-Milner type inference, however it---unlike contemporary implementations of Hindley-Milner---is flexible enough to allow overloading of data constructors, branches of different types etc. Further, to allow Erlang's dynamic type behaviour, we employ a program specialization technique called partial evaluation. Partial evaluation simplifies programs prior to type checking, and hence enables the type system to type such behaviour under certain restricted circumstances.
- Ana Bove, Peter Dybjer, and Ulf Norell. 2009. A brief overview of Agda–a functional language with dependent types. In International Conference on Theorem Proving in Higher Order Logics. Springer, 73–78. Google Scholar
Digital Library
- Luis Damas and Robin Milner. 1982. Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 207–212. Google ScholarDigital Library
- Gilles Dowek. 1993. The undecidability of typability in the lambdapi-calculus. In International Conference on Typed Lambda Calculi and Applications. Springer, 139–145. Google ScholarDigital Library
- Mark P Jones. 1999. Typing haskell in haskell. In Haskell workshop, Vol. 7.Google Scholar
- Neil D Jones, Carsten K Gomard, and Peter Sestoft. 1993. Partial evaluation and automatic program generation. Peter Sestoft. Google ScholarDigital Library
- Tobias Lindahl and Konstantinos Sagonas. 2005. Typer: a type annotator of erlang code. In Proceedings of the 2005 ACM SIGPLAN workshop on Erlang. ACM, 17–25. Google ScholarDigital Library
- Tobias Lindahl and Konstantinos Sagonas. 2006. Practical type inference based on success typings. In Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programming. ACM, 167–178. Google ScholarDigital Library
- Simon Marlow and Philip Wadler. 1997. A practical subtyping system for Erlang. ACM SIGPLAN Notices 32, 8 (1997), 136–149. Google ScholarDigital Library
- Robin Milner. 1978. A theory of type polymorphism in programming. Journal of computer and system sciences 17, 3 (1978), 348–375.Google ScholarCross Ref
- Didier Rémy. 2002. Using, understanding, and unraveling the OCaml language from practice to theory and vice versa. In Applied Semantics. Springer, 413–536.Google Scholar
- Mary Sheeran and Gunnar Stålmarck. 1998. A tutorial on Stålmarck’s proof procedure for propositional logic. In International Conference on Formal Methods in Computer-Aided Design. Springer, 82–99. Google ScholarDigital Library
Index Terms
- Typing the wild in Erlang
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 ...
Set-theoretic Types for Erlang
IFL '22: Proceedings of the 34th Symposium on Implementation and Application of Functional LanguagesErlang is a functional programming language with dynamic typing. The language offers great flexibility for destructing values through pattern matching and dynamic type tests. Erlang also comes with a type language supporting parametric polymorphism, ...
Gradual typing with unification-based inference
DLS '08: Proceedings of the 2008 symposium on Dynamic languagesStatic and dynamic type systems have well-known strengths and weaknesses. Gradual typing provides the benefits of both in a single language by giving the programmer control over which portions of the program are statically checked based on the presence ...
Comments