5
$\begingroup$

In Types and Programming Language's constraint typing rules (Figure 22-1), is it possible for any part of the typing derivation to contain free type variables that aren’t part of the fresh variables? Because the typing rules are based on the simply-typed lambda calculus with an infinite number of base types, a naïve reading would allow for $\Gamma$, $t$, or $T$ to contain type variables not mentioned in $\chi$. However, given that TAPL hasn't introduced polymorphism yet, I wonder if this case should implicitly be considered "invalid."

For a concrete example: Should $\varnothing \vdash (\lambda \, x : X \rightarrow X, \, 0) \, (\lambda \, x : X, \, x) : \mathbb{N}$ be considered to have a "valid" constraint typing derivation, even though $X$ wouldn't be mentioned in the resulting $\chi$?


Figure 22-1 from TAPL, for reference:

Figure 22-1, TAPL


EDIT: This question has been significantly edited in response to @frabala's answer, which made me realize that I hadn't been very clear initially. Hopefully it makes more sense now: See the edits and comments on @frabala's answer for a targeted answer to my question as currently written.

$\endgroup$
0
3
$\begingroup$

Not sure whether I completely understand the question, but here is my attempt:

a naïve reading would allow for Γ, t, or T to contain type variables not mentioned in χ.

$\Gamma$, $t$ and $T$ may contain type variables not mentioned in $\mathcal{X}$. The set $\mathcal{X}$ contains only unification variables. That is, fresh variables generated by the typing process (in particular, by rule CT-App, where it is explicitly stated that the new unification variable $X$ should not appear in $\Gamma$, $t$, $T$, etc). Try exercise 22.3.3. In the process of building a derivation for the judgment shown there, $\Gamma$ will end-up containing the type variables $X$, $Y$ and $Z$ (which initially are part of the term $t$) and those variables will not belong in $\mathcal{X}$ at any point of the derivation.

