Search Results

Documents authored by Schrijvers, Tom

Document
DOI: 10.4230/LIPIcs.ITP.2023.8
No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System

Authors: Roger Bosman, Georgios Karachalias, and Tom Schrijvers

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
The Hindley-Damas-Milner (HDM) system provides polymorphism, a key feature of functional programming languages such as Haskell and OCaml. It does so through a type inference algorithm, whose soundness and completeness have been well-studied and proven both manually (on paper) and mechanically (in a proof assistant). Earlier research has focused on the problem of inferring the type of a top-level expression. Yet, in practice, we also may wish to infer the type of subexpressions, either for the sake of elaboration into an explicitly-typed target language, or for reporting those types back to the programmer. One key difference between these two problems is the treatment of underconstrained types: in the former, unification variables that do not affect the overall type need not be instantiated. However, in the latter, instantiating all unification variables is essential, because unification variables are internal to the algorithm and should not leak into the output. We present an algorithm for the HDM system that explicitly tracks the scope of all unification variables. In addition to solving the subexpression type reconstruction problem described above, it can be used as a basis for elaboration algorithms, including those that implement elaboration-based features such as type classes. The algorithm implements input and output contexts, as well as the novel concept of full contexts, which significantly simplifies the state-passing of traditional algorithms. The algorithm has been formalised and proven sound and complete using the Coq proof assistant.
Cite as

