4
$\begingroup$

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

$\endgroup$
3
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Yes, you are right. It is about subtypes, not about Dependent types. $\endgroup$ – alim Aug 28 '17 at 10:02
  • 1
    $\begingroup$ And also answer the question. It should be the accepted answer for future people with the same doubts $\endgroup$ – hfehrmann Aug 28 '17 at 18:51
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – alim Jun 27 '16 at 5:26

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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