[Prev][Next][Index][Thread]

A non-typable if-expression

Dear All,

To my surprise, some intuitively well-formed terms containing
if-expressions may not be typable in  apparently reasonable 
systems with subtyping. Here, I give an example. 

First, an "apparently reasonable system" is defined as the simply 
typed lambda calculus extended with subtyping, subsumption rule,
and a rule for typing if-expression:

 M : A    A < B         b : Bool  M : A  N : A
----------------       ------------------------
     M : B                   (b?M:N) : A

Second, I give an "intuitively well-formed term containing 
if-expression". Assume a set of base types A,B,C,D,E and a set
of predefined subtyping relation:
  C < A, D < A, C < B, D < B
Note that C,D have two common upper bounds A,B, but do not have
least common upper bound. 

Assume b1,b2 : Bool, e1 : A->E, e2 : B->E, a1 : C, a2 : D
Then the follwing  term is not typable 

     (b1?e1:e2) (b2?a1:a2)  

(b2?a1:a2) has two types: A,B, (b1?e1:e2) has two types
C->E, D->E, which are the only common upper bounds of A->E and B->E.  
Neither A nor B is a subtype of C or D. 

The following term is computationally equivalent to the previous one,
it is typable as

   (b1? (e1 (b2?a1:a2)) : (e1 (b2?a1:a2))) : E
  

My Proposal to this problem:

I suggest to replace the above typing rule for if-expression by the
following:

b : Bool   e1 N1 .. Nk : A     e2 N1 .. Nk : A
-----------------------------------------------       (*)
           (b?e1:e2)N1..Nk : A

It is motivated by the equality:  (b?e1:e2)N = (b?(e1 N):(e2 N)) .

Also, the application rule:

M : A->B     N : A
-------------------
   M N : B

needs to be modified:

M : A->B     N : A    M \= (b?e1:e2)N1..Nk
-------------------------------------------
                M N : B

For such typing system, I discover a type checking algorithm, which 
consists of the rule (*) and the following:

x : B1-> .. Bn->A' in \Gamma   |- A' < A   Ni : Bi  i=1..n
-----------------------------------------------------------
            |- x N1 .. Nn : A

x : B |- M N2 .. Nn : A    |- N1 : B
---------------------------------------
  ([x:B].M) N1 .. Nn : A

x : B |- M : A   B' < B
------------------------
  [x:B].M : B' -> A

In fact, I started with the "apparently reasonable system" and 
constructed the above algorithm. When proving its soundness, I 
discovered the above problem. 

A few more remark. The above algorithm works for functional 
language. In most imperative language, the if-expression will
not return a function. Things can be simpler. In my message
"subtyping with if-expression" to Types, I showed an algorithm
for type checking the minimal calculus with subtyping and 
if-expression. Later I found that it is not complete. Actually,
it only fails to check those if-expressions which returns functions.
Therefore, it still works for imperative languages, and may be 
better than the algorithm just proposed. I include the revised 
version of that algorithm at the end of this mail.

Cheers

Gang Chen

================================================
A type checking algorithm for imperative language
with subtyping and if-expression

The judgement M |A| : B1->...->Bn->A denotes that
B1, ..., Bn can be derived from term M and type A, and
 B1->...->Bn->A is the minimal type such that
     M : C1->...->Cn->A

algorithmic type checking rules:

----------------       ----------------
tt |Bool| : Bool       ff |Bool| : Bool

x : B1 -> ... -> Bn -> A' in \Gamma    A'  <  A
-------------------------------------------------
      x  | A| : B1 -> ... -> Bn -> A

M |A| : B->C   N |B| : B
-------------------------
    MN |A| : C

 x : B |- M |A| : C
--------------------
 [x:B]M |A| : B->C

x : B  |- M |A| : A   B' < B
----------------------------
  [x:B]M |B'->A| : B'->A

b |Bool| : Bool   e1 |A| : A   e2 |A| : A
-----------------------------------------
        (b?e1:e2) |A| : A

Typing  rules.
                              b : Bool  e1 : A  e2 : A
----------      ----------    -----------------------
tt : Bool       ff : Bool         (b?e1:e2) : A


x : A in \Gamma
---------------
    x : A

x : A |- M : B     M : A->B  N : A   M : A  A < B
----------------   ---------------   ------------
 [x:A]M : A->B         M N : B          M : B