RECORD
Dynamic Type Inference for Gradual Hindley--Milner Typing
Programming Languages · Submitted 30 Oct 2018
abstract compiled · 2026-09-23 · no language-model review
The authors' main claim The DTI-based semantics not only avoids the divergence described above but also is sound and complete with respect to the semantics of fully instantiated terms in the following sense: if the evaluation of a term succeeds (i.e., terminates with a value) in the DTI-based semantics, then there is a fully instantiated version of the term that also succeeds in the explicitly typed blame calculus and vice versa.
The compiled record
The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
Open the compiled record
The abstract, sentence by sentence
Garcia and Cimini study a type inference problem for the ITGL, an implicitly and gradually typed language with let-polymorphism, and develop a sound and complete inference algorithm for it. Soundness and completeness mean that, if the algorithm succeeds, the input term can be translated to a well-typed term of an explicitly typed blame calculus by cast insertion and vice versa. However, in general, there are many possible translations depending on how type variables that were left undecided by static type inference are instantiated with concrete static types. Worse, the translated terms may behave differently---some evaluate to values but others raise blame. In this paper, we propose and formalize a new blame calculus $\lambda^{\textsf{DTI}}_{\textsf{B}}$ that avoids such divergence as an intermediate language for the ITGL. A main idea is to allow a term to contain type variables (that have not been instantiated during static type inference) and defer instantiation of these type variables to run time. We introduce dynamic type inference (DTI) into the semantics of $\lambda^{\textsf{DTI}}_{\textsf{B}}$ so that type variables are instantiated along reduction. The DTI-based semantics not only avoids the divergence described above but also is sound and complete with respect to the semantics of fully instantiated terms in the following sense: if the evaluation of a term succeeds (i.e., terminates with a value) in the DTI-based semantics, then there is a fully instantiated version of the term that also succeeds in the explicitly typed blame calculus and vice versa. Finally, we prove the gradual guarantee, which is an important correctness criterion of a gradually typed language, for the ITGL.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | Garcia and Cimini study a type inference problem for the ITGL, an implicitly and gradually typed language with let-polymorphism, and develop a sound and complete inference algorithm for it. | background 0.84 | 0.06 | 0.10 | asserted 1.00 |
| s1 | Soundness and completeness mean that, if the algorithm succeeds, the input term can be translated to a well-typed term of an explicitly typed blame calculus by cast insertion and vice versa. | interpretation 0.60 | 0.14 | 0.05 | asserted 1.00 |
| s2 | However, in general, there are many possible translations depending on how type variables that were left undecided by static type inference are instantiated with concrete static types. | background 0.74 | 0.14 | 0.03 | asserted 0.95 |
| s3 | Worse, the translated terms may behave differently---some evaluate to values but others raise blame. | background 0.81 | 0.14 | 0.03 | hedged possibility 0.76 |
| s4 | In this paper, we propose and formalize a new blame calculus $\lambda^{\textsf{DTI}}_{\textsf{B}}$ that avoids such divergence as an intermediate language for the ITGL. | contribution 1.00 | 0.95 | 0.44 | asserted 1.00 |
| s5 | A main idea is to allow a term to contain type variables (that have not been instantiated during static type inference) and defer instantiation of these type variables to run time. | method 0.81 | 0.82 | 0.10 | asserted 0.93 |
| s6 | We introduce dynamic type inference (DTI) into the semantics of $\lambda^{\textsf{DTI}}_{\textsf{B}}$ so that type variables are instantiated along reduction. | method 0.92 | 0.94 | 0.08 | asserted 1.00 |
| s7 | The DTI-based semantics not only avoids the divergence described above but also is sound and complete with respect to the semantics of fully instantiated terms in the following sense: if the evaluation of a term succeeds (i.e., terminates with a value) in the DTI-based semantics, then there is a fully instantiated version of the term that also succeeds in the explicitly typed blame calculus and vice versa. | result 0.92 | 0.91 | 0.40 | asserted 1.00 |
| s8 | Finally, we prove the gradual guarantee, which is an important correctness criterion of a gradually typed language, for the ITGL. | contribution 0.61 | 0.95 | 0.23 | asserted 1.00 |
What was examined, and what was not
- arXiv listing abstract v2
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
The paper
Original abstract
Garcia and Cimini study a type inference problem for the ITGL, an implicitly and gradually typed language with let-polymorphism, and develop a sound and complete inference algorithm for it. Soundness and completeness mean that, if the algorithm succeeds, the input term can be translated to a well-typed term of an explicitly typed blame calculus by cast insertion and vice versa. However, in general, there are many possible translations depending on how type variables that were left undecided by static type inference are instantiated with concrete static types. Worse, the translated terms may behave differently---some evaluate to values but others raise blame. In this paper, we propose and formalize a new blame calculus $\lambda^{\textsf{DTI}}_{\textsf{B}}$ that avoids such divergence as an intermediate language for the ITGL. A main idea is to allow a term to contain type variables (that have not been instantiated during static type inference) and defer instantiation of these type variables to run time. We introduce dynamic type inference (DTI) into the semantics of $\lambda^{\textsf{DTI}}_{\textsf{B}}$ so that type variables are instantiated along reduction. The DTI-based semantics not only avoids the divergence described above but also is sound and complete with respect to the semantics of fully instantiated terms in the following sense: if the evaluation of a term succeeds (i.e., terminates with a value) in the DTI-based semantics, then there is a fully instantiated version of the term that also succeeds in the explicitly typed blame calculus and vice versa. Finally, we prove the gradual guarantee, which is an important correctness criterion of a gradually typed language, for the ITGL.
Human review
Discussion
Know something about this paper? Leave a comment, or highlight any passage above to comment on it.