Cheap and Secure Web Hosting Provider : See Now

# [Solved]: how type checking fails?

, ,
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.

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

``       ctx[]|t:T ``

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

:)