InferType: A Compiler Toolkit for Implementing Efficient Constraint-Based Type Inference (Artifact)

Authors Senxi Li , Tetsuro Yamazaki , Shigeru Chiba



PDF
Thumbnail PDF

Artifact Description

DARTS.10.2.11.pdf
  • Filesize: 460 kB
  • 2 pages

Document Identifiers

Author Details

Senxi Li
  • The University of Tokyo, Japan
Tetsuro Yamazaki
  • The University of Tokyo, Japan
Shigeru Chiba
  • The University of Tokyo, Japan

Acknowledgements

This work was supported by JSPS KAKENHI Grant Numbers JP20H00578 and JP24H00688.

Cite AsGet BibTex

Senxi Li, Tetsuro Yamazaki, and Shigeru Chiba. InferType: A Compiler Toolkit for Implementing Efficient Constraint-Based Type Inference (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 11:1-11:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/DARTS.10.2.11

Artifact

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2024 Call for Artifacts and the ACM Artifact Review and Badging Policy.

Abstract

Supporting automatic type inference is in demand in modern language development. It is a challenging task but without appropriate supporting toolkits. This paper presents InferType, a Java library that helps implement constraint-based type inference. A compiler writer uses InferType’s classes and methods to describe type constraints and typing rules for type inference. InferType then performs constraint solving by translation to the Z3 SMT solver. InferType is equipped with our developed optimization technique. It reduces the search space for type variables by pre-computing the structures of those type variables for mitigating the performance bottleneck of constraint solving with deeply nested types. We use InferType to implement type inference for a subset of Python, and conduct experiments to evaluate how the developed optimization technique can affect the performance of type inference. Our results show that InferType’s optimization can greatly mitigate the performance bottleneck for programs with deeply nested types, and can potentially improve the performance for large nested types.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Domain specific languages
  • Theory of computation → Type theory
Keywords
  • Domain Specific Languages
  • Compilation
  • Static Analysis
  • Type Inference
  • Constraint Solving
  • SMT Solver

Metrics

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