Fixed Points of Type Constructors and Primitive Recursion (Errata)

Andreas Abel and Ralph Matthes

October 19, 2004

Abstract

Our contribution to CSL 04 [AM04] contains a little error, which is easily corrected by 2 elementary editing steps (replacing one character and deleting another).

Definition of wellformed contexts (fifth page). Typing contexts should, in contrast to kinding contexts, only contain type variable declarations without variance information. Hence, the second rule is too liberal; we must insist on p = ∘. The corrected set of rules is then:

\overline{⋄ cxt}  \frac{Δ cxt}{Δ, X^{∘κ} cxt}  \frac{Δ cxt  Δ ⊢ A : ∗}{Δ, x:A cxt}

Definition of welltyped terms (immediately following). Since wellformed typing contexts Δ contain no variance information, hence ∘Δ = Δ, we might drop the “∘” in the instantiation rule (fifth rule). The new set of rules is consequently,

\frac{(x:A) ∈ Δ  Δ cxt}{Δ ⊢ x : A}  \frac{Δ, x:A ⊢ t : B}{Δ ⊢ λx.t : A → B}  \frac{Δ ⊢ r : A → B  Δ ⊢ s : A}{Δ ⊢ r s : B}

\frac{Δ, X^{∘κ} ⊢ t : A}{Δ ⊢ t : ∀X^{κ}. A} \frac{Δ ⊢ t : ∀X^{κ}. A Δ ⊢ F : κ}{Δ ⊢ t : [F/X]A} \frac{Δ ⊢ t : A Δ ⊢ A = B : ∗}{Δ ⊢ t : B}

Lemma 4 fails if we allow variance information in contexts. Consider the typing

X^{+∗} ⊢ λx.x : X → X

which would imply X^{+∗} ⊢ X → X : ∗, a clearly wrong statement, since X → X is of mixed variance. With the corrected definition of wellformed typing contexts, Lemma 4 holds.

References

[AM04] Andreas Abel and Ralph Matthes. Fixed points of type constructors and primitive recursion. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, CSL’04, volume 3210, pages 190–204, 2004.