Computer Science > Programming Languages
arXiv:2302.12783 (cs)
[Submitted on 24 Feb 2023 (v1), last revised 13 Jun 2023 (this version, v2)]
Title:Set-theoretic Types for Erlang
View a PDF of the paper titled Set-theoretic Types for Erlang, by Albert Schimpf and 2 other authors
View PDFAbstract:Erlang 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, equi-recursive types, as well as union and a limited form of intersection types. However, type signatures only serve as documentation, there is no check that a function body conforms to its signature. Set-theoretic types and semantic subtyping fit Erlang's feature set very well. They allow expressing nearly all constructs of its type language and provide means for statically checking type signatures. This article brings set-theoretic types to Erlang and demonstrates how existing Erlang code can be statically typechecked without or with only minor modifications to the code. Further, the article formalizes the main ingredients of the type system in a small core calculus, reports on an implementation of the system, and compares it with other static typecheckers for Erlang.
| Comments: | 14 pages, 9 figures, IFL 2022; latexmk -pdf to build |
| Subjects: | Programming Languages (cs.PL) |
| Cite as: | arXiv:2302.12783 [cs.PL] |
| (orarXiv:2302.12783v2 [cs.PL] for this version) | |
| https://doi.org/10.48550/arXiv.2302.12783 arXiv-issued DOI via DataCite |
Submission history
From: Albert Schimpf [view email][v1] Fri, 24 Feb 2023 17:53:05 UTC (156 KB)
[v2] Tue, 13 Jun 2023 09:37:50 UTC (359 KB)
Full-text links:
Access Paper:
- View PDF
- TeX Source
- Other Formats
View a PDF of the paper titled Set-theoretic Types for Erlang, by Albert Schimpf and 2 other authors
References & Citations
Bookmark
Bibliographic and Citation Tools
Bibliographic Explorer(What is the Explorer?)
Connected Papers(What is Connected Papers?)
Litmaps(What is Litmaps?)
scite Smart Citations(What are Smart Citations?)
Code, Data and Media Associated with this Article
alphaXiv(What is alphaXiv?)
CatalyzeX Code Finder for Papers(What is CatalyzeX?)
DagsHub(What is DagsHub?)
Gotit.pub(What is GotitPub?)
Hugging Face(What is Huggingface?)
Papers with Code(What is Papers with Code?)
ScienceCast(What is ScienceCast?)
Demos
Recommenders and Search Tools
Influence Flower(What are Influence Flowers?)
CORE Recommender(What is CORE?)
arXivLabs: experimental projects with community collaborators
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community?Learn more about arXivLabs.