Cheap and Secure Web Hosting Provider : See Now

[Solved]: how type checking fails?

, , No Comments
Problem Detail: 

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)             :(∀B1<:A.∀C1<:A.(A-->B1)-->C1-->C1)    ----------------------------------------------(T-TABS) =>assume B=B1, rename B1 to B  A<:top,B<:A |- (λC<:A.λx:(A-->B).λy:C.x y)               :(∀C1<:A.(A-->B)-->C1-->C1)  ---------------------------------------------------(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.

Asked By : alim

Answered By : alim

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

         ctx[]|- t:S     ctx[]|S<:T          ---------------------------t-sub                ctx[]|-t: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".


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