Roger Bosman, Georgios Karachalias, and Tom Schrijvers. No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bosman_et_al:LIPIcs.ITP.2023.8,
  author =	{Bosman, Roger and Karachalias, Georgios and Schrijvers, Tom},
  title =	{{No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.8},
  URN =		{urn:nbn:de:0030-drops-183836},
  doi =		{10.4230/LIPIcs.ITP.2023.8},
  annote =	{Keywords: type inference, mechanization, let-polymorphism}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.27
Row and Bounded Polymorphism via Disjoint Polymorphism

Authors: Ningning Xie, Bruno C. d. S. Oliveira, Xuan Bi, and Tom Schrijvers

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Polymorphism and subtyping are important features in mainstream OO languages. The most common way to integrate the two is via 𝖥_{< :} style bounded quantification. A closely related mechanism is row polymorphism, which provides an alternative to subtyping, while still enabling many of the same applications. Yet another approach is to have type systems with intersection types and polymorphism. A recent addition to this design space are calculi with disjoint intersection types and disjoint polymorphism. With all these alternatives it is natural to wonder how they are related. This paper provides an answer to this question. We show that disjoint polymorphism can recover forms of both row polymorphism and bounded polymorphism, while retaining key desirable properties, such as type-safety and decidability. Furthermore, we identify the extra power of disjoint polymorphism which enables additional features that cannot be easily encoded in calculi with row polymorphism or bounded quantification alone. Ultimately we expect that our work is useful to inform language designers about the expressive power of those common features, and to simplify implementations and metatheory of feature-rich languages with polymorphism and subtyping.
Cite as

Ningning Xie, Bruno C. d. S. Oliveira, Xuan Bi, and Tom Schrijvers. Row and Bounded Polymorphism via Disjoint Polymorphism. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 27:1-27:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{xie_et_al:LIPIcs.ECOOP.2020.27,
  author =	{Xie, Ningning and Oliveira, Bruno C. d. S. and Bi, Xuan and Schrijvers, Tom},
  title =	{{Row and Bounded Polymorphism via Disjoint Polymorphism}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{27:1--27:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.27},
  URN =		{urn:nbn:de:0030-drops-131846},
  doi =		{10.4230/LIPIcs.ECOOP.2020.27},
  annote =	{Keywords: Intersection types, bounded polymorphism, row polymorphism}
}
Document
DOI: 10.4230/DagRep.8.4.104
Algebraic Effect Handlers go Mainstream (Dagstuhl Seminar 18172)

Authors: Sivaramakrishnan Krishnamoorthy Chandrasekaran, Daan Leijen, Matija Pretnar, and Tom Schrijvers

Published in: Dagstuhl Reports, Volume 8, Issue 4 (2018)

Abstract
Languages like C\#, C++, or JavaScript support complex control flow statements like exception handling, iterators (yield), and even asynchrony (async/await) through special extensions. For exceptions, the runtime needs to be extended with exception handling stack frames. For iterators and asynchrony, the situation is more involved, as the compiler needs to turn regular code into stack restoring state machines. Furthermore, these features need to interact as expected, e.g. finally blocks must not be forgotten in the state machines for iterators. And all of this work needs to be done again for the next control flow abstraction that comes along. Or we can use algebraic effect handlers! This single mechanism generalizes all the control flow abstractions listed above and more, composes freely, has simple operational semantics, and can be efficiently compiled, since there is just one mechanism that needs to be supported well. Handlers allow programmers to keep the code in direct-style, which is easy to reason about, and empower library writers to implement various high-level abstractions without special extensions. The idea of algebraic effects handlers has already been experimented with in the form of small research languages and libraries in several mainstream languages, including OCaml, Haskell, Clojure, and Scala. The next step, and the aim of this seminar, is to seriously consider adoption by mainstream languages including both functional languages such as OCaml or Haskell, as well as languages like JavaScript and the JVM and .NET ecosystems.
Cite as

Sivaramakrishnan Krishnamoorthy Chandrasekaran, Daan Leijen, Matija Pretnar, and Tom Schrijvers. Algebraic Effect Handlers go Mainstream (Dagstuhl Seminar 18172). In Dagstuhl Reports, Volume 8, Issue 4, pp. 104-125, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{chandrasekaran_et_al:DagRep.8.4.104,
  author =	{Chandrasekaran, Sivaramakrishnan Krishnamoorthy and Leijen, Daan and Pretnar, Matija and Schrijvers, Tom},
  title =	{{Algebraic Effect Handlers go Mainstream (Dagstuhl Seminar 18172)}},
  pages =	{104--125},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{8},
  number =	{4},
  editor =	{Chandrasekaran, Sivaramakrishnan Krishnamoorthy and Leijen, Daan and Pretnar, Matija and Schrijvers, Tom},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.4.104},
  URN =		{urn:nbn:de:0030-drops-97623},
  doi =		{10.4230/DagRep.8.4.104},
  annote =	{Keywords: algebraic effect handlers, implementation techniques, programming abstractions, programming languages}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.22
The Essence of Nested Composition

Authors: Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
Calculi with disjoint intersection types support an introduction form for intersections called the merge operator, while retaining a coherent semantics. Disjoint intersections types have great potential to serve as a foundation for powerful, flexible and yet type-safe and easy to reason OO languages. This paper shows how to significantly increase the expressive power of disjoint intersection types by adding support for nested subtyping and composition, which enables simple forms of family polymorphism to be expressed in the calculus. The extension with nested subtyping and composition is challenging, for two different reasons. Firstly, the subtyping relation that supports these features is non-trivial, especially when it comes to obtaining an algorithmic version. Secondly, the syntactic method used to prove coherence for previous calculi with disjoint intersection types is too inflexible, making it hard to extend those calculi with new features (such as nested subtyping). We show how to address the first problem by adapting and extending the Barendregt, Coppo and Dezani (BCD) subtyping rules for intersections with records and coercions. A sound and complete algorithmic system is obtained by using an approach inspired by Pierce's work. To address the second problem we replace the syntactic method to prove coherence, by a semantic proof method based on logical relations. Our work has been fully formalized in Coq, and we have an implementation of our calculus.
Cite as

Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The Essence of Nested Composition. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 22:1-22:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bi_et_al:LIPIcs.ECOOP.2018.22,
  author =	{Bi, Xuan and Oliveira, Bruno C. d. S. and Schrijvers, Tom},
  title =	{{The Essence of Nested Composition}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{22:1--22:33},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Millstein, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.22},
  URN =		{urn:nbn:de:0030-drops-92275},
  doi =		{10.4230/LIPIcs.ECOOP.2018.22},
  annote =	{Keywords: nested composition, family polymorphism, intersection types, coherence}
}
Document
DOI: 10.4230/DARTS.4.3.5
The Essence of Nested Composition (Artifact)

Authors: Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

Published in: DARTS, Volume 4, Issue 3, Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
The artifact contains the Coq formalization of \name, a simple calculus with disjoint intersection types supporting nested subtyping and composition, as described in the companion paper.
Cite as

Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The Essence of Nested Composition (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{bi_et_al:DARTS.4.3.5,
  author =	{Bi, Xuan and Oliveira, Bruno C. d. S. and Schrijvers, Tom},
  title =	{{The Essence of Nested Composition (Artifact)}},
  pages =	{5:1--5:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2018},
  volume =	{4},
  number =	{3},
  editor =	{Bi, Xuan and Oliveira, Bruno C. d. S. and Schrijvers, Tom},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.5},
  URN =		{urn:nbn:de:0030-drops-92363},
  doi =		{10.4230/DARTS.4.3.5},
  annote =	{Keywords: nested composition, family polymorphism, intersection types, coherence}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact