# How to understand these exposure algorithm rules for System F sub?

The book "Types and Programming Languages" said System F sub type checking introduce exposure typing rules alongside algorithmic typing and sub-typing rules.

       exposure algorithm

X<:T ∈ Γ        Γ |- T ⇑ T'
--------------------------- (XA-PROMOTE)
Γ |- X ⇑ T'

T is not a type variable
--------------------------- (XA-other)
Γ |- T ⇑ T


The first one seems simple, but the second rule seems bit wrong to me. "T is not a type variable", which "T" it is referring to?

Does "Γ |- T ⇑ T" mean left and right hand side of "⇑" are same types?

For example, with the type checking

          " Γ |- sone: SPos"


where

          sone= λ A <: Top.
λ B <: A.
λ C <: A.
λ m : A->B.
λ n : C. m n.

and

SPos= All A <: Top. All B<: A. All C<: A. (A-> B) -> (C-> A).


After applying "TA_TABS" and "TA_ABS" rules

 {A <: Top, B<: A, C<: A, m : A->B, n : C } |- m n :B
-----------------------------------------------------------TA-APP
{...} |- :- m:T1   ,  {...}|-T1 ⇑ (T11->B)  ,  {...}|-n:T2  , {...}|-T2<:T11

{...}|-n:T2    we know  T2=C
then
{...}|-C<:T11  we get T11=top

then put it in place

{...} |- :- m:T1   , {...}|-T1 ⇑ (top->B)
------------------------------------------

which rule applies now?

I believe from

{...}|-T1 ⇑ (top->B)

we should get "T1=A->B" , but how?

both (XA-PROMOTE) and (XA-other) seems cannot be applied.



In a typing rule (and more generally any deduction rule), all metavariables¹ are universally quantified. That is, the rule can be applied for any instantiation that is syntactically correct. For example, (XA-PROMOTE) means “for any context $\Gamma$, for any type variable $X$, for any type $T$, for any type $T'$, if $\Gamma$ contains $X <: T$ and the typing judgement $\Gamma \vdash T \Uparrow T'$ is true, then the typing judgement $\Gamma \vdash X \Uparrow T'$ is true”. The rule (XA-other) states “for any type $T$, for any context $\Gamma$, if $T$ is not a type variable then the typing judgement $T \vdash T \Uparrow T$ is true”.

The question “which $T$ is it referring to?” is not meaningful: the rule does not refer to a particular $T$. On the contrary, the rule applies to any $T$; the conclusion applies to any $T$ that matches the premise.

In $\Gamma \vdash T \Uparrow T$, the left- and right-hand sides of $\Uparrow$ are the same type. The rule states that the relation $\Uparrow$ in any given context $\Gamma$ is symmetric on the subset of the set of all types that consists of the types that are not type variables. Some examples of typing judgements that can be derived by this rule are: $$\vdash \mathsf{Top} \Uparrow \mathsf{Top} \\ X <: \mathsf{Top}, Y <: X \vdash X \rightarrow \mathsf{Top} \Uparrow X \rightarrow \mathsf{Top} \\ X <: \mathsf{Top}, Y <: X \vdash (\forall Z <: Y, X \rightarrow Z) \Uparrow (\forall Z <: Y, X \rightarrow Z) \\$$

I don't remember Pierce's presentation and I don't have the book here, but I think the reason XA-other has the premise that $T$ must not be a type variable is to make these rules syntax-directed: there's another rule that allows deriving judgement $\Gamma \vdash T \uparrow T$ when $T$ is a type variable. This is a presentation choice.

¹ A metavariable is a variable that is used to describe the system, for example $X$, $T$, $T'$ and $\Gamma$ in the rule (XA-PROMOTE). We use the term metavariable to distinguish this concept from a variable, which refers whatever the language calls a variable.

• Thanks for your answer. I made clear my question with a simple example, Could you please look at and explain to me.
– alim
Oct 6 '16 at 5:09