Dependent Types in Practical Programming
Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1999 · paper · Computer science
Proposes adding a restricted form of dependent types to ML, with type indices drawn from a constraint domain. Type-checking reduces to constraint satisfaction, the extension is proved conservative over ML, and a prototype exists for integer linear-inequality constraints.
Checked: PDF from cs.cmu.edu, fetched 4 Oct 2026. Page numbers are those of that PDF.
3 findings
Wording (ty-cons-w) in Fig. 6 types only "φ; Γ ⊢ c[⃗i](v) : δ(i[⃗a :=⃗i])" with a value argument v. Fig. 4 allows c[i1]...[in](e), and p.4 claims that cons[a + n](⟨x, append[a][n](⟨xs, ys⟩)⟩) is derivable "using the rules for expressions from Figure 6".
- p. 5 Figure 6, (ty-cons-w)
φ; Γ ⊢ v : τ[⃗a :=⃗i]
- p. 4 Figure 4, expressions
c[i1] . . . [in](e)
- p. 13 Figure 13, (elab-cons-w-up)
c[i1] . . . [in](e∗)
- p. 5 Figure 6, rule (ty-cons-w)
φ; Γ ⊢ c[⃗i](v) : δ(i[⃗a :=⃗i])
Only the authors can say what is right here.
Judge's note: Fig. 6 (p.5): the premise is φ; Γ ⊢ v : τ[⃗a:=⃗i] and the conclusion is c[⃗i](v). No other rule in Fig. 6 concludes a typing for a constructor application, and (ty-eq) does not change the term. Value grammars (Figs. 3–4): v ::= x | c(v) | ⟨⟩ | ⟨v1,v2⟩ | lam x:τ.e | c[i]..(v) | λa:γ.v. An application e1(e2) is therefore not a value. So ⟨x, append[a][n](⟨xs,ys⟩)⟩ is not a value, and the p.4 derivability claim does not go through under the rules as printed. (elab-cons-w-up) in Fig. 13 also outputs c[i1]...[in](e*) for an arbitrary e*, which Theorem 5.1(1) says is typable. The likely intent is e in place of v. With that change the stated results appear to stand, hence S3.
Second check: another model agreed
Report a problem with this finding
Wording Fig. 6's only rule for argument-less constructors, (ty-cons-wo), requires "S(c) = δ(i)", but (elab-cons-wo-up) in Fig. 13 elaborates c with "S(c) = Πa1 : γ1 . . . Πan : γn.δ(i)" to c[i1]...[in]. No typing rule covers that output, which Theorem 5.1(1) claims is typable.
- p. 5 Figure 6, rule (ty-cons-wo)
S(c) = δ(i)
- p. 13 Figure 13, rule (elab-cons-wo-up)
S(c) = Πa1 : γ1 . . . Πan : γn.δ(i)
- p. 7 Theorem 5.1(1)
then φ; Γ ⊢e∗: τ is derivable
Only the authors can say what is right here.
Judge's note: Checked the figures. (ty-cons-wo) in Fig. 6 assigns c the type δ(i) only when S(c) has no Π prefix. Because of that, (ty-iapp) cannot be used to apply c to indices either. (elab-cons-wo-up) in Fig. 13 produces c[i1]...[in] of type δ(i[a:=i]). The expression grammar in Fig. 4 lists only c[i1]...[in](e), with an argument. Theorem 5.1(1) on p.7 says the elaborated term is typable, but the printed rules give no derivation for an index-quantified nullary constructor. One <| {n:nat} lamexp(n+1) in Fig. 2 is an example from the paper itself. Adding the obvious typing rule appears to fix this, so the stated result likely stands (S3). Only the authors can confirm the intended rule.
Second check: another model agreed
Report a problem with this finding
Wording The (elab-let-down) rule displayed in Section 5.2 (p.7) has the conclusion "φ; Γ, x : τ1 ⊢ let x = e1 in e2 end ↓ τ2 ⇒ e∗"; the context should be φ; Γ, as in Fig. 14.
- p. 7 Section 5.2, rule displayed after 'as illustrated in the rule (elab-let-down) below'
φ; Γ, x : τ1 ⊢ let x = e1 in e2 end ↓ τ2 ⇒ e∗
- p. 14 Figure 14, (elab-let-down)
φ; Γ ⊢ let x = e1 in e2 end ↓ τ2 ⇒ let x = e∗
- p. 7 rule (elab-let-down), conclusion
φ; Γ, x : τ1 ⊢ let x = e1 in e2 end ↓ τ2 ⇒ e*
- p. 14 Figure 14, rule (elab-let-down)
φ; Γ ⊢ let x = e1 in e2 end ↓ τ2 ⇒ let x = e1* in e2* end
Judge's note: The p.7 image shows Γ, x : τ1 in the conclusion, while the first premise is φ; Γ ⊢ e1 ↑ τ1. Fig. 14 (p.14) states the same rule with conclusion φ; Γ ⊢ let x = e1 in e2 end ↓ τ2 ⇒ let x = e1* in e2* end. This matches (ty-let) in Fig. 6. The let binds x, so x cannot already be in the conclusion's context. The two statements of the rule disagree, and the body version is the wrong one.
Second check: another model agreed
Report a problem with this finding
20 minor (typos and the like; most checked by the judge only)
Wording Type equality is introduced as "the judgment φ ⊢ τ1 ≡ τ2" (p.3, also p.4 "φ ⊢ intlist((a+n)+1) ≡ intlist(m+n)"), but (ty-eq) in Fig. 6 and the *-down rules in Figs. 13–14 write "φ |= τ1 ≡ τ2" / "φ |= µ1 ≡ µ2".
- p. 3 Section 4, text before the congruence rules
uses the judgment φ ⊢ τ1 ≡ τ2
- p. 5 Figure 6, (ty-eq)
φ |= τ1 ≡ τ2
- p. 13 Figure 13, (elab-var-down)
φ |= µ1 ≡ µ2
- p. 3 Section 4, definition of type conversion judgment
uses the judgment φ ⊢τ1 ≡τ2 which is the congruent ex-
Judge's note: Page 3 text and congruence rules use ⊢. In Fig. 6, (ty-eq) has the premise φ |= τ1 ≡ τ2. In Figs. 13–14, (elab-var-down), (elab-cons-*-down), (elab-app-down) and (elab-anno-down) use φ |= µ1 ≡ µ2. The paper defines |= only as satisfaction of index constraints Φ. Nothing in the paper says that |= on types abbreviates the ⊢ judgment. The meaning is recoverable, so this is a notational inconsistency, not a substantive error.
Second check: another model agreed
Report a problem with this finding
Typo Section 1, first sentence prints "or Haskell!(Hudak, Peyton Jones, and Wadler 1992)": a stray "!" follows "Haskell" and there is no space before the citation.
- p. 1 Section 1, first sentence
Haskell!(Hudak, Peyton Jones, and Wadler 1992)
Judge's note: Crop of page 1 shows "Haskell!(Hudak, ..." while the neighbouring items read "Standard ML (Milner, ...)" and "Caml (Weis and Leroy 1993)". The character is on the page, not an extraction artefact.
Second check: none (judge only)
Report a problem with this finding
Typo The abstract lists "higher-order functions, general recursions, let-polymorphism" while Section 1 (page 2) lists "higher-order functions, general recursion, let-polymorphism".
- p. 1 Abstract
higher-order functions, general recursions, let-polymorphism
- p. 2 Section 1
higher-order functions, general recursion, let-polymorphism
Judge's note: Both crops read as quoted. The plural in the abstract is a small wording inconsistency for the same feature list; meaning is unaffected.
Second check: none (judge only)
Report a problem with this finding
Typo Page 2 prints the de Bruijn term as "Abs(Abs(App(Shift(One),One))." with four opening and three closing parentheses; the term needs one more ")": Abs(Abs(App(Shift(One),One))).
- p. 2 Section 1, paragraph on Figure 2
Abs(Abs(App(Shift(One),One))
Judge's note: Crop of page 2 shows the term followed directly by the sentence's full stop. Counted on the image: opening after Abs, Abs, App, Shift (4); closing one after the first One and two after the second One (3).
Second check: none (judge only)
Report a problem with this finding
Typo Index-constraint grammar (p.3) reads "Φ ::= P | Φ1 ∧ Φ1 | P ⊃ Φ | …"; the conjunction should be Φ1 ∧ Φ2.
- p. 3 Section 3, grammar line 'index constraints'
P | Φ1 ∧ Φ1 | P ⊃ Φ
- p. 3 Section 3, grammar of index constraints
P | Φ1 ∧ Φ1 | P ⊃ Φ |
- p. 3 Section 3, index constraints grammar
Φ1 ∧Φ1
Judge's note: The page 3 image shows subscript 1 on both conjuncts. The proposition grammar just above uses P1 ∧ P2 | P1 ∨ P2, so the second operand is clearly meant to be Φ2. This is a typographical slip.
Second check: none (judge only)
Report a problem with this finding
Typo Section 3 prints "We use f for interpreted functions symbols"; should be "function symbols".
- p. 3 Section 3, second paragraph
terpreted functions symbols
- p. 3 Section 3, first paragraph
We use f for in-terpreted functions symbols
Judge's note: Crop of page 3 shows "in-terpreted functions symbols, p for atomic predicates". Grammatical slip.
Second check: none (judge only)
Report a problem with this finding
Typo Figure 4 constructor signature reads "S ::= · | S, c : Πa1 : γ1 . . . Πan : γm.τ → δ(i)"; the last sort should be γn.
- p. 4 Figure 4, constructor signature
Πa1 : γ1 . . . Πan : γm.τ → δ(i)
- p. 13 Figure 13, (elab-cons-w-up)
S(c) = Πa1 : γ1 . . . Πan : γn.τ → δ(i)
- p. 4 Figure 4, constructor signature
Πan : γm
- p. 13 Figure 13, (elab-cons-wo-up)
Πan : γn
Judge's note: The Fig. 4 crop shows Πan : γm, and m is never introduced. The same signature in Fig. 13 (elab-cons-wo-up, elab-cons-w-up) is written Πa1 : γ1 . . . Πan : γn. Each binder carries one sort, so the subscripts must match.
Second check: none (judge only)
Report a problem with this finding
Typo Figure 5: the two branches of the case expression ("⟨nil, ys⟩ ⇒ ys" and the cons branch on the next line) are not separated by "|", although the syntax of matches is "(p ⇒ e) | (p ⇒ e | ms)".
- p. 5 Figure 5, case expression
⟨nil, ys⟩ ⇒ ys
- p. 4 Figure 3, matches
(p ⇒ e) | (p ⇒ e | ms)
Judge's note: Zoomed render of Figure 5 shows the two branches on consecutive lines with no bar; Figure 3 on page 4 gives matches with the bar, and the sugared version below in Figure 5 does use "|". Could be a display layout choice; cosmetic.
Second check: none (judge only)
Report a problem with this finding
Typo Theorem 4.4 prints "If e →d v derivable in MLΠ0(C), then ‖e‖ →0 ‖v‖ is derivable"; "is" is missing before the first "derivable".
- p. 6 Theorem 4.4
If e →d v derivable in
Judge's note: Crop of page 6 shows the sentence as quoted. Theorems 4.3 and 4.5 use "is derivable" / "derivable" with a verb.
Second check: none (judge only)
Report a problem with this finding
Typo Page 6 prints "this alternative leads some (unnecessary) complications"; "to" is missing after "leads".
- p. 6 Section 4, paragraph after Theorem 4.6
this alternative leads some (unnecessary)
Judge's note: Crop of page 6 shows the sentence as quoted.
Second check: none (judge only)
Report a problem with this finding
Typo Section 5 prints "a serious drawback from a programmer's point view"; "of" is missing ("point of view").
- p. 6 Section 5, first paragraph
mer’s point view
- p. 6 Section 5, first paragraph
from a program-mer’s point view
Judge's note: Crop of page 6 shows "program-mer's point view:". Page 2 has "pragmatic point of view".
Second check: none (judge only)
Report a problem with this finding
Typo (elab-lam) as displayed on p.7 concludes "(lam x : τ1.e∗1)" although its premise produces e∗; Fig. 14 has "(lam x : τ1.e∗)".
- p. 7 Section 5.2, rule for lambda abstraction (elab-lam)
(lam x : τ1.e∗
- p. 14 Figure 14, (elab-lam)
φ; Γ ⊢ (lam x.e) ↓ τ1 → τ2 ⇒ (lam x : τ1.e∗) (elab-lam)
- p. 7 Section 5.2, rule (elab-match)
φ; Γ ⊢ (p ⇒ e) ↓ (τ1 ⇒ τ2) ⇒ (p∗ ⇒ e∗
- p. 7 Section 5.2, displayed rule for lam
(lam x : τ1.e∗1)
Judge's note: The p.7 crop clearly shows a subscript 1 on e∗ in the conclusion. The premise φ; Γ, x : τ1 ⊢ e ↓ τ2 ⇒ e∗ never binds e∗1. Fig. 14 has plain e∗. The same slip in (elab-match) is judged separately under C017.
Second check: none (judge only)
Report a problem with this finding
Typo (elab-match) as displayed on p.7 concludes "(p∗ ⇒ e∗1)" although its premise produces e∗; Fig. 14 has "(p∗ ⇒ e∗)".
- p. 7 Section 5.2, rule after 'the declarations in φ′ are treated as hypotheses'
φ; Γ ⊢ (p ⇒ e) ↓ (τ1 ⇒ τ2) ⇒ (p∗ ⇒ e∗
- p. 14 Figure 14, (elab-match)
φ; Γ ⊢ (p ⇒ e) ↓ (τ1 ⇒ τ2) ⇒ (p∗ ⇒ e∗)
- p. 7 Section 5.2, displayed rule (elab-match)
(p∗⇒e∗1)
- p. 14 Figure 14, (elab-match)
(p∗⇒e∗)
Judge's note: The p.7 crop shows the subscript 1 on e∗ in the conclusion. The premise φ, φ′; Γ, Γ′ ⊢ e ↓ τ2 ⇒ e∗ binds only e∗. Fig. 14 prints (p∗ ⇒ e∗). The p.7 version also leaves out the premise φ ⊢ τ2 : ∗, but that point was not raised.
Second check: none (judge only)
Report a problem with this finding
Typo The proof of Theorem 5.1 says "induction on the derivations of Γ ⊢ e ↑ τ ⇒ e∗ and φ; Γ ⊢ e ↓ τ ⇒ e∗"; the first judgment is missing the index context "φ;".
- p. 7 Proof of Theorem 5.1
derivations of Γ ⊢ e ↑
- p. 7 Proof of Theorem 5.1
derivations of Γ ⊢e ↑ τ ⇒e∗and φ; Γ ⊢e ↓τ ⇒e∗
- p. 7 Proof of Theorem 5.1
derivations of Γ ⊢e ↑ τ ⇒e∗
Judge's note: The p.7 crop shows "Γ ⊢ e ↑ τ ⇒ e∗" with no φ. The theorem statement and the second judgment in the same sentence both use φ; Γ. This is a trivial slip and the meaning is clear.
Second check: none (judge only)
Report a problem with this finding
Typo Section 8.1: "all leaves are marked black and all other node are marked either red or black"; "node" should be "nodes".
- p. 8 Section 8.1, first paragraph
and all other node are marked either red or black
- p. 8 Section 8.1, condition (a)
all other node are marked either red or black
- p. 8 Section 8.1, condition (a)
all leaves are marked black and all other node are marked either red or black
Judge's note: The page 8 image, right column, Section 8.1, prints "and all other node are marked either red or black". Singular noun with a plural verb.
Second check: none (judge only)
Report a problem with this finding
Typo Section 9: "He works in the context of of lazy functional programming." The word "of" is printed twice.
- p. 9 Section 9, second paragraph
He works in the context of of
- p. 9 Section 9, paragraph on Zenger
in the context of of
- p. 9 Section 9, Related Work, paragraph on Zenger
He works in the context of of lazy functional programming.
- p. 9
97)). He works in the context of of lazy functional pro
Judge's note: The page 9 image, right column, shows the line ending "He works in the context of of" and the next line starting "lazy functional programming". Both "of"s are on the same printed line, so this is a duplicated word in the PDF and not an extraction artefact.
Second check: code check
Report a problem with this finding
Typo Appendix A: "have difficulty accessing (Xi 1997), where complete these and other larger examples are available." The word "complete" is misplaced.
- p. 11 Appendix A, first sentence
where complete these
- p. 11 Appendix A, first paragraph
where complete these and other larger examples are available
Judge's note: The page 11 image, first sentence of Appendix A, prints "where complete these and other larger examples are available". The word order is garbled as printed. The likely intent is "where these and other larger complete examples are available" or "complete versions of these", but the exact fix is the authors' to choose.
Second check: none (judge only)
Report a problem with this finding
Typo Appendix A: "The depe-dent type checker verifies" spells the word "depedent"; it should be "dependent".
- p. 11 Appendix A, third paragraph
The depe-
- p. 11 Appendix A, paragraph on Figure 10
The depe-dent type checker
Judge's note: The page 11 image shows the line ending "The depe-" and the next line starting "dent type checker verifies". Joined, this gives "depedent", with the "n" missing.
Second check: none (judge only)
Report a problem with this finding
Typo Reference entry for Sannella and Tarlecki (1989): "Depatment of Computer Science, University of Edinburgh"; should be "Department".
- p. 11 References, Sannella and Tarlecki (1989)
Depatment of Computer
- p. 11 References, Sannella and Tarlecki (1989)
Depatment of Computer Science, University of Edinburgh
Judge's note: The page 11 image, reference list, Sannella and Tarlecki entry, prints "Foundations of Computer Science, Depatment of Computer Science, University of Edinburgh". Misspelling.
Second check: none (judge only)
Report a problem with this finding
Typo Reference entry for Parent (1995): "In Proceedings of the International Conference on Mathematics for Programs Constructions. Springer-Verlag LNCS 947." The conference name appears garbled (probably "Mathematics of Program Construction").
- p. 11 References, Parent (1995)
International Conference on Mathematics for Programs
Only the authors can say what is right here.
Judge's note: Rests on outside knowledge: that the conference published as Springer LNCS 947 is titled "Mathematics of Program Construction" (MPC '95). The page 11 image does print "International Conference on Mathematics for Programs Constructions. Springer-Verlag LNCS 947". The doubled plural "Programs Constructions" is awkward on its face, but the correct title cannot be verified from the files, so this goes to the authors as a query.
Second check: none (judge only)