DROPS

Document

Artifact

Elementary Type Inference (Artifact)

Authors: Jinxu Zhao and Bruno C. d. S. Oliveira

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract

This artifact contains the Appendix of the paper, proofs of theorems declared in the paper, and a sample implementation of the type inference algorithm. The proof contains 3 main results: soundness, completness and decidability of the type-inference algorithm. Moreover, there are several proofs about the declarative system and also a soundness/completeness proof between stable subtyping and a syntax-directed specification.

Cite as

Jinxu Zhao and Bruno C. d. S. Oliveira. Elementary Type Inference (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{zhao_et_al:DARTS.8.2.5,
  author =	{Zhao, Jinxu and Oliveira, Bruno C. d. S.},
  title =	{{Elementary Type Inference (Artifact)}},
  pages =	{5:1--5:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Zhao, Jinxu and Oliveira, Bruno C. d. S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.5},
  URN =		{urn:nbn:de:0030-drops-162036},
  doi =		{10.4230/DARTS.8.2.5},
  annote =	{Keywords: Type Inference}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2022.2

Elementary Type Inference

Authors: Jinxu Zhao and Bruno C. d. S. Oliveira

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract

Languages with polymorphic type systems are made convenient to use by employing type inference to avoid redundant type information. Unfortunately, features such as impredicative types and subtyping make complete type inference very challenging or impossible to realize. This paper presents a form of partial type inference called elementary type inference. Elementary type inference adopts the idea of inferring only monotypes from past work on predicative higher-ranked polymorphism. This idea is extended with the addition of explicit type applications that work for any polytypes. Thus easy (predicative) instantiations can be inferred, while all other (impredicative) instantiations are always possible with explicit type applications without any compromise in expressiveness. Our target is a System F extension with top and bottom types, similar to the language employed by Pierce and Turner in their seminal work on local type inference. We show a sound, complete and decidable type system for a calculus called F_{< :}^e, that targets that extension of System F. A key design choice in F_{< :}^e is to consider top and bottom types as polytypes only. An important technical challenge is that the combination of predicative implicit instantiation and impredicative explicit type applications, in the presence of standard subtyping rules, is non-trivial. Without some restrictions, key properties, such as subsumption and stability of type substitution lemmas, break. To address this problem we introduce a variant of polymorphic subtyping called stable subtyping with some mild restrictions on implicit instantiation. All the results are mechanically formalized in the Abella theorem prover.

Cite as

Jinxu Zhao and Bruno C. d. S. Oliveira. Elementary Type Inference. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 2:1-2:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{zhao_et_al:LIPIcs.ECOOP.2022.2,
  author =	{Zhao, Jinxu and Oliveira, Bruno C. d. S.},
  title =	{{Elementary Type Inference}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{2:1--2:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.2},
  URN =		{urn:nbn:de:0030-drops-162303},
  doi =		{10.4230/LIPIcs.ECOOP.2022.2},
  annote =	{Keywords: Type Inference}
}

Search Results

Documents authored by Zhao, Jinxu

Elementary Type Inference (Artifact)

Abstract

Cite as

Elementary Type Inference

Abstract

Cite as

Thanks for your feedback!

Could not send message