3
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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

:)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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