**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

` ctx[]|t:T `

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

:)

###### Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/64075

**3.2K people like this**

## 0 comments:

## Post a Comment

Let us know your responses and feedback