Cheap and Secure Web Hosting Provider : See Now

[Answers] System f-sub, how to do type checking?

, , No Comments
Problem Detail: 

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

Asked By : alim

Answered By : Musa Al-hassy

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.

Best Answer from StackOverflow

Question Source :

3.2K people like this

 Download Related Notes/Documents


Post a Comment

Let us know your responses and feedback