[Prev][Next][Index][Thread]
A nontypable ifexpression

To: types <types@cs.indiana.edu>

Subject: A nontypable ifexpression

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

Date: Wed, 01 Jul 1998 18:40:34 +0200

DeliveryDate: Wed, 01 Jul 1998 11:49:52 0500
Dear All,
To my surprise, some intuitively wellformed terms containing
ifexpressions 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 ifexpression:
M : A A < B b : Bool M : A N : A
 
M : B (b?M:N) : A
Second, I give an "intuitively wellformed term containing
ifexpression". 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 ifexpression 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 ifexpression will
not return a function. Things can be simpler. In my message
"subtyping with ifexpression" to Types, I showed an algorithm
for type checking the minimal calculus with subtyping and
ifexpression. Later I found that it is not complete. Actually,
it only fails to check those ifexpressions 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 ifexpression
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