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

Subtyping with if

The discusssion raised from the message "subject reduction fails
in Java" of Benjamin et al. reveals a rather challenging problem:
subtyping with if-expression.

The situation is that, nobody knows how to derive minimal types
for terms without the assumption of the existence of least upper
bound for types, so no type checking algorithm is complete. One
of the consequence, as pointed out in the message of Bruce
(originally discovered by Wadler (and/or)Odersky) is that, Java
does not fully support subtyping.

Attracted by this problem, I make a formal study in a simply typed
lambda calculus extended by subtyping and if-expression (rules 
are at the end of this mail). It enjoys subject reduction. But
type checking is challenging. However, I have managed to construct
a type checking algorithm, which seems sound and complete. It does
not assume the existence of least upper bound for types. No 
runtime type casting is needed.


The algorithm does not derive the minimal types for terms. It only
checks M : A. Here I explain the idea. First, to check
(b?e1:e2) : A, we need only to check that b : Bool,  e1 : A
and  e2 : A. But, to check  MN : A, we need to find B such that
M : B -> A and  N : B. The traditional method solves this problem
by deriving the minimal type for M. Thus  it  fails for type 
checking  if-expression. We propose to derive  B  from both 
M  and  A. Due to subtyping, there may be more than one such  B  
and we would like to derive a B which satisfies a minimal condition:

 B  = min{ C  |  M : C -> A }

Such condition will ensure that the algorithm is complete.

>From this analysis, we propose a new judgment:

    M  |A| : B

Its meaning is that, there exists n >= 0, and  B1,...,Bn  such that

 B = min { B1 -> ... -> Bn -> A  |   M :  B1 -> ... -> Bn -> A  }

We present a set of algorithmic type checking rules to derive the
judgement M  |A| : B. Note that the normal typing is a
special case of such judgement: M : A <=> M |A| : A.

Here is the main part of the type checking algorithm,


----------      ----------
tt : Bool       ff : 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| : C   B' < B
--------------------------
[x:B]M |B'->A| : B'->C

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

Main results are stated without proofs as follows:

1. M |A| : B <=> there exists n>=0, B1, .. Bn such that
  B = min{B1 -> ... -> Bn -> A | M : B1 -> ... -> Bn -> A}
2. M : A <=> M |A| : A
3. Given M,A, it is decidable that if there exists B
such that M |A| : B

More details can be found in my draft "Subtyping with if-expression"
from http://www.dmi.ens.fr/~gang/subif.dvi.gz.

Comments, critiques, improvements and corrections are all welcome.

Cheers.

Gang Chen


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


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


Subtyping rules:

A < B \in \Gamma      C<A  B<D     A<B  B<C
----------------    -----------    --------
    A < B           A->B < C->D      A<C

Reductions:

([x:A]M)N  -> M[x:=N]
(tt?M:N)   -> M
(ff?M:N)   -> N