# A non-typable if-expression

• To: types <types@cs.indiana.edu>
• Subject: A non-typable if-expression
• From: Gang CHEN <Chen.Gang@ens.fr>
• Date: Wed, 01 Jul 1998 18:40:34 +0200
• Delivery-Date: Wed, 01 Jul 1998 11:49:52 -0500

```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
```