# how type checking fails?

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.

• – Anton Trunov Sep 30 '16 at 11:58
• @AntonTrunov. not sure where it will get attention. I delete one of them once another is answered. – alim Sep 30 '16 at 13:58
• I think this is the right place. A tip: you can use MathJax to typeset formulas on this site. – Anton Trunov Sep 30 '16 at 14:00
• 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. – D.W. Sep 30 '16 at 16:13
• @D.W. another one is deleted. – alim Oct 1 '16 at 5:42

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

:)