# System f-sub, how to do type checking?

I was reading that system f-sub (polymorphic lambda calculus with sub-typing) and I was quite confused with its one checking rule called "T-TAPP".

This rule as following (ctx denotes the typing context)

   ctx |- t1 : ∀X<:T11. T12    ,    ctx |- T2<:T11
-----------------------------------------------
ctx |- t1 [T2] : [X-->T2]T12


I could not understand how '[x-->T2]T12' will be used (I know it is substitution). This rule appears on page 10 in the following source. I am looking for two type checking examples, in which above inference rule will be applied and at least one example is a case of type checking failure.

Could anyone provide me with concrete examples?
Description of system F-sub

• "J.B.Wells, Typability and type checking in System F are equivalent and undecidable" Commented Nov 15, 2022 at 3:34

I know this is old but the previous answer has a huge misconception.

The following function is in System F.

$f = \lambda X. X \rightarrow X \rightarrow X$

All we know of this function is it selects one of its arguments and can be instantieded with any type; $\ f$ [Bool] : Bool $\rightarrow$ Bool $\rightarrow$ Bool.

In System $F_{<:}$ is possible to have the following function.

$f' = \lambda X<:$Number$.\ X \rightarrow X \rightarrow X$

This function can be the addition, multiplication, division, subtraction, etc, and can be instantiated with subtypes of Number.

$f'$ [Int], $\ f'$ [Double], $\ f'$ [Real] are valid instantiations, but $\ f'$ [Bool] not, because Bool is not a subtype of Nat.

Dependent types are a different thing. It has nothing to do here and is out of the scope of the question, but it is a very interesting topic. See Lambda Cube

• Yes, you are right. It is about subtypes, not about Dependent types.
– alim
Commented Aug 28, 2017 at 10:02
• And also answer the question. It should be the accepted answer for future people with the same doubts Commented Aug 28, 2017 at 18:51

It would've helped if you mentioned what page that rule appears in.

Anyhow, from what I can tell here's an example.

⊢ t₁ : ∀ X <: Animal. “X makes noise”            ⊢ Cat <: Animal
------------------------------------------------------------
⊢  t₁ [Cat] : “Cat makes noise”


The idea seems to be that t₁ is to be treated as a generic function, or a dependently-typed function, in that for each Animal subtype X, in our example, it gives us a proof t₁[X] and the rule just formalises this idea.

Hope that helps.

• I was expecting a type checking example in this system, such as to prove "ctx |- t : T". so rules applies from bottom-up fashion. I could not figure out how to apply that rule in such cases.
– alim
Commented Jun 27, 2016 at 5:26