I was doing a type checking example in system f sub on paper to understand how it works.

according to Pierce's book Types and Programming Languages, numbers and their types are following in system f sub. (see chapter 26.3, page 399)

   1)top is universal type, 
   2)capital letters are type variables, small letters are term variables  

    church number 1
    sone = λA<:top.λB<:A.λC<:A.λx:(A-->B).λy:C.x y
    stwo = λA<:top.λB<:A.λC<:A.λx:(A-->B).λy:C.x (x y)

    type for church number 0
    SZero = ∀A<:top.∀B<:A.∀C<:A.(A-->B)-->C-->C

    type for numbers except 0
    SPos = ∀A<:top.∀B<:A.∀C<:A.(A-->B)-->C-->B
    SNat = ∀A<:top.∀B<:A.∀C<:A.(A-->B)-->C-->A

for the type checking

   Γ |-  stwo :  SZero  

should fail.

book said "SPos is inhabited by all the elements of SNat except SZero".
Also I saw there is a input test test files, it shows above example should fail.

Therefore, I assume

 Γ |-  sone :  SZero  

should fail too.

I want to see how it is going to fail and did pen-paper type checking as following (see type checking rules in the same book, previous page)

  1)for convenience, I wrote from top to down fashion
  2)variables are given distinct

   Γ |-  (λA<:top.λB<:A.λC<:A.λx:(A-->B).λy:C.x y)  
       : (∀A1<:top.∀B1<:A1.∀C1<:A1.(A1-->B1)-->C1-->C1)
   ---------------------------------------------(T-TABS) =>assume A=A1,top=top
                                                             ,and renamed A1 to A 
  A<:top |- (λB<:A.λC<:A.λx:(A-->B).λy:C.x y) 
  ----------------------------------------------(T-TABS) =>assume B=B1, rename B1 to B

A<:top,B<:A |- (λC<:A.λx:(A-->B).λy:C.x y)
 ---------------------------------------------------(T-TABS) =>assume C=C1, rename C1 to C
 A<:top,B<:A,C<:A |- (λx:(A-->B).λy:C.x y)
                   : (A-->B)-->C-->C
 -----------------------------------------------------T_ABS =>have A-->B=A-->B,   get A=A,B=B,remove them

 A<:top,B<:A,C<:A,x:A-->B |- (λy:C.x y) : C-->C 
 ------------------------------------------------T-ABS ==>have  C=C
 A<:top,B<:A,C<:A,x:A-->B,y:C | ( x y ) : C         
 ----------------------------------------------- T-APP  introduce type variable T1
 A<:top,B<:A,C<:A,x:A-->B,y:C | x : T1-->C  A:top,B<:A,C<:A,x:A-->B,y:C | y:T1     
 ----------------------------------------  ----------------------------------
   have X:T1-->C                                   have y:T1
        X:A-->B                                         y:C
    so, T1=/=A, B=/=C                                   T1=/=C

so fails I assume.

I thought the type checking

  Γ |-  sone :  SPos 

should be successful, but it ..

 1) type is different a bit here

   Γ |-  (λA<:top.λB<:A.λC<:A.λx:(A-->B).λy:C.x y)  
       : (∀A1<:top.∀B1<:A1.∀C1<:A1.(A1-->B1)-->C1-->B1)

        intermediate steps are all same 
  A<:top,B<:A,C<:A,x:A-->B |- (λy:C.x y) : C-->B 
 ------------------------------------------------T-ABS ==>have  C=C
 A<:top,B<:A,C<:A,x:A-->B,y:C | ( x y ) : B         
 ----------------------------------------------- T-APP  introduce type variable T1
 A<:top,B<:A,C<:A,x:A-->B,y:C | x : T1-->B  A:top,B<:A,C<:A,x:A-->B,y:C | y:T1     
 ----------------------------------------  ----------------------------------
   have X:T1-->B                                   have y:T1
        X:A-->B                                         y:C
    so, T1=/=A, B=B                                   T1=/=C

See, these two type checking ended up pretty same, I did not understand why the first type checking should fail, while second one should be successful.

How to do type checking in system F sub? If you know, please correct me, thank you.

  • 1
    $\begingroup$ Cross-post? $\endgroup$ Commented Sep 30, 2016 at 11:58
  • $\begingroup$ @AntonTrunov. not sure where it will get attention. I delete one of them once another is answered. $\endgroup$
    – alim
    Commented Sep 30, 2016 at 13:58
  • $\begingroup$ I think this is the right place. A tip: you can use MathJax to typeset formulas on this site. $\endgroup$ Commented Sep 30, 2016 at 14:00
  • 1
    $\begingroup$ Cross-posted on CS.SE and SO: cs.stackexchange.com/q/64075/755, stackoverflow.com/q/39769680/781723. Please do not post the same question on multiple sites. Each community should have an honest shot at answering without anybody's time being wasted. $\endgroup$
    – D.W.
    Commented Sep 30, 2016 at 16:13
  • $\begingroup$ @D.W. another one is deleted. $\endgroup$
    – alim
    Commented Oct 1, 2016 at 5:42

1 Answer 1


I finally figured it out. The key is using sub-typing rules.

         ctx[]|- t:S     ctx[]|S<:T

By applying this rule after T-APP rules, you can eliminate all "A==B" equations by using

       eq(A,A) -> .
       eq(A-->B,A-->B) -> eq(A,A),eq(B,B).

One can easily observe how to write these rules to eliminate "eq"s. If there is one or some "eq"s left, such as "eq(A,B)", means a contradiction, so type checking fails.

If you can eliminate all "eq"s, means type checking successful.

One important point about "t-sub" rule is that it is not suitable for implementation, because it is not syntax directed. That rule is applicable for any statement with the form of


therefore, algorithmic version is proved to has the same power in the book "Types and Programming Languages".



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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