Gradual Typing for Functional Languages
2006 · paper · Computer science
Presents a type system for a lambda-calculus with optional type annotations, letting programmers mix static and dynamic typing. The authors prove it sound for fully annotated terms and type safe, and claim the cost of dynamism is pay-as-you-go.
Checked: PDF from scheme2006.cs.uchicago.edu, fetched 4 Oct 2026. Page numbers are those of that PDF.
4 findings
Substance Definition 1 requires only that "for every location l in the domain of Σ there exists a type τ such that Γ|Σ ⊢ µ(l) : τ". It never requires τ to equal Σ l, and with that weaker hypothesis Lemma 8 (Soundness of evaluation) is false as printed.
- p. 9 Definition 1
there exists a type τ such that Γ|Σ ⊢ µ(l) : τ
- p. 9 Definition 1
there exists a type τ such that Γ|Σ ⊢ µ(l) : τ.
- p. 9 Lemma 8
Soundness of evaluation
- p. 8 Figure 7, ELOC and EDEREF
(EDEREF)
Only the authors can say what is right here.
Judge's note: I read Definition 1 and Lemma 8 on p9, ELOC and EDEREF in Figure 7 on p8, and TLOC and TDEREF (TLOC needs Σ l = ⌊τ⌋). My own counterexample: Σ={l↦int}, µ={l↦#t}. The domains are equal and ∅|Σ ⊢ #t : bool, so Definition 1 holds. TLOC and TDEREF give ∅|Σ ⊢ !l : int. At n=2 the only derivation is ELOC (0<1), then EDEREF, giving #t|µ. EKILL needs depth 0, EDEREFP needs an error result and EDEREFT needs a non-location, so none of them applies. Lemma 8's conclusion then needs ∅|Σ′ ⊢ #t : int, which no Σ′ satisfies, and #t is neither CastError nor KillError. So the lemma fails as stated. The fix seems to be: for each l with Σ l = ⌊τ⌋, Γ|Σ ⊢ µ(l) : τ. The Isabelle development probably uses that form, but the printed definition does not. Theorem 2 starts from the empty store, so it is unaffected once the definition is corrected. All three reviewer notes describe this same defect.
Second check: another model agreed
Report a problem with this finding
Reference or label Reference [23] gives the author as "G. L. S. Jr.", so no surname appears.
- p. 11 Reference [23]
G. L. S. Jr.
Only the authors can say what is right here.
Judge's note: Rests on outside knowledge: that the author of 'An overview of COMMON LISP' (LFP '82) is Guy L. Steele Jr. Reference [23] on the page 11 image reads "G. L. S. Jr. An overview of COMMON LISP", so the entry plainly has no surname, which suggests a BibTeX name-parsing error. The correct name has to come from outside the files.
Second check: another model agreed
Report a problem with this finding
Reference or label Reference [24] lists the editors as "R. Kelsey, W. Clinger, and J. R. (eds.).", so the third editor's surname is missing.
- p. 11 Reference [24]
W. Clinger, and J. R. (eds.)
- p. 11 Reference [24]
R. Kelsey, W. Clinger, and J. R. (eds.).
Only the authors can say what is right here.
Judge's note: Rests on outside knowledge: that the third editor of R5RS is Jonathan Rees. Reference [24] on the page 11 image reads "R. Kelsey, W. Clinger, and J. R. (eds.).", so the third name has initials only and no surname.
Second check: another model agreed
Report a problem with this finding
Wording The cast rules in Figure 7 (e.g. ECSTR: "∅ | Σ ⊢ unbox v : ref τ") use a store typing Σ that does not appear in the evaluation judgment e|µ ↪n r|µ and is not tied to µ. A well-typed program can therefore be derived to evaluate to TypeError, which contradicts the prose gloss of Lemma 8 ("but never a type error"). The existential statements of Lemma 8 and Theorem 2 are not contradicted.
- p. 8 Figure 7, ECSTR
∅ | Σ ⊢ unbox v : ref τ
- p. 8 Figure 8, EAPPT
TypeError
- p. 9 Theorem 2
Theorem 2 (Type safety).
Only the authors can say what is right here.
Judge's note: I checked Figure 7 and Figure 8 on p8 and Lemma 8, Theorem 2 and the surrounding prose on p9. The judgment form is e|µ ↪n r|µ′, so the Σ in the premises of ECSTG, ECSTF, ECSTR and ECSTE is free and not linked to µ. I reworked the counterexample myself with µ={l↦1} and Σ0={l↦int}. The expression (!⟨ref(int→int)⟩⟨?⟩l) 1 is well typed at int: by TLOC, l has type ref int; ref int ~ ?; ? ~ ref(int→int); TDEREF gives int→int; TAPP gives int. Evaluation: ELOC gives l at depth 1. ECSTU gives ⟨?⟩l at depth 2, because unbox l = l. ECSTR, with a free Σ1 where Σ1 l = int→int, satisfies ∅|Σ1 ⊢ unbox(⟨?⟩l)=l : ref(int→int) and returns l at depth 3. EDEREF returns 1 at depth 4. Since 1 ∉ FunVal, EAPPT gives TypeError at depth 5. Lemma 8 and Theorem 2 only assert that some non-TypeError result exists, and here an alternative derivation exists, so the stated results stand. The step is still faulty, and so is the p9 claim that evaluation produces "never a type error". The text on p7 adds an inconsistency: it describes the premise as "∅| ∅⊢unbox v : τ, as in the rule (ECSTG)", while the figure prints ∅ | Σ. Only the authors, or the Isabelle source, can say how Σ is meant to be bound.
Second check: another model agreed
Report a problem with this finding
16 minor (typos and the like; most checked by the judge only)
Wording "The addition operator expects type number but gets an argument of type Ω." The example shown is (λ (x) (succ x)), which uses the constant succ and no addition operator.
- p. 4 Section 3, left column
The addition operator expects type number but gets an argument of type Ω.
Judge's note: Seen in crop C008-a (p.4). The only operator in the example is succ, which the paper elsewhere calls 'the succ constant' (p.7). The text loosely calls it an addition operator. The intent is clear, so this is minor.
Second check: another model agreed
Report a problem with this finding
Wording The text says "instead of the typing judgment ∅ | ∅ ⊢ unbox v : τ, as in the rule (ECSTG)", but rule (ECSTG) in Figure 7 has the premise ∅ | Σ ⊢ unbox v : γ.
- p. 7 Section 5.2, right column
instead of the typing judgment ∅ | ∅ ⊢ unbox v : τ, as in the rule (ECSTG)
- p. 8 Figure 7, rule (ECSTG)
∅ | Σ ⊢ unbox v : γ
Judge's note: Viewed crop C013-a (p.7) and Figure 7 on p.8. Every cast rule (ECSTG, ECSTF, ECSTR, ECSTE) types unbox v under the store typing Σ, not under ∅. The prose quotes the premise with an empty store typing and τ. The τ might be a deliberate generalisation, but the ∅ store typing contradicts the rule it cites.
Second check: another model agreed
Report a problem with this finding
Typo Ground types are called "number and boolean" (Section 3 and the examples), but the Introduction ("a value of type int must actually be an integer") and Lemma 5 ("If ∅ | Σ ⊢ v : int ... If ∅ | Σ ⊢ v : bool") use int/bool.
- p. 2 Introduction, Lemma 5 paragraph
a value of type int must actually be an integer
- p. 4 Section 3
ground types such as number and boolean
- p. 7 Lemma 5
If ∅ | Σ ⊢ v : int and v ∈ V then ∃n. v = n.
Judge's note: Viewed p.2 (crop C004-a) and p.7 (Lemma 5, which uses int and bool). The examples on p.7 use number and boolean, and Section 3 lists 'number and boolean' as ground types. The two naming schemes are never reconciled. The meaning is clear, so this is cosmetic.
Second check: none (judge only)
Report a problem with this finding
Typo "the run-time cost of dynamism in λ?→ can “pay-as-you-go”" is missing a word (should read "can be “pay-as-you-go”").
- p. 2 Introduction, Lemma 5 paragraph
cost of dynamism in λ?→can “pay-as-you-go”
- p. 2 Introduction
cost of dynamism in λ?
- p. 2 Introduction, paragraph on Lemma 5
can “pay-as-you-go”
Judge's note: Seen on the p.2 page image (crop C004-a). The subject is 'the run-time cost', so the sentence needs 'be'.
Second check: none (judge only)
Report a problem with this finding
Typo "two partial functions are consistent when every elements that is in the domain of both functions" should read "every element".
- p. 3 Section 2, left column
when every elements that is in the domain
- p. 3 Section 2, partial functions analogy
consistent when every elements that is in the domain
- p. 3 Section 2, partial functions analogy
every elements that is in the domain
Judge's note: Seen in crop C005-a (p.3, left column).
Second check: none (judge only)
Report a problem with this finding
Typo The relation ∼ is defined as "the consistency relation" but is called "type compatibility relation" (p.3 proof sketch of Theorem 1, p.10 BabyJ paragraph), and p.5 says "require the types to be compatible".
- p. 3 Proof sketch of Theorem 1
type compatibility relation collapses to type equality
- p. 10 Section 7, BabyJ paragraph
our type compatibility relation ∼ takes into account function types
- p. 3 Section 2, definition
We axiomatize the consistency relation ∼ on types
Judge's note: Viewed crops C006-a (p.3) and C006-b (p.10), and the p.5 text in crop C009-a. The same relation ∼ is named two ways, and the alternative name is never introduced. The meaning is recoverable from the symbol, so this is a minor terminology inconsistency.
Second check: none (judge only)
Report a problem with this finding
Typo "e ← e stores the value form the right-hand side expression" should read "from".
- p. 5 Section 4
stores the value form the right-hand side expression
- p. 5 Section 4
value form the right-hand side expression
- p. 6 Section 5.2
syntacical
- p. 6 Section 5.1
occuring
Judge's note: Seen in crop C009-a (p.5). The 'syntacical' and 'occuring' items in this cluster are judged under C012 and C011.
Second check: none (judge only)
Report a problem with this finding
Typo "which means that references types are invariant" should read "reference types".
- p. 5 Section 4
which means that references types are invariant
Judge's note: Seen at the bottom of the left column of p.5 in crop C009-a.
Second check: none (judge only)
Report a problem with this finding
Typo "to prevent type errors from occuring at run-time" should read "occurring".
- p. 6 Section 5.1, after Lemma 4
prevent type errors from occuring
- p. 6 Section 5.1 and 5.2
syntacical
- p. 6 Section 5.1 after Lemma 4
occuring
- p. 6 Section 5.1
type errors from occuring
Judge's note: Seen in crop C011-a (p.6, right column).
Second check: none (judge only)
Report a problem with this finding
Typo "which serves as a syntacical representation of boxed values" should read "syntactical".
- p. 6 Section 5.2, first paragraph
which serves as a syntacical repre-
- p. 6 Section 5.2
syntacical
Judge's note: Seen in crop C012-a (p.6, Section 5.2).
Second check: none (judge only)
Report a problem with this finding
Typo Lemma 6, third bullet reads "If Γ | Σ ⊢ e : τ and ⋀l. If l ∈ dom Σ then Σ′ l = Σ l. then Γ | Σ′ ⊢ e : τ.": a nested if-then with its own full stop leaves the malformed sequence ". then".
- p. 9 Lemma 6, third bullet
If l ∈ dom Σ then Σ′ l = Σ l. then Γ | Σ′ ⊢ e : τ.
Judge's note: I checked the page 9 image. The third bullet of Lemma 6 is printed exactly as quoted, with an inner "If … then … ." inside the outer implication and a stray full stop before "then Γ | Σ′ ⊢ e : τ". The intended meaning can still be worked out (for all l in dom Σ, Σ′ l = Σ l), so this is a presentation slip, not a mathematical error.
Second check: none (judge only)
Report a problem with this finding
Typo "et. all" is printed for "et al.": "casts of Abadi et. all [1]" (Section 6, p. 9) and "Ou et. all. [31]" (Section 7, p. 10).
- p. 9 Section 6
casts of Abadi et. all [1]
- p. 9 Section 6
Abadi et. all [1]
- p. 10 Related work
Ou et. all. [31]
Judge's note: The page images confirm "Abadi et. all [1]" in the first paragraph of Section 6 on page 9 and "Ou et. all. [31]" on page 10. The Section 6 heading spells it correctly ("Abadi et al."), and so does "Gray et al." on page 9.
Second check: none (judge only)
Report a problem with this finding
Typo Number mismatch: "applies to all terminating programs and does not apply to non-terminating program, as we intend" should end "non-terminating programs".
- p. 9 Section 5.4
does not apply to non-terminating program
- p. 9
does not apply to non-terminating program, as we intend.
Judge's note: The page 9 image shows the phrase running across the column break from the left column to the right column. The parallel phrase "terminating programs" earlier in the same sentence is plural, so the singular "program" is a slip.
Second check: none (judge only)
Report a problem with this finding
Typo The Conclusion's "migrating between dynamic to static could take place gradually" mixes "between … and" with "from … to".
- p. 10 Section 8, first paragraph
migrating between dynamic to static
- p. 10 Section 8 Conclusion, first paragraph
migrating between dynamic to static could take place gradually
Judge's note: Confirmed on the page 10 image, in the first paragraph of Section 8. It is a grammatical slip only.
Second check: none (judge only)
Report a problem with this finding
Typo The Acknowledgments omit a conjunction: "We thank Emir Pasalic the members of the Resource Aware Programming Laboratory" (should be "Emir Pasalic and the members").
- p. 10 Acknowledgments
Emir Pasalic the members of the Resource Aware Programming
- p. 10 Acknowledgments
Emir Pasalic the members of the Resource Aware Programming Laboratory
Judge's note: Confirmed on the page 10 image, in the Acknowledgments paragraph.
Second check: none (judge only)
Report a problem with this finding
Typo Subject–verb agreement: "The type system and run-time semantics of λ?→ is relatively straightforward" has a compound subject with a singular verb.
- p. 10 Section 8 Conclusion, second paragraph
The type system and run-time seman-tics of λ? → is relatively straightforward
- p. 10 Conclusion
run-time semantics of λ
Judge's note: Confirmed on the page 10 image, in the second paragraph of the Conclusion. It is a minor grammar slip.
Second check: none (judge only)