I think my question is actually if any of Γ, t, or T can have free type variables (i.e. that haven't been introduced by the type-inference rules).

$\Gamma$ can have type variables not introduced by the rules. For example, the term $(\lambda y : B.y)$ of the polymorphic type $B \to B$ is typable under some environment like $\Gamma = x:A$ (and to avoid ambiguity, one needs to make sure that the identifiers $x$ and $y$ are distinct). This would be another way to encode constants in a language. For example, instead of having the rule CT-Zero, we could always type a term under the unvironment $\Gamma_0 = 0 : \mathrm{Nat}$.

Regarding the term $t$, this term is given and therefore, so are the type variables that it contains. So, the type variables in $t$ are certainly not introduced by the rules. The rules only manipulate the environment $\Gamma$, the type $T$, the unification variables $\mathcal{X}$ and the constraint set $\mathcal{C}$. The term $t$ is only being read.

Regarding the type $T$, it can also contain type variables not mentioned in $\mathcal{X}$. For example, try typing the term $(\lambda f: A \to A. f\,0)$. When you reach rule CT-Var, the type $T$ in the conclusion of the rule will be $A\to A$, where $A$ will not appear in $\mathcal{X}$.

Edit 1

I still don't fully understand the question. What do you mean by "standalone" derivations? Anyway, there is something I'd like to add:

e.g. I can apply CT-App to two subderivations for which 𝐶₂ contains type variables in χ₁.

First, note that the typing rules are such that every new unification variable is recorded in $\mathcal{X}$.

Now, indeed rule CT-App loses some information. In particular, the derivation for $t_1$ does not keep track of the fresh unification variables introduced in the derivation for $t_2$, and vice versa. So, it could happen that $\mathcal{C}_2$ contains unification variables that are mentioned in $\mathcal{X}_1$.

However, any unification variable in $\mathcal{C}_2$ is recorded in $\mathcal{X}_2$. Thus, if $\mathcal{C}_2$ contains unification variables mentioned in $\mathcal{X}_1$, then $\mathcal{X}_1\cap \mathcal{X}_2 \neq \emptyset$. Because of this, applying CT-App on the two subderivations will fail in this problematic scenario, since the rule requires that $\mathcal{X}_1\cap \mathcal{X}_2 = \emptyset$.

This does not mean that the term application $t_1\, t_2$ is not typable. Instead, this condition forces you to rename your unification variables accordingly, so that overlaps between the names of variables contained in $\mathcal{X}_1$ and $\mathcal{X}_2$ do not occur.

To sum up, two variables that have the same name and belong to both $\mathcal{X}_1$ and $\mathcal{X}_2$ should not be considered as the same variable. Instead, they should be considered as distinct variables that "coincidentally" were given the same identifier. Thus, an appropriate renaming solves the problem and rule CT-App can be applied.

Maybe now I do understand the question:

if there are any implicit meta-constraints that disallow "standalone" type derivations from containing free type variables.

First, let's clarify that all type variables appear free, because the language has no type abstraction in its syntax. There are no $\Lambda$ or $\forall$ binders as those in System F. Now, every type variable $P$ that appears in $\Gamma$, $T$ or $\mathcal{C}$ has one and only one of the following two origins: either a) $P$ originates from the term $t$ (in the type of a $\lambda$-binder), and thus was given by the programmer, or b) $P$ is a freshly generated type variable. The set $\mathcal{X}$ keeps track of these type variables.

So given that we start our typing process with an empty $\Gamma$, all type variables that appear in a derivation are free and necessarily have one of these two origins. There can be no type variables of some other origin and this is not an implicit constraint. It is enforced by the typing rules. You can try proving the following:

$\text{If }\Gamma\vdash t: T\mid_{\mathcal{X}} \mathcal{C}\text{, then }\forall P,\,P\in\mathsf{FT}(T)\cup\mathsf{FT}(\mathcal{C})\implies P\in\mathcal{X}\cup\mathsf{FT}(\Gamma)\cup\mathsf{FT}(t).$

This statement also takes into account the case where we start the typing process with a non-empty $\Gamma$. I believe the proof can work by induction on the typing judgment.

Wow, I wrote a lot! :D

Edit 2

Yes, your example is well-typed. In the application of rule CT-App, type $T_1$ (from the rule in the figure) is actually $(X\to X)\to \mathbb{N}$ and type $T_2$ is $X\to X$. This rule generates a fresh variable. The name of this variable should be distinct from those that appear in $\mathcal{X}_1$, $\mathcal{X}_2$, $T_1$, $T_2$, ... (3rd line of the rule's premises). So, because $X$ already appears in $T_1$, we should come up with another name. Say, Y. The conclusion of the rule will be:

$$ \emptyset \vdash t_1\,t_2 : Y \mid_{\{Y\}} \{(X\to X)\to\mathbb{N} = (X\to X)\to Y\}$$

where $t_1 = (\lambda x : X\to X. 0)$ and $t_2 = (\lambda x : X. x)$. The rest of the derivation is more straight-forward to build.

$\endgroup$
6
  • $\begingroup$ Thanks! I hindsight, I should've clarified something: I understand that it's technically possible to have free type variables in the terms—I'm mostly just wondering if there's an implicit "a standalone typing derivation should contain no free type variables" constraint. I've just edited my original question as such, and my apologies for not being clearer originally. $\endgroup$ – BalinKingOfMoria Reinstate CMs Jun 7 at 22:26
  • $\begingroup$ Either way, I've upvoted (and will accept after enough time), since you do give an excellent answer to my question as written :-) $\endgroup$ – BalinKingOfMoria Reinstate CMs Jun 7 at 22:32
  • 1
    $\begingroup$ This makes sense. I've thought about it more, and I think my real question this whole time has been: When "P originates from the term t (in the type of a 𝜆-binder)," does it still make sense to apply the constraint-typing rules even though we don't have polymorphism yet at this point in TAPL? (I'm an undergrad learning this for the first time, hence the scatteredness of my thoughts—your patience is much appreciated.) $\endgroup$ – BalinKingOfMoria Reinstate CMs Jun 8 at 19:11
  • 1
    $\begingroup$ @BalinKingOfMoriaReinstateCMs I think that this section is not to be regarded in isolation. Later on, in section 22.6, it explains that this constraint typing system can be used to support a language that has no type annotations at all (also discussed in the 2nd half of 22.2). So, for your example, the expression by the programmer would be $(\lambda x. 0)\,(\lambda x.x)$ and the parser would annotate it as $(\lambda x:A. 0)\,(\lambda x : B.x)$ and feed it to the constraint-type-checker. $\endgroup$ – frabala Jun 8 at 20:31
  • 1
    $\begingroup$ So, I'd say in the end you get a kind of polymorphism similar to that of the untyped calculus. Only, recursion is not supported, but according to the book the system can be extended with a rule for a built-in fix-operator. Happy to help! :) $\endgroup$ – frabala Jun 8 at 20:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.