[Prev][Next][Index][Thread]
Subtyping with if

To: types@cs.indiana.edu

Subject: Subtyping with if

From: Gang CHEN <Chen.Gang@ens.fr>

Date: Tue, 23 Jun 1998 11:40:35 +0200

DeliveryDate: Tue, 23 Jun 1998 04:57:36 0500

References: <4022.898574038@cslinux1.cs.indiana.edu>
The discusssion raised from the message "subject reduction fails
in Java" of Benjamin et al. reveals a rather challenging problem:
subtyping with ifexpression.
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 ifexpression (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 ifexpression. 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 ifexpression"
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