From types-errors@cs.indiana.edu Fri Jun 19 01:09:56 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil t nil nil] [nil "Thu" "18" "June" "1998" "15:01:25" "-0500" "Benjamin Pierce" "pierce@cs.indiana.edu" nil "131" "Subject reduction fails in Java" "^From:" nil nil "6" "1998061820:01:25" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id BAA15577; Fri, 19 Jun 1998 01:09:54 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id WAA08337 for ; Thu, 18 Jun 1998 22:46:55 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id WAA13455 for ; Thu, 18 Jun 1998 22:46:54 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id WAA08328 for types-distrib@cs.indiana.edu; Thu, 18 Jun 1998 22:46:53 -0500 (EST) Message-Id: <199806190346.WAA08328@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Thu, 18 Jun 1998 15:01:29 -0500 Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id PAA22162; Thu, 18 Jun 1998 15:01:28 -0500 (EST) Received: from localhost (pierce@localhost [127.0.0.1]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id PAA05837; Thu, 18 Jun 1998 15:01:26 -0500 (EST) Reply-to: pierce@cs.indiana.edu Errors-To: types-errors@cs.indiana.edu From: Benjamin Pierce To: types@cs.indiana.edu Cc: hahosoya@cs.indiana.edu, David Turner Subject: Subject reduction fails in Java Date: Thu, 18 Jun 1998 15:01:25 -0500 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] We were recently surprised to discover that Java fails to possess a straightforward analogue of the familiar SUBJECT REDUCTION property of typed lambda-calculi. This note sketches a counterexample and briefly discusses its significance. Regards, Haruo Hosoya Benjamin Pierce David Turner "SUBJECT REDUCTION" IN JAVA --------------------------- Given a definition R m (T1 x1, ..., Tn xn) { return r; } of a method m with parameters x1...xn of types T1...Tn and result type R, we might expect to be able to rewrite a call to m of the form m(a1...an) by "inlining" the body r, replacing formal parameters by corresponding arguments: m(a1...an) --> r[a1/x1...an/xn] Unfortunately, this inlining operation does not, in general, preserve typing. That is, it may be that both the definition and the use of m are well typed, but that the "contractum" r[a1/x1...an/xn] is not. COUNTEREXAMPLE -------------- The culprit here is the innocent-looking conditional expression b ? e1 : e2 which yields e1 if the boolean expression b is true and e2 if b is false. The typing rule for such expressions given in the Java Specification (page 367-368) says: 1) the guard b must have type boolean 2) if the bodies e1 and e2 have reference types E1 and E2, then either 2a) E1 and E2 must be identical, or 2b) one of E1 and E2 must be a subtype of the other. 3) similar conditions when E1 and E2 are numeric types or the special null type. Now, suppose that the method m above is defined as follows: Object m (Object a1, Object a2) { return (b ? a1 : a2); } That is, it takes parameters a1 and a2 of type Object and returns (b ? a1 : a2), where b is some boolean expression. The body (b ? a1 : a2) is well typed, using rules 1 and 2a above. Next, consider the following program fragment: Integer i = new Integer(); HashTable h = new HashTable(); Object o = m (i, h); Again, this code is well typed. But if we "beta-reduce" the call to m, we obtain Integer i = new Integer(); HashTable h = new HashTable(); Object o = (b ? i : h); which is *not* well typed: the branches of the conditional now have the *different* reference types Integer and Hashtable, neither of which is a subtype of the other. DISCUSSION ---------- One may wonder how this failure of subject reduction squares with recent proofs of type soundness for fragments of Java by Drossopolou and Eisenbach [2] and Nipkow and XXXXXXXXXXXXXX [3]. On the one hand, since these fragments omit the conditional expression form, this failure does not affect the validity of their results, per se. On the other hand, both of these papers use a reduction-based operational semantics, and therefore, it seems, their proof methods cannot easily be extended to deal with the full Java language including conditional expressions. Of course, it remains intuitively clear that the typing rule for conditional expressions *is* sound, in the sense that it cannot lead to unchecked failures at run time. One possible way of formalizing this intuition is to alter the beta-reduction rule so that, in the example above, the expression Integer i = new Integer(); HashTable h = new HashTable(); Object o = m (i, h); is rewritten as Integer i = new Integer(); HashTable h = new HashTable(); Object o = (b ? (Object)i : (Object)h); carrying the parameter types along explicitly during the substitution operation and thus maintaining the well-typedness of the conditional expression. CITATIONS --------- [1] Gosling, Joy, and Steele, The Java Language Specification, Addison Wesley, 1996. [2] Drossopolou and Eisenbach, "Java is type safe -- probably," ECOOP '97. [3] Nipkow and von Oheimb, "Java_light is type-safe -- definitely," POPL '98. From types-errors@cs.indiana.edu Fri Jun 19 15:52:53 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Fri" "19" "June" "1998" "10:27:41" "+0100" "Christian Horn" "chorn@lionet-technologies.com" nil "13" "Typing in Java" "^From:" nil nil "6" "1998061909:27:41" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id PAA18045; Fri, 19 Jun 1998 15:52:52 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA12630 for ; Fri, 19 Jun 1998 12:57:46 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA21314 for ; Fri, 19 Jun 1998 12:57:46 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id MAA12619 for types-distrib@cs.indiana.edu; Fri, 19 Jun 1998 12:57:44 -0500 (EST) Message-Id: <199806191757.MAA12619@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Fri, 19 Jun 1998 04:31:53 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id EAA08288 for ; Fri, 19 Jun 1998 04:31:51 -0500 (EST) Received: from mail.webstream.net (mail.webstream.net [209.203.197.7]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id EAA26394 for ; Fri, 19 Jun 1998 04:31:49 -0500 (EST) Received: from clara ([194.125.148.191]) by mail.webstream.net (Post.Office MTA v3.1 release PO205e ID# 0-39863U2500L250S0) with SMTP id AAA192; Fri, 19 Jun 1998 05:33:11 -0400 Reply-To: chorn@lionet-technologies.com Organization: Lionet Technologies X-Mailer: Mozilla 3.01 (WinNT; I) MIME-Version: 1.0 References: <358A22B5.B786E893@cs.tcd.ie> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Errors-To: types-errors@cs.indiana.edu From: chorn@lionet-technologies.com (Christian Horn) To: Simon Dobson CC: fmg@cs.tcd.ie, Distributed Systems Group , types@cs.indiana.edu Subject: Typing in Java Date: Fri, 19 Jun 1998 10:27:41 +0100 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] The problem mentioned has nothing todo with the conditional expression and not with Java, but with the way reduction for typed languages has to be formulated with casting of the actual parameter types to the formal parameter types. > > m(a1...an) --> r[((T1)a1)/x1...((Tn)an)/xn] > Christian Horn From types-errors@cs.indiana.edu Fri Jun 19 15:51:58 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Fri" "19" "June" "1998" "11:07:32" "+0100" "Zhaohui Luo" "Zhaohui.Luo@durham.ac.uk" nil "184" "Re: Subject reduction fails in Java" "^From:" nil nil "6" "1998061910:07:32" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id PAA18002; Fri, 19 Jun 1998 15:51:57 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA12577 for ; Fri, 19 Jun 1998 12:56:39 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA20777 for ; Fri, 19 Jun 1998 12:56:39 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id MAA12569 for types-distrib@cs.indiana.edu; Fri, 19 Jun 1998 12:56:38 -0500 (EST) Message-Id: <199806191756.MAA12569@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Fri, 19 Jun 1998 05:07:44 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.254.191]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id FAA10964; Fri, 19 Jun 1998 05:07:43 -0500 (EST) Received: from hermes.dur.ac.uk (hermes.dur.ac.uk [129.234.4.9]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id FAA27855; Fri, 19 Jun 1998 05:07:41 -0500 (EST) Received: from easby by hermes.dur.ac.uk id (8.8.8/ for dur.ac.uk) with SMTP; Fri, 19 Jun 1998 11:07:39 +0100 (BST) Received: from ws-zl.durham.cs by easby id ; Fri, 19 Jun 1998 11:07:37 +0100 Received: from localhost by ws-zl.durham.cs (SMI-8.6/SMI-SVR4) id LAA14496; Fri, 19 Jun 1998 11:07:36 +0100 In-Reply-To: <199806190346.WAA08328@shovelnose.cs.indiana.edu> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Errors-To: types-errors@cs.indiana.edu From: Zhaohui Luo To: types@cs.indiana.edu cc: hahosoya@cs.indiana.edu, David Turner , Zhaohui Luo , Benjamin Pierce Subject: Re: Subject reduction fails in Java Date: Fri, 19 Jun 1998 11:07:32 +0100 (BST) [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Dear Benjamin, The subject reduction problem with Java discussed in your message in the types-mailing list is very interesting. I believe that it is closely related to the notion of typed reduction we have been studying in our work on Coercive Subtyping (see, for example, my papers [1][2] for the description of the framework.) Java-conversions (the widening conversions) can be regarded as what we have called "coercions". In the framework of coercive subtyping, if f:K->K', a:K0, and K0 <_c K (ie, K is a subtype via coercion c), then f(a) is computationally equal to (reduces to) f(c(a)) In particular, ([x:K]b)(a) does not reduce to [a/x]b, but it reduces to ([x:K]b)(c(a)) (coercion insertion as reduction) which beta-reduces to [c(a)/x]b. In other words, reductions such as beta cannot be done directly when the argument's type is a proper subtype of the required type; instead, a coercion (or type-casting operation, or conversion in Java's term) has to be inserted (as a step of reduction) before the reduction (beta in the above example) can be done. I think this corresponds to the suggestion you have made in your DISCUSSION section of your message. I am very interested in this and hope to get your further opinions. Do you know of other related work that uses the similar ideas to deal with these situations? (Please let me know if so.) Best regards, Zhaohui. P.S. It is OK for this message to be sent to the types-list if you think it is appropriate. [1] Z. Luo. Coercive subtyping in type theory. Proc. of CSL'96, the 1996 Annual Conference of the European Association for Computer Science Logic, Utrecht. LNCS 1258, 1997. [Available from URL: http://www.dur.ac.uk/~dcs0zl/SUBTYPING96.ps.gz] [2] Z. Luo. Coercive subtyping. Submitted to Journal of Logic and Computation. 1997. To appear. [Draft available from URL: http://www.dur.ac.uk/~dcs0zl/JLC98.ps.gz] On Thu, 18 Jun 1998, Benjamin Pierce wrote: > [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] > > We were recently surprised to discover that Java fails to possess a > straightforward analogue of the familiar SUBJECT REDUCTION property of > typed lambda-calculi. This note sketches a counterexample and briefly > discusses its significance. > > Regards, > > Haruo Hosoya > Benjamin Pierce > David Turner > > > "SUBJECT REDUCTION" IN JAVA > --------------------------- > > Given a definition > > R m (T1 x1, ..., Tn xn) { > return r; > } > > of a method m with parameters x1...xn of types T1...Tn and result type > R, we might expect to be able to rewrite a call to m of the form > > m(a1...an) > > by "inlining" the body r, replacing formal parameters by corresponding > arguments: > > m(a1...an) --> r[a1/x1...an/xn] > > Unfortunately, this inlining operation does not, in general, preserve > typing. That is, it may be that both the definition and the use of m > are well typed, but that the "contractum" r[a1/x1...an/xn] is not. > > > COUNTEREXAMPLE > -------------- > > The culprit here is the innocent-looking conditional expression > > b ? e1 : e2 > > which yields e1 if the boolean expression b is true and e2 if b is > false. The typing rule for such expressions given in the Java > Specification (page 367-368) says: > 1) the guard b must have type boolean > 2) if the bodies e1 and e2 have reference types E1 and E2, then > either > 2a) E1 and E2 must be identical, or > 2b) one of E1 and E2 must be a subtype of the other. > 3) similar conditions when E1 and E2 are numeric types or the > special null type. > > > Now, suppose that the method m above is defined as follows: > > Object m (Object a1, Object a2) { > return (b ? a1 : a2); > } > > That is, it takes parameters a1 and a2 of type Object and returns > (b ? a1 : a2), where b is some boolean expression. The body (b ? a1 : a2) > is well typed, using rules 1 and 2a above. > > Next, consider the following program fragment: > > Integer i = new Integer(); > HashTable h = new HashTable(); > Object o = m (i, h); > > Again, this code is well typed. But if we "beta-reduce" the call to > m, we obtain > > Integer i = new Integer(); > HashTable h = new HashTable(); > Object o = (b ? i : h); > > which is *not* well typed: the branches of the conditional now have > the *different* reference types Integer and Hashtable, neither of > which is a subtype of the other. > > > DISCUSSION > ---------- > > One may wonder how this failure of subject reduction squares with > recent proofs of type soundness for fragments of Java by Drossopolou > and Eisenbach [2] and Nipkow and XXXXXXXXXXXXXX [3]. On the one hand, > since these fragments omit the conditional expression form, this > failure does not affect the validity of their results, per se. On the > other hand, both of these papers use a reduction-based operational > semantics, and therefore, it seems, their proof methods cannot easily > be extended to deal with the full Java language including conditional > expressions. > > Of course, it remains intuitively clear that the typing rule for > conditional expressions *is* sound, in the sense that it cannot lead > to unchecked failures at run time. One possible way of formalizing > this intuition is to alter the beta-reduction rule so that, in the > example above, the expression > > Integer i = new Integer(); > HashTable h = new HashTable(); > Object o = m (i, h); > > is rewritten as > > Integer i = new Integer(); > HashTable h = new HashTable(); > Object o = (b ? (Object)i : (Object)h); > > carrying the parameter types along explicitly during the substitution > operation and thus maintaining the well-typedness of the conditional > expression. > > > CITATIONS > --------- > > [1] Gosling, Joy, and Steele, The Java Language Specification, Addison > Wesley, 1996. > > [2] Drossopolou and Eisenbach, "Java is type safe -- probably," ECOOP > '97. > > [3] Nipkow and von Oheimb, "Java_light is type-safe -- definitely," > POPL '98. > > From types-errors@cs.indiana.edu Fri Jun 19 15:58:31 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Fri" "19" "June" "1998" "09:13:52" "-0400" "Philip Wadler" "wadler@research.bell-labs.com" nil "40" "Re: Subject reduction fails in Java " "^From:" nil nil "6" "1998061913:13:52" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id PAA18298; Fri, 19 Jun 1998 15:58:30 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA12588 for ; Fri, 19 Jun 1998 12:56:59 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA20937 for ; Fri, 19 Jun 1998 12:56:58 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id MAA12580 for types-distrib@cs.indiana.edu; Fri, 19 Jun 1998 12:56:58 -0500 (EST) Message-Id: <199806191756.MAA12580@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Fri, 19 Jun 1998 08:14:09 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id IAA21056 for ; Fri, 19 Jun 1998 08:14:08 -0500 (EST) Received: from dirty.research.bell-labs.com (dirty.research.bell-labs.com [204.178.16.6]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with SMTP id IAA03990 for ; Fri, 19 Jun 1998 08:14:04 -0500 (EST) Received: from research.research.bell-labs.com ([135.104.1.3]) by dirty; Fri Jun 19 09:13:57 EDT 1998 Received: from nslocum.cs.bell-labs.com ([135.104.8.38]) by research; Fri Jun 19 09:13:54 EDT 1998 Received: from nslocum.cs.bell-labs.com (localhost [127.0.0.1]) by nslocum.cs.bell-labs.com (8.8.8/8.8.8) with ESMTP id JAA24217; Fri, 19 Jun 1998 09:13:52 -0400 (EDT) In-reply-to: Your message of "Thu, 18 Jun 1998 15:01:25 CDT." <199806190346.WAA08328@shovelnose.cs.indiana.edu> Errors-To: types-errors@cs.indiana.edu From: Philip Wadler To: pierce@cs.indiana.edu, types@cs.indiana.edu Cc: hahosoya@cs.indiana.edu, David Turner Subject: Re: Subject reduction fails in Java Date: Fri, 19 Jun 1998 09:13:52 -0400 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Haruo, Benli, Dave, This is the least of your problems. Reduction, in the sense you define it, can easily change the meaning of a program, thanks to Java's notion of overloading. Original program prints "true". class Counterexample { static boolean overloaded (Object x) { return true; } static int overloaded (String s) { return 42; } static void m (Object x) { System.out.println(overloaded(x)); } public static void main (String[] args) { m("hello"); } } Reduced program prints "42". class Counterexample { static boolean overloaded (Object x) { return true; } static int overloaded (String s) { return 42; } static void m (Object x) { System.out.println(overloaded(x)); } public static void main (String[] args) { System.out.println(overloaded("hello")); } } Yours, -- P ----------------------------------------------------------------------- Philip Wadler wadler@research.bell-labs.com Bell Labs, Lucent Technologies http://www.cs.bell-labs.com/~wadler 600 Mountain Ave, room 2T-402 office: +1 908 582 4004 Murray Hill, NJ 07974-0636 fax: +1 908 582 5857 USA home: +1 908 626 9252 ----------------------------------------------------------------------- From johan@ccs.neu.edu Fri Jun 19 11:54:14 1998 Status: RO X-VM-v5-Data: ([nil nil nil t t nil nil nil nil] [nil "Fri" "19" "June" "1998" "11:53:57" "-0400" "Johan Ovlinger" "johan@ccs.neu.edu" "<199806191553.LAA08263@boron.ccs.neu.edu>" "26" "Re: [Fwd: Benjamin Pierce] Subject reduction fails in Java " "^From:" nil nil "6" "1998061915:53:57" nil nil nil nil] nil) Received: from boron.ccs.neu.edu (root@boron.ccs.neu.edu [129.10.116.167]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id LAA03998; Fri, 19 Jun 1998 11:53:58 -0400 (EDT) Received: from boron.ccs.neu.edu (johan@localhost [127.0.0.1]) by boron.ccs.neu.edu (8.8.4/8.8.6) with ESMTP id LAA08263; Fri, 19 Jun 1998 11:53:57 -0400 (EDT) Message-Id: <199806191553.LAA08263@boron.ccs.neu.edu> In-reply-to: Your message of "Fri, 19 Jun 1998 10:44:23 EDT." <13706.31047.825966.809430@delphi.ccs.neu.edu> From: Johan Ovlinger To: Mitchell Wand cc: dem@ccs.neu.edu, pl-seminar@ccs.neu.edu Subject: Re: [Fwd: Benjamin Pierce] Subject reduction fails in Java Date: Fri, 19 Jun 1998 11:53:57 -0400 Well, their beta reduction fails because it is incorrect. Their proposed fix is to use the correct beta reduction. Let me expand: If you want to model java's method application sematics, you have to do so in a way that corresponds to the language definition. By just inlining the body of the function w/o the widening casts that are _mandated_ by the language definition, they are performing a program transformation that is incorrect. I quote from the Java langauge specification (http://java.sun.com/docs/books/jls/html/5.doc.html#12687) 5.3 Method Invocation Conversion Method invocation conversion is applied to each argument value in a method or constructor invocation ('15.8, '15.11): the type of the argument expression must be converted to the type of the corresponding ^^^^ parameter. Method invocation contexts allow the use of an identity conversion ('5.1.1), a widening primitive conversion ('5.1.2), or a widening reference conversion ('5.1.4). A widening reference conversion is: (Object) anInt; Johan From wand@ccs.neu.edu Fri Jun 19 12:03:50 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Fri" "19" "June" "1998" "12:03:44" "-0400" "Mitchell Wand" "wand@ccs.neu.edu" nil "38" "Re: [Fwd: Benjamin Pierce] Subject reduction fails in Java " "^From:" "johan@ccs.neu.edu, wand@ccs.neu.edu, dem@ccs.neu.edu, pl-seminar@ccs.neu.edu" "Johan Ovlinger, Mitchell Wand, dem@ccs.neu.edu, pl-seminar@ccs.neu.edu" "6" "1998061916:03:44" nil nil nil nil] nil) Received: from delphi.ccs.neu.edu (wand@delphi.ccs.neu.edu [129.10.116.177]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id MAA04513; Fri, 19 Jun 1998 12:03:45 -0400 (EDT) Received: (from wand@localhost) by delphi.ccs.neu.edu (8.8.6/8.8.6) id MAA14421; Fri, 19 Jun 1998 12:03:45 -0400 (EDT) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <13706.35808.568485.105264@delphi.ccs.neu.edu> In-Reply-To: <199806191553.LAA08263@boron.ccs.neu.edu> References: <13706.31047.825966.809430@delphi.ccs.neu.edu> <199806191553.LAA08263@boron.ccs.neu.edu> X-Mailer: VM 6.51 under Emacs 19.34.1 From: Mitchell Wand To: Johan Ovlinger Cc: Mitchell Wand , dem@ccs.neu.edu, pl-seminar@ccs.neu.edu Subject: Re: [Fwd: Benjamin Pierce] Subject reduction fails in Java Date: Fri, 19 Jun 1998 12:03:44 -0400 (EDT) >>>>> On Fri, 19 Jun 1998 11:53:57 -0400, Johan Ovlinger >>>>> said: JO> Well, their beta reduction fails because it is incorrect. Their JO> proposed fix is to use the correct beta reduction. JO> Let me expand: If you want to model java's method application JO> sematics, you have to do so in a way that corresponds to the language JO> definition. By just inlining the body of the function w/o the widening JO> casts that are _mandated_ by the language definition, they are JO> performing a program transformation that is incorrect. JO> I quote from the Java langauge specification JO> (http://java.sun.com/docs/books/jls/html/5.doc.html#12687) JO> 5.3 Method Invocation Conversion JO> Method invocation conversion is applied to each argument value in a JO> method or constructor invocation ('15.8, '15.11): the type of the JO> argument expression must be converted to the type of the corresponding JO> ^^^^ JO> parameter. Method invocation contexts allow the use of an identity JO> conversion ('5.1.1), a widening primitive conversion ('5.1.2), or a JO> widening reference conversion ('5.1.4). JO> A widening reference conversion is: (Object) anInt; Ah, so the beta reduction should have been {body of m}[((Object) i)/a1, ((Object) h)/a2] That would do the job.... Perhaps you should write Benli a nice note? --Mitch From gts@harlequin.com Fri Jun 19 12:18:48 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "" "19" "June" "1998" "12:17:44" "-0400" "Gregory T. Sullivan" "gts@harlequin.com" nil "8" "Re: [Fwd: Benjamin Pierce] Subject reduction fails in Java" "^From:" nil nil "6" "1998061916:17:44" nil nil nil nil] nil) Received: from hilly.harlequin.com (hilly.harlequin.com [198.3.232.58]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id MAA05174; Fri, 19 Jun 1998 12:18:48 -0400 (EDT) Received: from karst.harlequin.com (karst.harlequin.com [192.124.144.184]) by hilly.harlequin.com (8.8.4/8.8.4) with ESMTP id MAA28443; Fri, 19 Jun 1998 12:18:17 -0400 (EDT) Received: from aretha.harlequin.com (aretha.harlequin.com [192.124.144.236]) by karst.harlequin.com (8.8.4/8.8.4) with SMTP id MAA22623; Fri, 19 Jun 1998 12:17:45 -0400 (EDT) Received: by aretha.harlequin.com (5.65) id AA04750; Fri, 19 Jun 1998 12:17:45 -0400 References: <13706.31047.825966.809430@delphi.ccs.neu.edu> <199806191553.LAA08263@boron.ccs.neu.edu> <13706.35808.568485.105264@delphi.ccs.neu.edu> In-Reply-To: Mitchell Wand's message of "Fri, 19 Jun 1998 12:03:44 -0400 (EDT)" Message-Id: Lines: 8 X-Mailer: Gnus v5.6.4/Emacs 20.2 From: gts@harlequin.com (Gregory T. Sullivan) To: Mitchell Wand Cc: Johan Ovlinger Subject: Re: [Fwd: Benjamin Pierce] Subject reduction fails in Java Date: 19 Jun 1998 12:17:44 -0400 Or, could they toss the requirement that one branch of the conditional be subtype-or-eq? the other? Why not say that the type of (p ? a1 : a2) is the lub of the types of a1 and a2? Is lub not well defined in the Java type system? In their example, lub(Integer, HashTable) would probably be Object. -- Greg From types-errors@cs.indiana.edu Fri Jun 19 15:51:22 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Fri" "19" "June" "1998" "12:20:44" "-0400" "Kim Bruce" "kim@bull.cs.williams.edu" nil "31" "Re: Subject reduction fails in Java" "^From:" nil nil "6" "1998061916:20:44" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id PAA17942; Fri, 19 Jun 1998 15:51:21 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA12599 for ; Fri, 19 Jun 1998 12:57:15 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA21060 for ; Fri, 19 Jun 1998 12:57:14 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id MAA12591 for types-distrib@cs.indiana.edu; Fri, 19 Jun 1998 12:57:13 -0500 (EST) Message-Id: <199806191757.MAA12591@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Fri, 19 Jun 1998 11:20:52 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.254.191]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id LAA01389; Fri, 19 Jun 1998 11:20:51 -0500 (EST) Received: from harmony.williams.edu (harmony.williams.edu [137.165.4.25]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id LAA11260; Fri, 19 Jun 1998 11:20:50 -0500 (EST) Received: from cs.williams.edu (bull.cs.williams.edu) by williams.edu (PMDF V5.1-10 #24595) with SMTP id <0EUT005JN46D7J@williams.edu>; Fri, 19 Jun 1998 12:23:01 -0400 (EDT) Received: from chianini.williams.edu by cs.williams.edu (SMI-8.6/SMI-SVR4) id MAA15988; Fri, 19 Jun 1998 12:20:45 -0400 Received: by chianini.williams.edu (SMI-8.6/SMI-SVR4) id MAA03404; Fri, 19 Jun 1998 12:20:44 -0400 X-Sun-Charset: US-ASCII Errors-To: types-errors@cs.indiana.edu From: kim@bull.cs.williams.edu (Kim Bruce) To: types@cs.indiana.edu, pierce@cs.indiana.edu Cc: hahosoya@cs.indiana.edu, dnt@an-teallach.com Subject: Re: Subject reduction fails in Java Date: Fri, 19 Jun 1998 12:20:44 -0400 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Here is an interesting historical tidbit related to Pierce's message on Subject Reduction and Java. I was amused when I first learned (from Wadler and/or Odersky, I believe) that Java does not fully support subtyping (subsumption, actually) because of the restrictions on the if-then-else expression (written b?x:y). We ran into this problem many years ago when proving a subject-reduction theorem for TOOPLE, a functional object-oriented programming language. The proof depended on showing that each term had a minimum type. We were quite surprised to find that the if-then-else expression presented a big problem in that regard because we could write "if cond then exp1 else exp2" where the minimum types of exp1 and exp2 needed only to have a common supertype. We resolved the problem by ensuring that every pair of types with an upper bound has a least upper bound (and because of covariance problems, also a similar statement with lower bounds). The moral is that seemingly simple expressions can result in big problems when working with operational semantics (never dismiss anything as trivial!). The proof of minimum typing for TOOPLE was given in Bruce et al, "Safe & decidable type-checking in an object-oriented language" in OOPSLA '93 proceedings, pp. 29-46. The actual proof of subject-reduction of TOOPLE can be found in Bruce et al, "An operational semantics for TOOPLE: A statically typed object-oriented programming language", MFPS '93 proceedings, LNCS 802, pp. 603-626. Kim Bruce From dougo@ccs.neu.edu Fri Jun 19 12:29:03 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Fri" "19" "June" "1998" "12:28:55" "-0400" "Doug Orleans" "dougo@ccs.neu.edu" nil "22" "Re: [Fwd: Benjamin Pierce] Subject reduction fails in Java " "^From:" nil nil "6" "1998061916:28:55" nil nil nil nil] nil) Received: from vega.ccs.neu.edu (dougo@vega.ccs.neu.edu [129.10.114.125]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id MAA05631; Fri, 19 Jun 1998 12:28:57 -0400 (EDT) Received: (from dougo@localhost) by vega.ccs.neu.edu (8.8.6/8.8.6) id MAA29621; Fri, 19 Jun 1998 12:28:55 -0400 (EDT) Message-Id: <199806191628.MAA29621@vega.ccs.neu.edu> In-Reply-To: <13706.35808.568485.105264@delphi.ccs.neu.edu> References: <13706.31047.825966.809430@delphi.ccs.neu.edu> <199806191553.LAA08263@boron.ccs.neu.edu> <13706.35808.568485.105264@delphi.ccs.neu.edu> X-Mailer: VM 6.22 under 19.15p7 XEmacs Lucid X-Face: (4D-osoq?}7M3\EgvbWKo To: Mitchell Wand Cc: Johan Ovlinger , dem@ccs.neu.edu, pl-seminar@ccs.neu.edu Subject: Re: [Fwd: Benjamin Pierce] Subject reduction fails in Java Date: Fri, 19 Jun 1998 12:28:55 -0400 (EDT) Mitchell Wand writes: > Ah, so the beta reduction should have been > > {body of m}[((Object) i)/a1, ((Object) h)/a2] > > That would do the job.... Perhaps you should write Benli a nice note? That was in the original post, at the bottom. Another way of fixing it would be to loosen the restriction of the ternary expression, and have the type of (a ? b : c) be the most specific ancestor type of b and c. Then boolean b; String s; Hashtable h; Object o = (b ? s : h); is a correctly typed program. I'm not sure why the definition of the ternary expression is as restrictive as it is. Maybe multiple supertypes (interface classes) mean there might not be a unique most-specific-ancestor? Guess we need union types... --Doug From types-errors@cs.indiana.edu Fri Jun 19 15:56:24 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Fri" "19" "June" "1998" "18:00:18" "+0100" "Sophia Drossopoulou" "scd@doc.ic.ac.uk" nil "131" "Re: subject reduction fails in Java -- how it CAN be proven" "^From:" nil nil "6" "1998061917:00:18" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id PAA18209; Fri, 19 Jun 1998 15:56:23 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA12614 for ; Fri, 19 Jun 1998 12:57:34 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA21223 for ; Fri, 19 Jun 1998 12:57:33 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id MAA12605 for types-distrib@cs.indiana.edu; Fri, 19 Jun 1998 12:57:33 -0500 (EST) Message-Id: <199806191757.MAA12605@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Fri, 19 Jun 1998 12:02:40 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.254.191]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA03604 for ; Fri, 19 Jun 1998 12:02:39 -0500 (EST) Received: from scorch.doc.ic.ac.uk (scorch.doc.ic.ac.uk [146.169.2.14]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA12791 for ; Fri, 19 Jun 1998 12:02:37 -0500 (EST) Received: from doc.ic.ac.uk (dse-pc-scd.doc.ic.ac.uk [146.169.14.117]) by scorch.doc.ic.ac.uk (8.8.8/8.8.8) with ESMTP id SAA24340; Fri, 19 Jun 1998 18:02:31 +0100 (BST) X-Mailer: Mozilla 4.04 [en] (WinNT; I) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Errors-To: types-errors@cs.indiana.edu From: Sophia Drossopoulou To: types@cs.indiana.edu CC: se@doc.ic.ac.uk, Donald Syme Subject: Re: subject reduction fails in Java -- how it CAN be proven Date: Fri, 19 Jun 1998 18:00:18 +0100 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] We at IC were quite surprised and intrigued by the counterexample to the subject reduction property in Java. Indeed, we did not expect the interaction of conditional expressions and method calls to produce that effect. On the other hand, a) we feel that this problem is due to the type rule for conditionals being too weak (it should say that the type of the conditional is the most specific supertype of the two branches) b) subject reduction can be proven, namely > ... it seems, their proof methods cannot easily > be extended to deal with the full Java language including conditional > expressions. our proof can easily be extended to deal with conditional expressions. Namely, we can apply the same trick which we developed for type checking assignments (suggested by Don Syme), whereby we have different type rules for the compiled language (Java_SE), than for the run-time language (Java_R). In more detail: 1. In Java_SE require for ( b ? e1 : e2 ) that b is boolean; e1, e2 have such types that one can be widened to the other. That is: b : boolean e_1 : T_1 e_2 : T_2 (T_1 widens to T_2 and T_2=T) or (T_2 widens to T_1 and T_1=T) ---------------------------------------- ( b ? e_1 : e_2 ) : T 2. In Java_R we only require for ( b ? e1 ? e2 ) that b is boolean; e_1 and e_2 are well-typed and the whole expression has the minimal type to which those of e_1 and e_2 can be widened. That is: b : boolean e_1 : T_1 e_2 : T_2 T = min { T' | T_1 widens to T', and T_2 widens to T') ------------------------------------------------ ( b ? e_1 : e_2 ) : T 3. We prove that for a Java_SE term t with \Gamma |-_{se} t : T using the Java_SE type rules, it also holds that \Gamma |-_{r} t : T this time using the Java_R type rules 4. We can now prove the subject reduction theorem stating, that for a well typed Java_R term t, and a well-typed Java_SE program p, rewriting t (which might invoke methods from p) preserves types up to widening. Furthermore, I believe that the type rule suggested for Java_R is the rule that _should_ be given for the type of conditional expressions, and that the actual type (as described for Java_SE) is an easy approximation to it, which allows an easier implementation of the compiler. The suggestion given by Haruo Hosoya, Benjamin Pierce and David Turner, > > Integer i = new Integer(); > HashTable h = new HashTable(); > Object o = (b ? (Object)i : (Object)h); > > carrying the parameter types along explicitly during the substitution is more concise, but, I feel, it is less faithful to what really happens at run-time, since a conditional expression does not require run-time checks, whereas the conditional as transformed above does require run-time checks (which are guaranteed to succeed). Also, I feel that this feature of conditional expressions is another indication that the approach of distinguishing the compiled language from the run-time language (due to Don Syme, again), where typing in the first reflects the compile - time checks whereas typing in the latter serves the requirements of formulating and proving soundness properties, is a useful vehicle when considering full, "real-world" languages. Greetings, Sophia Drossopoulou > CITATIONS > --------- .... > [2] Drossopolou and Eisenbach, "Java is type safe -- probably," ECOOP > '97. please, consider our more recent work: Drossopoulou and Eisenbach: "Towards an Operations Semantics and Proof of Type Soundness for Java" April 1998, the most recent version of the previous work, in which we clarify and simplify many issues. This paper will appear as a chapter in a book. Also available at: http://www-dse.doc.ic.ac.uk/projects/slurp/papers.html -- Dr. Sophia Drossopoulou tel: +44 171 594 8368 http://www-ala.doc.ic.ac.uk/~scd/ Department of Computing fax: +44 171 581 8024 Imperial College of Science, Technology and Medicine LONDON SW7 2BZ, England email: sd@doc.ic.ac.uk -- Dr. Sophia Drossopoulou tel: +44 171 594 8368 http://www-ala.doc.ic.ac.uk/~scd/ Department of Computing fax: +44 171 581 8024 Imperial College of Science, Technology and Medicine LONDON SW7 2BZ, England email: sd@doc.ic.ac.uk From types-errors@cs.indiana.edu Fri Jun 19 16:22:00 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Fri" "19" "June" "1998" "13:32:34" "-0500" "Benjamin Pierce" "pierce@cs.indiana.edu" nil "114" "Subject reduction fails in Java - Part 2" "^From:" nil nil "6" "1998061918:32:34" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id QAA19388; Fri, 19 Jun 1998 16:21:59 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id NAA13087 for ; Fri, 19 Jun 1998 13:33:06 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id NAA22829 for ; Fri, 19 Jun 1998 13:33:05 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id NAA13077 for types-distrib@cs.indiana.edu; Fri, 19 Jun 1998 13:33:05 -0500 (EST) Message-Id: <199806191833.NAA13077@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Fri, 19 Jun 1998 13:32:38 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.254.191]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id NAA09009 for ; Fri, 19 Jun 1998 13:32:37 -0500 (EST) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id NAA22812 for ; Fri, 19 Jun 1998 13:32:36 -0500 (EST) Received: from localhost (pierce@localhost [127.0.0.1]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id NAA13064 for ; Fri, 19 Jun 1998 13:32:35 -0500 (EST) Reply-to: pierce@cs.indiana.edu Errors-To: types-errors@cs.indiana.edu From: Benjamin Pierce To: types@cs.indiana.edu Subject: Subject reduction fails in Java - Part 2 Date: Fri, 19 Jun 1998 13:32:34 -0500 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] SUMMARY ------- Our posting yesterday seems to have generated an unusual amount of activity on the TYPES list! The responses so far (both postings and some private emails) have basically been of two forms: 1) Some people reiterated our suggestion that a "beta reduction" rule for Java should explicitly cast the arguments to the parameter types before substituting. This solution has the advantage of dealing with the (related) difficulty with subject reduction and overloading, observed by Wadler. 2) Others proposed a different solution: change the original typing rule for conditionals from b : bool e1:E1 e2:E2 T=E1>E2 or T=E2>E1 --------------------------- (b?e1:e2) : T to (some variation of): b : bool e1:E1 e2:E2 E1 < T E2 < T --------------------------- (*) (b?e1:e2) : T That is, take the type of the conditional to be any common supertype of the types of the branches. DISCUSSION ---------- The second proposal is one that we also considered [and should have discussed in the original posting]. The problem with it is that a typechecking algorithm typically needs to calculate a single _minimal_ type for each term. But, the suggested rule (*) only admits minimal types if the subtype relation possesses a join for every pair of types. Java's subtyping relation, unfortunately, does not have all joins. For example, suppose we have Java interfaces A, B, C, and D, with the following subtyping relations declared among them: A B |\ /| | \ / | | . | | / \ | |/ \| C D Now suppose that we have declared variables x of type C and y of type D. Then, according to the rule (*), the expression (b ? x : y) could validly be either type A or type B, since these are both common supertypes of C and D. But C and D have no minimal common supertype (there is nothing in the position marked . in the diagram), so there is no "best result type" for the typechecking algorithm to return. The lack of joins seems to be a basic property of Java's approach to typing. We do not see any way to "add in joins" without substantial and fundamental changes to the type system. A THIRD APPROACH ---------------- One other approach to the original difficulty is also worth mentioning. 3) We might choose to regard the typing of the conditional as a _type inference_ problem. In this view, we would distinguish (a) the surface language in which the programmer writes from (b) a "fully typed" internal language, where some annotations have been added by the compiler. In the internal language, the conditional expression would be given an explicit type annotation (b ? x : y) in T that would determine its result type exactly: b : bool e1:E1 e2:E2 E1 < T E2 < T --------------------------- ((b?e1:e2) in T) : T The transformation from surface to internal language would involve filling in the "in T" annotations on conditionals using some simple rule such as the one currently used by Java. (Overloading resolution might also take place at this point.) Subject reduction would then be a question of preservation of typing by reductions of one internal language expression to another. [A similar division of labor between surface and internal language is being explored by the ML2000 project.] Regards, Haruo Hosoya Benjamin Pierce David Turner From types-errors@cs.indiana.edu Fri Jun 19 17:20:28 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Fri" "19" "June" "1998" "15:48:43" "-0400" "Vijay Saraswat" "vj@research.att.com" nil "29" "Re: Typing in Java" "^From:" nil nil "6" "1998061919:48:43" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id RAA22470; Fri, 19 Jun 1998 17:16:27 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id OAA14010 for ; Fri, 19 Jun 1998 14:53:17 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id OAA26263 for ; Fri, 19 Jun 1998 14:53:16 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id OAA14002 for types-distrib@cs.indiana.edu; Fri, 19 Jun 1998 14:53:16 -0500 (EST) Message-Id: <199806191953.OAA14002@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Fri, 19 Jun 1998 14:50:23 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id OAA13857 for ; Fri, 19 Jun 1998 14:50:22 -0500 (EST) Received: from rumor.research.att.com (rumor.research.att.com [192.20.225.9]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with SMTP id OAA26022 for ; Fri, 19 Jun 1998 14:50:21 -0500 (EST) Received: from research.att.com ([135.207.30.100]) by rumor; Fri Jun 19 15:44:54 EDT 1998 Received: from amontillado.research.att.com ([135.207.24.32]) by research; Fri Jun 19 15:48:31 EDT 1998 Received: from bual.research.att.com (bual.research.att.com [135.207.24.19]) by amontillado.research.att.com (8.8.7/8.8.7) with ESMTP id PAA29817; Fri, 19 Jun 1998 15:48:43 -0400 (EDT) Received: (from vj@localhost) by bual.research.att.com (8.7.5/8.7) id PAA02927; Fri, 19 Jun 1998 15:48:43 -0400 (EDT) In-reply-to: "chorn@lionet-technologies.com"'s message of Fri, 19 Jun 1998 10:27:41 +0100 Errors-To: types-errors@cs.indiana.edu From: Vijay Saraswat To: chorn@lionet-technologies.com cc: types@cs.indiana.edu Subject: Re: Typing in Java Date: Fri, 19 Jun 1998 15:48:43 -0400 (EDT) [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Date: Fri, 19 Jun 1998 10:27:41 +0100 From: chorn@lionet-technologies.com (Christian Horn) [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] The problem mentioned has nothing todo with the conditional expression and not with Java, but with the way reduction for typed languages has to be formulated with casting of the actual parameter types to the formal parameter types. > > m(a1...an) --> r[((T1)a1)/x1...((Tn)an)/xn] > Indeed the issue here isnt that "Subject reduction" is violated (it is preserved for "exact types"), but that, as Kim just remarked, the conditional violates the "OO polymorphism property": If an expression e is soundly typed under the assumption that variables X1,...,Xn have type T1,...,Tn respectively, then it is soundly typed under the assumption that X1,..., Xn have types T1', ..., Tn' respectively, where each Ti' is a subtype of Ti. From types-errors@cs.indiana.edu Fri Jun 19 18:28:46 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Fri" "19" "June" "1998" "15:57:07" "-0400" "Robert O'Callahan" "roc+@cs.cmu.edu" nil "37" "Re: subject reduction fails in Java -- how it CAN be proven" "^From:" nil nil "6" "1998061919:57:07" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id SAA25454; Fri, 19 Jun 1998 18:28:45 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id QAA16156 for ; Fri, 19 Jun 1998 16:07:25 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id QAA29268 for ; Fri, 19 Jun 1998 16:07:24 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id QAA16148 for types-distrib@cs.indiana.edu; Fri, 19 Jun 1998 16:07:23 -0500 (EST) Message-Id: <199806192107.QAA16148@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Fri, 19 Jun 1998 15:01:08 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.254.191]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id PAA14838 for ; Fri, 19 Jun 1998 15:01:07 -0500 (EST) Received: from ux1.sp.cs.cmu.edu (UX1.SP.CS.CMU.EDU [128.2.198.101]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with SMTP id PAA26644 for ; Fri, 19 Jun 1998 15:01:06 -0500 (EST) Received: from MAJESTY.FAC.CS.CMU.EDU by ux1.sp.cs.cmu.edu id aa28965; 19 Jun 98 15:58 EDT Reply-To: roc+@cs.cmu.edu Organization: Carnegie Mellon University X-Mailer: Mozilla 4.04 [en] (WinNT; I) MIME-Version: 1.0 References: <199806191757.MAA12605@shovelnose.cs.indiana.edu> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Errors-To: types-errors@cs.indiana.edu From: "Robert O'Callahan" To: types@cs.indiana.edu Subject: Re: subject reduction fails in Java -- how it CAN be proven Date: Fri, 19 Jun 1998 15:57:07 -0400 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Sophia Drossopoulou wrote: > We at IC were quite surprised and intrigued by the counterexample > to the subject reduction property in Java. Indeed, we did not expect > the interaction of conditional expressions and method calls > to produce that effect. > > On the other hand, > > a) we feel that this problem is due to the type rule for conditionals > being too weak (it should say that the type of the conditional is > the most specific supertype of the two branches) Unfortunately that's not possible. Two Java types may not have a most specific supertype, e.g. the classes X and Y: interface A { ... } interface B { ... } class X implements A, B { ... } class Y implements A, B { ... } The most specific supertype would be the combination of the two interfaces A and B, but that is not a Java type. This has already come up at the bytecode level ... see the work of Qian. The solution is obviously to fix the definition of a type --- not a problem if we're just talking about proof machinery, but perhaps more serious if it means a change to the language definition. Rob -- [Robert O'Callahan (roc+@cs.cmu.edu) 4th year CMU SCS PhD Home page: http://www.cs.cmu.edu/~roc 1 Samuel 15:22 --- "But Samuel replied: "Does the Lord delight in burnt offerings and sacrifices as much as in obeying the voice of the Lord? To obey is better than sacrifice, and to heed is better than the fat of rams."] From types-errors@cs.indiana.edu Fri Jun 19 18:11:16 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Fri" "19" "June" "1998" "16:17:25" "-0400" "Vijay Saraswat" "vj@research.att.com" nil "84" "Re: Subject reduction fails in Java" "^From:" nil nil "6" "1998061920:17:25" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id SAA24845; Fri, 19 Jun 1998 18:11:13 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id PAA15480 for ; Fri, 19 Jun 1998 15:28:00 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id PAA27734 for ; Fri, 19 Jun 1998 15:27:59 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id PAA15472 for types-distrib@cs.indiana.edu; Fri, 19 Jun 1998 15:27:58 -0500 (EST) Message-Id: <199806192027.PAA15472@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Fri, 19 Jun 1998 15:20:22 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id PAA15972; Fri, 19 Jun 1998 15:20:21 -0500 (EST) Received: from rumor.research.att.com (rumor.research.att.com [192.20.225.9]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with SMTP id PAA27327; Fri, 19 Jun 1998 15:20:19 -0500 (EST) Received: from research.att.com ([135.207.30.100]) by rumor; Fri Jun 19 16:14:51 EDT 1998 Received: from amontillado.research.att.com ([135.207.24.32]) by research; Fri Jun 19 16:17:12 EDT 1998 Received: from bual.research.att.com (bual.research.att.com [135.207.24.19]) by amontillado.research.att.com (8.8.7/8.8.7) with ESMTP id QAA00789; Fri, 19 Jun 1998 16:17:24 -0400 (EDT) Received: (from vj@localhost) by bual.research.att.com (8.7.5/8.7) id QAA03006; Fri, 19 Jun 1998 16:17:25 -0400 (EDT) In-reply-to: message from Philip Wadler on Fri, 19 Jun 1998 09:13:52 -0400 Errors-To: types-errors@cs.indiana.edu From: Vijay Saraswat To: wadler@research.bell-labs.com CC: pierce@cs.indiana.edu, types@cs.indiana.edu, hahosoya@cs.indiana.edu, dnt@an-teallach.com Subject: Re: Subject reduction fails in Java Date: Fri, 19 Jun 1998 16:17:25 -0400 (EDT) [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Delivery-Date: Fri, 19 Jun 1998 08:14:09 -0500 Cc: hahosoya@cs.indiana.edu, David Turner Date: Fri, 19 Jun 1998 09:13:52 -0400 From: Philip Wadler Errors-To: types-errors@cs.indiana.edu [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Haruo, Benli, Dave, This is the least of your problems. Reduction, in the sense you define it, can easily change the meaning of a program, thanks to Java's notion of overloading. Original program prints "true". class Counterexample { static boolean overloaded (Object x) { return true; } static int overloaded (String s) { return 42; } static void m (Object x) { System.out.println(overloaded(x)); } public static void main (String[] args) { m("hello"); } } Reduced program prints "42". class Counterexample { static boolean overloaded (Object x) { return true; } static int overloaded (String s) { return 42; } static void m (Object x) { System.out.println(overloaded(x)); } public static void main (String[] args) { System.out.println(overloaded("hello")); } } A nice concise example illustrating a common pitfall for newbie Java programmers. More details on Java's "pseudo compile-time method resolution" at http://www.javasoft.com/docs/books/jls/html/8.doc.html#227941: When a method is invoked, the number of actual arguments and the compile-time types of the argument are used, at compile-time, to determine the signature of the method that will be invoked. Note that the "right" notion of reduction for Java would unfold the program to: class Counterexample { static boolean overloaded (Object x) { return true; } static int overloaded (String s) { return 42; } static void m (Object x) { System.out.println(overloaded(x)); } public static void main (String[] args) { Object x = "hello"; System.out.println(overloaded(x)); } } Java won't brook any compile-time flow analysis that will let you infer a type for arguments "tighter" than the declared type! Why was Java designed so? Clearly, doing full run-time type resolution (checking the exact type of the arguments at run-time, and then choosing the "most refined" method body available) might be too costly. So the decision taken was to record in the bytecodes for the call (in the classfile) the actual signature (well, signature modulo classloader) of the method that compile-time resolution identifies as the target, and then to use this signature to search at run-time on the subject for the actual method. But I wonder. Is there a "better" way of resolving this problem, which would allow more accurate compile-time inference of argument types to be used? Best, Vijay From types-errors@cs.indiana.edu Fri Jun 19 21:46:00 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Fri" "19" "June" "1998" "18:07:28" "-0400" "Matt Timmermans" "matt@microstar.com" nil "41" "Re: subject reduction fails in Java" "^From:" nil nil "6" "1998061922:07:28" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id VAA00728; Fri, 19 Jun 1998 21:45:59 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id TAA18255 for ; Fri, 19 Jun 1998 19:39:14 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id TAA06203 for ; Fri, 19 Jun 1998 19:39:13 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id TAA18247 for types-distrib@cs.indiana.edu; Fri, 19 Jun 1998 19:39:12 -0500 (EST) Message-Id: <199806200039.TAA18247@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Fri, 19 Jun 1998 17:07:32 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id RAA23216 for ; Fri, 19 Jun 1998 17:07:32 -0500 (EST) Received: from otta02.microstar.com (pinkfloyd2.microstar.com [199.43.112.4]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id RAA01736 for ; Fri, 19 Jun 1998 17:07:30 -0500 (EST) Received: by otta02.microstar.com with Internet Mail Service (5.0.1458.49) id ; Fri, 19 Jun 1998 18:07:31 -0400 X-Priority: 3 MIME-Version: 1.0 X-Mailer: Internet Mail Service (5.0.1458.49) Content-Type: text/plain Errors-To: types-errors@cs.indiana.edu From: Matt Timmermans To: "'types@cs.indiana.edu'" Subject: Re: subject reduction fails in Java Date: Fri, 19 Jun 1998 18:07:28 -0400 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Benjamin Pierce [pierce@cs.indiana.edu] writes (approximately > >One possible way of formalizing this intuition is to alter the >beta-reduction rule so that: > > Object m (Object a1, Object a2) { > return (b ? a1 : a2); > } > Object o = m (i, h); > >is rewritten as > > Object o = (b ? (Object)i : (Object)h); > Or, more generally, with types A Matt Timmermans | Phone: +1 613 596-2233 Microstar Software Ltd. | Fax: +1 613 596-5934 3775 Richmond Road | E-mail: mtimmerm@microstar.com Nepean Ontario CANADA K2H 5B7 | Web: http://www.microstar.com From types-errors@cs.indiana.edu Fri Jun 19 22:07:18 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Fri" "19" "June" "1998" "18:24:35" "-0400" "Kim Bruce" "kim@bull.cs.williams.edu" nil "26" "Re: Subject reduction fails in Java - Part 2" "^From:" nil nil "6" "1998061922:24:35" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id WAA01448; Fri, 19 Jun 1998 22:07:17 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id TAA18266 for ; Fri, 19 Jun 1998 19:39:18 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id TAA06209 for ; Fri, 19 Jun 1998 19:39:17 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id TAA18258 for types-distrib@cs.indiana.edu; Fri, 19 Jun 1998 19:39:16 -0500 (EST) Message-Id: <199806200039.TAA18258@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Fri, 19 Jun 1998 17:24:42 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id RAA24387 for ; Fri, 19 Jun 1998 17:24:41 -0500 (EST) Received: from harmony.williams.edu (harmony.williams.edu [137.165.4.25]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id RAA02626; Fri, 19 Jun 1998 17:24:40 -0500 (EST) Received: from cs.williams.edu (bull.cs.williams.edu) by williams.edu (PMDF V5.1-10 #24595) with SMTP id <0EUT008BBL0RSS@williams.edu>; Fri, 19 Jun 1998 18:26:51 -0400 (EDT) Received: from chianini.williams.edu by cs.williams.edu (SMI-8.6/SMI-SVR4) id SAA16925; Fri, 19 Jun 1998 18:24:36 -0400 Received: by chianini.williams.edu (SMI-8.6/SMI-SVR4) id SAA03450; Fri, 19 Jun 1998 18:24:35 -0400 Errors-To: types-errors@cs.indiana.edu From: kim@bull.cs.williams.edu (Kim Bruce) To: pierce@cs.indiana.edu, types@cs.indiana.edu Subject: Re: Subject reduction fails in Java - Part 2 Date: Fri, 19 Jun 1998 18:24:35 -0400 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] The fact that in Java, types with upper bounds do not have least upper bounds seems to be yet another argument for the use of structural subtyping rather than "by declaration" subtyping in OO languages. Those looking at adding bounded polymorphism to Java have already run into difficulties with "by declaration" subtyping when the bound for a polymorphic function is defined after the classes you wish to instantiate it with. This is a particular problem with Java because you are not allowed to declare an "extends" or "implements" relation after the class has been defined. Interestingly, one of the claimed advantages of using "where" clauses rather than bounded polymorphism is that this problem no longer exists, but of course it is really an argument for structural subtyping (though I'm not sure the where clause proponents would accept this). The argument for "by declaration" subtyping is that it catches errors that might otherwise slip by (e.g. an accidental subtyping of a graphics class with a "draw" method and a cowboy class with a "draw" method), but has anyone ever run into such a problem in real life? I'd be interested in hearing if anyone feels there are strong advantages to "by declaration" subtyping versus structural subtyping. Kim Bruce From types-errors@cs.indiana.edu Sat Jun 20 12:04:08 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Sat" "20" "June" "1998" "16:16:13" "+1000" "Anthony Dekker" "dekker@acm.org" nil "51" "Re: subject reduction fails in Java -- how it CAN be proven" "^From:" nil nil "6" "1998062006:16:13" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id MAA14677; Sat, 20 Jun 1998 12:04:06 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id JAA21631 for ; Sat, 20 Jun 1998 09:31:28 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id JAA01869 for ; Sat, 20 Jun 1998 09:31:28 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id JAA21624 for types-distrib@cs.indiana.edu; Sat, 20 Jun 1998 09:31:27 -0500 (EST) Message-Id: <199806201431.JAA21624@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Sat, 20 Jun 1998 01:16:34 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id BAA22533 for ; Sat, 20 Jun 1998 01:16:33 -0500 (EST) Received: from oznet11.ozemail.com.au (oznet11.ozemail.com.au [203.2.192.118]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id BAA15489 for ; Sat, 20 Jun 1998 01:16:30 -0500 (EST) Received: from [203.108.192.55] (slcan2p39.ozemail.com.au [203.108.192.55]) by oznet11.ozemail.com.au (8.8.4/8.6.12) with SMTP id QAA18033; Sat, 20 Jun 1998 16:16:09 +1000 (EST) X-Sender: dekker@ozemail.com.au Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Errors-To: types-errors@cs.indiana.edu From: dekker@acm.org (Anthony Dekker) To: roc+@cs.cmu.edu, types@cs.indiana.edu Cc: malcolm.newey@cs.anu.edu.au Subject: Re: subject reduction fails in Java -- how it CAN be proven Date: Sat, 20 Jun 1998 16:16:13 +1000 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] At 3:57 PM 19/6/98, Robert O'Callahan wrote: >> a) we feel that this problem is due to the type rule for conditionals >> being too weak (it should say that the type of the conditional is >> the most specific supertype of the two branches) > >Unfortunately that's not possible. Two Java types may not have a most >specific supertype, e.g. the classes X and Y: > >interface A { ... } >interface B { ... } >class X implements A, B { ... } >class Y implements A, B { ... } > >The most specific supertype would be the combination of the two interfaces >A and B, but that is not a Java type. > >This has already come up at the bytecode level ... see the work of Qian. >The solution is obviously to fix the definition of a type --- not a problem >if we're just talking about proof machinery, but perhaps more serious if it >means a change to the language definition. At the byecode level, one can define a "type" to be a class and a set of interfaces (this is the strategy we have used in the JAWS project). The LUB of X and Y is then the pair (Object,{A,B}). One could apply this strategy at the source code level, but only by creating a new class during the rewriting process which X and Y extend (acceptable for the purposes of static partial evaluation, but not very nice): abstract class XY implements A, B { } class X extends XY implements A, B { ... } class Y extends XY implements A, B { ... } This rewriting of the program as a whole doesn't alter the semantics: it just makes a new LUB possible. Tony Dekker -------------------------------------------------------------------- Anthony Dekker dekker@ACM.org http://www.acm.org/~dekker/ PO Box 3925, Manuka ACT 2603, AUSTRALIA -------------------------------------------------------------------- From types-errors@cs.indiana.edu Sat Jun 20 12:08:51 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Sat" "20" "June" "1998" "15:16:34" "+0100" "Sophia Drossopoulou" "scd@doc.ic.ac.uk" nil "138" "Re: Subject Reduction in Java -- without joins " "^From:" nil nil "6" "1998062014:16:34" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id MAA14744; Sat, 20 Jun 1998 12:08:44 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id JAA21703 for ; Sat, 20 Jun 1998 09:39:49 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id JAA02103 for ; Sat, 20 Jun 1998 09:39:48 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id JAA21694 for types-distrib@cs.indiana.edu; Sat, 20 Jun 1998 09:39:47 -0500 (EST) Message-Id: <199806201439.JAA21694@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Sat, 20 Jun 1998 09:18:58 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.254.191]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id JAA19273 for ; Sat, 20 Jun 1998 09:18:52 -0500 (EST) Received: from scorch.doc.ic.ac.uk (scorch.doc.ic.ac.uk [146.169.2.14]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id JAA01650 for ; Sat, 20 Jun 1998 09:18:50 -0500 (EST) Received: from doc.ic.ac.uk (dse-pc-scd.doc.ic.ac.uk [146.169.14.117]) by scorch.doc.ic.ac.uk (8.8.8/8.8.8) with ESMTP id PAA09428; Sat, 20 Jun 1998 15:18:48 +0100 (BST) X-Mailer: Mozilla 4.04 [en] (WinNT; I) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Errors-To: types-errors@cs.indiana.edu From: Sophia Drossopoulou To: TYPES CC: se@doc.ic.ac.uk, dpw@doc.ic.ac.uk, Tanya Valyevych , Vishnu Kotrahars , David von OheimB Subject: Re: Subject Reduction in Java -- without joins Date: Sat, 20 Jun 1998 15:16:34 +0100 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] I feel that we all agreed so far, that conditional expressions as defined in Java now 1) do not satisfy subject reduction for small step semantics 2) do not create any possibility for breaking the type system, so are not a serious threat to soundness of the type system Therefore, as well as thinking about improving the language definition, it is interesting to try to formalize the situation as is and prove soundness. I see the following alternatives: 1) Use large step semantics -- I believe that the Nipkov/vonOheimB proof could be extended to describe conditional expressions without any problems. 2) Some variation of the idea that the language executed is an "enrichment" of the original language (e.g. enriched by signatures in the case of method calls). More about this later on. I feel that an interesting lesson is, that oo languages may be sound even if they do not satisfy the "OO polymorphism property" or "substitution property". > If an expression e is soundly typed under the assumption that > variables X1,...,Xn have type T1,...,Tn respectively, then it > is soundly typed under the assumption that X1,..., Xn have > types T1', ..., Tn' respectively, where each Ti' is subtype of Ti. Now, in more detail, about alternative 2: 2.1 > From: Benjamin Pierce, Date: Fri, 19 Jun 1998 13:32:34 -0500 > ... a "beta reduction" rule for Java should explicitly cast > the arguments to the parameter types before substituting. This casting is only necessary is order to help the type system, and one would not like a real implementation to be performing all these checks at run-time. 2.2 How about introducing a special kind of casting that is just a type annotation used for describing types, but is not executed? This would - I suppose - correspond to the THIRD APPROACH as described in Benjamin Pierce's message. I feel this is better than the normal casts, but still do not like entering in the compiled language information that is only necessary to support the proof of subject reduction. 2.3 Another suggestion would be to allow expressions of the run-time language to have many types, and to reformulate the "OO polymorphism" and subject reduction properties accordingly. 2.4 The last idea is to restrict syntactically the language under consideration and allow conditionals to appear only after assignments -- thus the type of the left hand side plays the role of the type annotation in suggestions 1 and 2. More details on 2.3 ------------------- 1) For the original language type rule for conditionals remains as is 2) For the run-time language the type rule for conditionals is b : bool e1:E1 e2:E2 E1 < T E2 < T ----------------------------------------- (b?e1:e2) T that is, the conditional may have many types. 3) The "OO polymorphism property" is modified to say that: If \Gamma, X1:T1, .. Xn:Tn |- e : T then, for T1', ..., Tn', where each Ti' is subtype of Ti, there exists a type T'', such that * \Gamma, X1:T1, .. Xn:Tn |- e : T'' * \Gamma, X1:T1', .. Xn:Tn' |- e : T' * T' is subtype of T'' In other words, substitution preserves _one of the types_ of the expression e. 3) The subject reduction theorem also has to be modified to say If \Gamma |- e : T, and e non-ground, then then, there exists a T', T'', e' such that 1. Case * e rewrtites to e' * \Gamma |- e : T'' * \Gamma, |- e' : T' * T' is subtype of T'' 2. Case an exception was raised 4) The soundness theorem then says that If |- e : T in the original language, then execution of the term will produce value of a subtype of T (remember that types in the original language are unique) I 'll think about 2.3 over the week end. Now, More on details on 2.4 ----------------------- This seems more straightforward. 1. require conditional expressions to appear only after assignments, something like a conditional assignment operator, which may only appear as as statement = ? : , e.g. x = ( b ? e1 : e2 ) where x is any variable, and b, e1, e2 any expressions 2. In Java_SE require for x = ( b ? e1 ? e2 ) that b is boolean; e1, e2 have such types that one can be widened to the other; the types of e1 and e2 can be widened to that of x 3. In Java_R we only require for x = ( b ? e1 ? e2 ) that b is boolean; the types of e1 and e2 can be widened to that of x 4. We can then prove the subject reduction theorem The syntactic restriction does not really restrict the expresive power of Java, since it only requires the introduction of local variuables to transform any Java program inbto one that satisfies the restriction =============================================================================== Have a nice week-end, Sophia From types-errors@cs.indiana.edu Sat Jun 20 15:48:06 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Sat" "20" "June" "1998" "19:59:22" "+0200" "Gang CHEN" "Chen.Gang@ens.fr" nil "43" "Re: Subject reduction fails in Java -- coercions of Luo" "^From:" nil nil "6" "1998062017:59:22" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id PAA19109; Sat, 20 Jun 1998 15:48:02 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id NAA23581 for ; Sat, 20 Jun 1998 13:15:14 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id NAA06696 for ; Sat, 20 Jun 1998 13:15:13 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id NAA23573 for types-distrib@cs.indiana.edu; Sat, 20 Jun 1998 13:15:12 -0500 (EST) Message-Id: <199806201815.NAA23573@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Sat, 20 Jun 1998 13:12:51 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id NAA01825 for ; Sat, 20 Jun 1998 13:12:50 -0500 (EST) Received: from nef.ens.fr (nef.ens.fr [129.199.96.12]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id NAA06637 for ; Sat, 20 Jun 1998 13:12:49 -0500 (EST) Received: from dmi.ens.fr (dmi.ens.fr [129.199.96.11]) by nef.ens.fr (8.8.7/jtpda-5.1) with ESMTP id UAA13268 ; Sat, 20 Jun 1998 20:12:10 +0200 (MET DST) Received: from ens.fr (ppp-7.ens.fr [129.199.1.166]) by dmi.ens.fr (8.8.8/jtpda-5.1) with ESMTP id UAA28249 ; Sat, 20 Jun 1998 20:12:08 +0200 (MET DST) X-Mailer: Mozilla 4.05 [en] (Win95; I) MIME-Version: 1.0 References: <199806191756.MAA12569@shovelnose.cs.indiana.edu> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Errors-To: types-errors@cs.indiana.edu From: Gang CHEN To: Zhaohui Luo CC: types@cs.indiana.edu Subject: Re: Subject reduction fails in Java -- coercions of Luo Date: Sat, 20 Jun 1998 19:59:22 +0200 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Zhaohui Luo wrote: > Java-conversions (the widening conversions) can be regarded as what we > have called "coercions". In the framework of coercive subtyping, if > f:K->K', a:K0, and K0 <_c K (ie, K is a subtype via coercion c), then > > f(a) is computationally equal to (reduces to) f(c(a)) > > In particular, ([x:K]b)(a) does not reduce to [a/x]b, but it reduces to > > ([x:K]b)(c(a)) (coercion insertion as reduction) > > which beta-reduces to [c(a)/x]b. In other words, reductions such as beta > cannot be done directly when the argument's type is a proper subtype of > the required type; instead, a coercion (or type-casting operation, or > conversion in Java's term) has to be inserted (as a step of reduction) > before the reduction (beta in the above example) can be done. ... I agree with the main idea of coercion inference. But it is not clear why coercion insertion takes place at run time? It seems less efficient than the coercion inference at compile time . > I am very interested in this and hope to get your further opinions. Do > you know of other related work that uses the similar ideas to deal with > these situations? (Please let me know if so.) > In my thesis (available at http://www.dmi.ens.fr/~gang), I have studied coercive subtyping to the Calculus of Constructions(CC). It contains proofs of the completeness of coercion and the completeness of coercion inference among other things. I have not changed the notion of reduction. In implementation, coercion inference of a term should be done before its execution. Regards. Gang Chen From types-errors@cs.indiana.edu Sat Jun 20 15:48:54 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Sat" "20" "June" "1998" "13:07:14" "-0500" "Gary T. Leavens" "leavens@cs.iastate.edu" nil "57" "Re: Subject reduction fails in Java - Part 2" "^From:" nil nil "6" "1998062018:07:14" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id PAA19199; Sat, 20 Jun 1998 15:48:53 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id NAA23530 for ; Sat, 20 Jun 1998 13:12:28 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id NAA06633 for ; Sat, 20 Jun 1998 13:12:27 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id NAA23522 for types-distrib@cs.indiana.edu; Sat, 20 Jun 1998 13:12:27 -0500 (EST) Message-Id: <199806201812.NAA23522@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Sat, 20 Jun 1998 13:07:19 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id NAA01719 for ; Sat, 20 Jun 1998 13:07:18 -0500 (EST) Received: from flash.cs.iastate.edu (root@flash.cs.iastate.edu [129.186.3.1]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id NAA06561 for ; Sat, 20 Jun 1998 13:07:17 -0500 (EST) Received: from ren.cs.iastate.edu (ren.cs.iastate.edu [129.186.3.41]) by flash.cs.iastate.edu (8.8.7/8.8.7) with ESMTP id NAA25697; Sat, 20 Jun 1998 13:07:15 -0500 (CDT) Received: (from leavens@localhost) by ren.cs.iastate.edu (8.8.7/8.7.1) id NAA27175; Sat, 20 Jun 1998 13:07:14 -0500 (CDT) In-reply-to: <199806200039.TAA18258@shovelnose.cs.indiana.edu> (kim@bull.cs.williams.edu) Errors-To: types-errors@cs.indiana.edu From: "Gary T. Leavens" To: kim@bull.cs.williams.edu CC: types@cs.indiana.edu, leavens@cs.iastate.edu Subject: Re: Subject reduction fails in Java - Part 2 Date: Sat, 20 Jun 1998 13:07:14 -0500 (CDT) [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Kim Bruce writes: > I'd be interested in hearing if anyone feels there are strong advantages > to "by declaration" subtyping versus structural subtyping. One possible advantage of "by declaration" (or "by name" or "occurrence") subtyping is that the programmer can inform the type system of behavioral subtype relationships. Most type systems do not express information about behavioral specifications, and most langauge implementations, even if they had such information, would not want to do the theorem proving required to prove behavioral subtyping relationships structurally, as that is undecideable in general. (An exception is Abadi and Leino's work [1].) Furthermore, it is useful to have the type system check that only behavioral subtypes are used as subtypes, as that automates part of the verification of OO programs. Moreover, when a language has a declaration that says that a type is a subtype of some other type(s), one can automatically introduce proof obligations for the subtype, or use specification inheritance to force behavioral subtype relationships (as in [2]). If potential supertypes are unknown, then a verification logic has no way to do introduce these proof obligations once and for all, but instead must introduce them at each point of use of one type as a subtype of another (as described above). That said, as a Java programmer, I've often wished for structural subtyping, as it's impossible to provide, for example, a reusable container class that relies on the elements implementing some interface. You simply can't expect that other people would know enough to implement that interface ahead of time. I expect that the same arguments also apply to behavioral subtyping, so it may be, in the end, that we want to make verification logics (like [1]) that do this structurally as well, trading complications in the logic for more reuse. REFERENCES [1] Martin Abadi and Rustan Leino. A Logic of Object-Oriented Programs. In Michel Bidoit and Max Dauchet (eds.), TAPSOFT '97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille, France, pages 682-696. Volume 1214 of Lecture Notes in Computer Science, Springer-Verlag 1997. [2] Krishna Kishore Dhara and Gary T. Leavens. Forcing Behavioral Subtyping Through Specification Inheritance. In Proceedings 18th International Conference on Software Engineering, Berlin, Germany, pages 258-267. IEEE, 1996. An extended and slightly revised version is Department of Computer Science, Iowa State University, TR #95-20c, March 1997. ftp://ftp.cs.iastate.edu/pub/techreports/TR95-20/TR.ps.gz Gary From types-errors@cs.indiana.edu Sat Jun 20 19:00:37 1998 Status: RO X-VM-v5-Data: ([nil nil nil t nil nil nil nil nil] [nil "Sat" "20" "June" "1998" "17:10:27" "-0400" "Drew Dean" "ddean@cs.princeton.edu" nil "40" "Re: Subject Reduction in Java -- without joins " "^From:" nil nil "6" "1998062021:10:27" nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id TAA23824; Sat, 20 Jun 1998 19:00:36 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id QAA25491 for ; Sat, 20 Jun 1998 16:18:52 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id QAA10693 for ; Sat, 20 Jun 1998 16:18:51 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id QAA25483 for types-distrib@cs.indiana.edu; Sat, 20 Jun 1998 16:18:50 -0500 (EST) Message-Id: <199806202118.QAA25483@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Sat, 20 Jun 1998 16:11:56 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id QAA12089 for ; Sat, 20 Jun 1998 16:11:55 -0500 (EST) Received: from CS.Princeton.EDU (root@CS.Princeton.EDU [128.112.136.10]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id QAA10626 for ; Sat, 20 Jun 1998 16:11:54 -0500 (EST) Received: from caesar (ddean@caesar.CS.Princeton.EDU [128.112.136.40]) by CS.Princeton.EDU (8.8.8/8.8.8) with SMTP id RAA06011; Sat, 20 Jun 1998 17:10:28 -0400 (EDT) Received: from localhost by caesar (SMI-8.6) id RAA22265; Sat, 20 Jun 1998 17:10:27 -0400 In-Reply-To: Your message of "Sat, 20 Jun 1998 15:16:34 +0100" References: <199806201439.JAA21694@shovelnose.cs.indiana.edu> X-Mailer: Mew version 1.69 on Emacs 19.31.1 Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit Errors-To: types-errors@cs.indiana.edu From: Drew Dean To: scd@doc.ic.ac.uk Cc: types@cs.indiana.edu, se@doc.ic.ac.uk, dpw@doc.ic.ac.uk, tanya@cs.city.ac.uk, vk1@doc.ic.ac.uk, oheimb@informatik.tu-muenchen.de Subject: Re: Subject Reduction in Java -- without joins Date: Sat, 20 Jun 1998 17:10:27 -0400 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] > > From: Benjamin Pierce, Date: Fri, 19 Jun 1998 13:32:34 -0500 > > ... a "beta reduction" rule for Java should explicitly cast > > the arguments to the parameter types before substituting. > This casting is only necessary is order to help the type system, > and one would not like a real implementation to be performing > all these checks at run-time. > > 2.2 How about introducing a special kind of casting that is just a type > annotation used for describing types, but is not executed? This > would - I suppose - correspond to the THIRD APPROACH as described in > Benjamin Pierce's message. > > I feel this is better than the normal casts, but still do not like > entering in the compiled language information that is only necessary > to support the proof of subject reduction. I'm away from my copy of the language spec, so please be gentle if I misremember here. Widening casts shouldn't actually generate code -- the bytecode verifier has to do the right thing here. The lack of a common supertype for multiple interfaces has been independently rediscovered by lots of folks -- Sophia Drossopoulou was the first to point it out to me; Ken Zadeck also (re)discovered the problem, and noted that Sun's JVM does not follow the JVM spec here. If memory serves properly, the VM is _not_ required (by the spec) to handle this case; i.e., the spec says such uses of interfaces are not valid programs. The widening cast to Object is a particularly interesting special case, because it is certainly the intention of Java (modulo various ClassLoader problems) that all objects will be instances of (sub)classes of Object. Thus, we _know_ the cast will succeed, statically. So it seems like the type-checker needs some information to handle this, but we don't need dynamic checks. The question is, "How does this generalize?" Drew Dean From types-errors@cs.indiana.edu Tue Jun 23 01:56:54 1998 Status: RO X-VM-v5-Data: ([nil nil nil nil nil nil nil nil nil] [nil "Sun" "21" "June" "1998" "19:01:38" "-0500" "Matthias Felleisen" "matthias@cs.rice.edu" nil "56" "Re: Subject reduction fails in Java" "^From:" nil nil "6" nil nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id BAA18918; Tue, 23 Jun 1998 01:56:52 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id XAA12319 for ; Mon, 22 Jun 1998 23:20:09 -0500 (EST) Received: from cslinux1.cs.indiana.edu (ppierce.cs.indiana.edu [129.79.240.243]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id XAA22505 for ; Mon, 22 Jun 1998 23:20:06 -0500 (EST) Received: (from pierce@localhost) by cslinux1.cs.indiana.edu (8.8.7/8.8.7) id WAA03995 for types-distrib@cs.indiana.edu; Mon, 22 Jun 1998 22:47:30 -0500 Message-Id: <199806230347.WAA03995@cslinux1.cs.indiana.edu> X-Authentication-Warning: cslinux1.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Sun, 21 Jun 1998 19:01:43 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.254.191]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id TAA07270 for ; Sun, 21 Jun 1998 19:01:42 -0500 (EST) Received: from cs.rice.edu (cs.rice.edu [128.42.1.30]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id TAA19073 for ; Sun, 21 Jun 1998 19:01:41 -0500 (EST) Received: from africa.cs.rice.edu (africa.cs.rice.edu [128.42.1.175]) by cs.rice.edu (8.8.5/8.8.4) with ESMTP id TAA20897; Sun, 21 Jun 1998 19:01:39 -0500 (CDT) Received: (from matthias@localhost) by africa.cs.rice.edu (8.9.0/8.9.0) id TAA06162; Sun, 21 Jun 1998 19:01:38 -0500 (CDT) Reply-to: matthias@rice.edu Errors-To: types-errors@cs.indiana.edu From: Matthias Felleisen To: types@cs.indiana.edu CC: mflatt@cs.rice.edu, shriram@cs.rice.edu Subject: Re: Subject reduction fails in Java Date: Sun, 21 Jun 1998 19:01:38 -0500 (CDT) [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Dear All: Before you jump on Java or the typing rules, you may wish to consider the *full* context of the discussion. Java is *not* a functional language. It is an imperative language and, if we wish to prove all of Java type sound, we should include assignment in the reduction semantics. Felleisen-Friedman-Hieb (popl 87, tcs 87, 89) have shown that this strategy is possible. Felleisen-Wright (rice 91/info-comp 94) have shown how to prove type-soundness for core ML. At POPL'98, Flatt-Krishnamurthi-Felleisen show how to scale this approach to Java. Proving type soundness of Java + if-expressions using small-step subject-reduction is then straightforward. Here is the approximate reduction according to FSF98: Object m (Object a1, Object a2) { return (b ? a1 : a2); } Integer i = new Integer(); HashTable h = new HashTable(); Object o = m (i, h); --> Object m (Object a1, Object a2) { return (b ? a1 : a2); } Integer i = new Integer(); HashTable h = new HashTable(); Object a1 = ; Object a2 = ; Object o = (b ? a1 : a2); More generally, the FSF approach requires a (minor) elaboration from surface syntax into core syntax and the rewriting happens on core syntax. Every intermediate stage can trivially be converted into a running Java program (we carry along a quasi-store, i.e., we use the Felleisen-Hieb trick, and it must be converted into definitions). -- The rewriting model is close to an implementation in that sense, even though it can be read at the surface syntax model. I do not consider this a plus or a minus of a model, I simply wish to point out an attribute. Personally I believe a model should be useful for reasoning in context. If the question concerns types, please ignore the above remarks and excuse their length. Regards -- Matthias Felleisen P.S. I conjecture that Phil Wadler's example also disappears. From types-errors@cs.indiana.edu Tue Jun 23 02:02:33 1998 Status: RO X-VM-v5-Data: ([nil nil nil nil nil nil nil nil nil] [nil "Mon" "22" "June" "1998" "00:12:43" "+0100" "Donald Syme" "Donald.Syme@cl.cam.ac.uk" nil "205" "Re: Subject reduction fails in Java" "^From:" nil nil "6" nil nil nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id CAA19000; Tue, 23 Jun 1998 02:02:31 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id XAA12335 for ; Mon, 22 Jun 1998 23:23:17 -0500 (EST) Received: from cslinux1.cs.indiana.edu (ppierce.cs.indiana.edu [129.79.240.243]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id XAA22667 for ; Mon, 22 Jun 1998 23:23:13 -0500 (EST) Received: (from pierce@localhost) by cslinux1.cs.indiana.edu (8.8.7/8.8.7) id WAA04003 for types-distrib@cs.indiana.edu; Mon, 22 Jun 1998 22:50:37 -0500 Message-Id: <199806230350.WAA04003@cslinux1.cs.indiana.edu> X-Authentication-Warning: cslinux1.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Sun, 21 Jun 1998 20:27:27 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id UAA11803; Sun, 21 Jun 1998 20:27:26 -0500 (EST) Received: from heaton.cl.cam.ac.uk (exim@heaton.cl.cam.ac.uk [128.232.0.11]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with SMTP id UAA20794; Sun, 21 Jun 1998 20:27:23 -0500 (EST) Received: from merganser.cl.cam.ac.uk (cl.cam.ac.uk) [128.232.0.49] (drs1004) by heaton.cl.cam.ac.uk with esmtp (Exim 1.82 #1) id 0yntI3-0004ME-00; Mon, 22 Jun 1998 00:12:51 +0100 X-Mailer: exmh version 2.0.2+CL 2/24/98 Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Errors-To: types-errors@cs.indiana.edu From: Donald Syme To: types@cs.indiana.edu cc: pierce@cs.indiana.edu, hahosoya@cs.indiana.edu, David Turner Subject: Re: Subject reduction fails in Java Date: Mon, 22 Jun 1998 00:12:43 +0100 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Here's my take on the issue that Haruo et al. have raised. It describes the method I currently use to tackle this kind of problem in my theorem prover based verifications of subject reduction for Sophia and Susan's subset of Java (I'm sure others have used the method before). I hope it's of use. I'm away for the next week so please be patient with follow ups. First a general point: (a) Sooner or later we want to be able to reason about dynamic semantics that do not have access to additional type annotations. That is, ultimately we would like to be able to formulate arguments for the type correctness of "real" implementations of languages, or at least close approximations to them. These do not carry around much type information, and so further annotating our runtime apparatus with types is, from my perspective, "cheating". It is in a way potentially giving us theoreticians access to more information than is really available to those poor compiler writers. (A separate argument could be formulated to demonstrate that we don't really use this information to modify the course of a computation, but as it turns out we don't need the annotations anyway). [ Note I prefer to call the dynamic semantics the "runtime machine" to emphasise that it must be an idealised interpreter, or, even better, a formal description of a real implementation of, say, a JVM. ] Now two specific points: (b) In general, it is impossible to give *exact* types to terms that occur in runtime machines. We should use a compatibility relation instead. (c) It is a mistake is to assume that static typing rules should also apply to *all* terms that appear at runtime. That is, we should not expect the rules for the compatibility relation to be just the rules for the static type system plus widening. Let's discuss (b) first. Typically a lot of information may be thrown away when compiling to runtime terms (e.g. assembly code), and execution itself may muddy the waters further. For example an "honest" dynamic semantics for a JVM would use the same term to represent the null object and the 0 integer (of the correct length): we can't tell, by looking at the dynamic structures alone, what types the terms have. Type erasure and other optimizations that occur in real compilers pretty much guarantee there will be ambiguity in the types of runtime terms. [ Aside: There is a similar problem with the runtime treatment of datatype constructors for any faithful descriptions of Standard ML: in most implementations datatype constructors get mapped to a very ambiguous integer tag! I believe (and forgive me Myra if I'm wrong) that Myra van Inwegen hit a related difficulty in her thesis [2], where she failed to use a compatibility relation and instead tried to recover an exact type from insufficient runtime information. ] The solution is to come up with a compatibility relation between types and runtime terms. Thus, -- to type runtime structures we use compatibility -- to type statically we use exact types So, to verify the type correctness of a runtime machine, we must demonstrate the continuing compatibility of term (and its derivatives) with its static type. Compatibility must simply be strict enough to ensure: -- the machine doesn't get stuck (i.e. can always make a transition unless the program terminates) -- any outputs from the runtime machine are compatible with their expected types. Applying this methodology to our two examples... 1. Conditionals Say we have statically typed (b ? e1 : e2) to T, using the standard rule b : boolean e_1 : T_1 e_2 : T_2 (T_1 widens to T_2 and T_2=T) or (T_2 widens to T_1 and T_1=T) ---------------------------------------- ( b ? e_1 : e_2 ) : T The compatibility (<:) rule for dynamic terms of this form will be: b <: boolean e_1 <: T_1 e_2 <: T_2 T_1 widens to T T_2 widens to T ------------------------------------------------ ( b ? e_1 : e_2 ) <: T T is not uniquely determined by this rule and need not be minimal: we just need to show that the type bounds derived during static checking are not exceeded during reduction. (The rule is like the one Haruo et al. suggest except without the explicit annotation, which we can fill in as part of the subject reduction proof, based on the static type judgment for the corresponding original term). Thus, to use the original example, m (i, h) <: Object certainly holds (the compatibility rule for terms containing procedure calls will simply check compatibility of arguments and results in the obvious way, since it has access to the types of the method "m") as does (b ? i : h) <: Object because Object is a common supertype. Note it is a mistake is to suppose that static typing rules should also apply to all terms that appear at runtime: looser rules must be used for the terms that appear along the way (which is as we would expect: compiled code can do whatever it likes for a while as long as all paths eventually lead to a state where type sanity is restored. The compatibility relation is used to capture the invariant along the way). [ This approach is roughly Sophia's (2.3) suggestion, applied to the notion of compatibility, which makes the statement of subject reduction more succinct: If \Gamma |- e <: T, and e non-ground and e ---> e' then 1. Case * \Gamma |- e' <: T 2. Case an exception was raised (plus various invariants needed to make the proof go through...) ] 2. Array Assignment In the Java static semantics the array rule is arr : T[] idx : INT v : T' T' widens_to T ------------------------- arr[idx] := v : void Of course a runtime typecheck is needed for array assignments because as execution progresses "arr" might become narrower, as might "v", and no one knows a priori what situation we'll end up in. So (presuming the evaluation of "arr" and "v" actually terminate) we will arrive at the point where - "arr" has runtime-type T''[] (via a real runtime type annotation) - "v" has runtime-type T''' and we dynamically check that T''' widens to T''. The question is "what terms appear along the way, and can we use the static rule above to type them? " The answer is no: as execution progresses, "arr" might become too narrow for this rule, even though "v" might subsequently reduce to something even narrower so the runtime typecheck will pass. Again the solution is not to add more type annotations, but to weaken the rule for compatibility for runtime terms: arr <: T[] idx <: INT v <: T' ------------------------- arr[idx] := v <: void We assert no relation between T and T' (actually we may need some weak relation depending on the strength of the runtime checks: e.g. if one of T and T' is a primitive type then they must be identical, since no runtime typechecks are carried out for primitive type array assignments). Finally, note that we do sometimes need a notion of "exact typing" for runtime terms, when reducing the left hand side of an assignment. In Java we must prove that the "exact types" of field accesses and local variable mutable cells are maintained by execution prior to dereferencing, because there are no runtime checks for these. Cheers, Don ----------------------------------------------------------------------------- At the lab: At home: The Computer Laboratory Trinity Hall New Museums Site CB2 1TJ University of Cambridge Cambridge, UK CB2 3QG, Cambridge, UK Ph: +44 (0) 1223 334688 Ph: +44 (0) 1223 563783 http://www.cl.cam.ac.uk/users/drs1004/ email: drs1004@cl.cam.ac.uk ----------------------------------------------------------------------------- From types-errors@cs.indiana.edu Tue Jun 23 13:49:05 1998 Status: RO X-VM-v5-Data: ([nil nil nil nil nil nil nil nil nil] [nil "Tue" "23" "June" "1998" "08:53:13" "-0400" "Carl Gunter" "gunter@saul.cis.upenn.edu" nil "31" "Re: Subject reduction fails in Java" "^From:" nil nil "6" nil "Subject reduction fails in Java" nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id NAA11954; Tue, 23 Jun 1998 13:49:02 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id KAA15640 for ; Tue, 23 Jun 1998 10:52:59 -0500 (EST) Received: from cslinux1.cs.indiana.edu (cslinux1.cs.indiana.edu [129.79.244.160]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id KAA08029 for ; Tue, 23 Jun 1998 10:52:58 -0500 (EST) Received: (from pierce@localhost) by cslinux1.cs.indiana.edu (8.8.7/8.8.7) id KAA04652 for types-distrib@cs.indiana.edu; Tue, 23 Jun 1998 10:20:29 -0500 Message-Id: <199806231520.KAA04652@cslinux1.cs.indiana.edu> X-Authentication-Warning: cslinux1.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Tue, 23 Jun 1998 09:17:44 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.254.191]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id JAA00453 for ; Tue, 23 Jun 1998 09:17:42 -0500 (EST) Received: from linc.cis.upenn.edu (LINC.CIS.UPENN.EDU [158.130.12.3]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id JAA00080 for ; Tue, 23 Jun 1998 09:17:41 -0500 (EST) Received: from saul.cis.upenn.edu (SAUL.CIS.UPENN.EDU [158.130.12.4]) by linc.cis.upenn.edu (8.8.5/8.8.5) with ESMTP id IAA09394; Tue, 23 Jun 1998 08:53:13 -0400 (EDT) Received: (from gunter@localhost) by saul.cis.upenn.edu (8.8.5/8.8.5) id IAA02353; Tue, 23 Jun 1998 08:53:13 -0400 (EDT) In-reply-to: <199806230347.WAA03995@cslinux1.cs.indiana.edu> (message from Matthias Felleisen on Sun, 21 Jun 1998 19:01:38 -0500 (CDT)) Errors-To: types-errors@cs.indiana.edu From: Carl Gunter To: matthias@rice.edu CC: types@cs.indiana.edu, mflatt@cs.rice.edu, shriram@cs.rice.edu Subject: Re: Subject reduction fails in Java Date: Tue, 23 Jun 1998 08:53:13 -0400 (EDT) [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Date: Sun, 21 Jun 1998 19:01:38 -0500 (CDT) From: Matthias Felleisen [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Dear All: Before you jump on Java or the typing rules, you may wish to consider the *full* context of the discussion. Java is *not* a functional language. It is an imperative language and, if we wish to prove all of Java type sound, we should include assignment in the reduction semantics. Felleisen-Friedman-Hieb (popl 87, tcs 87, 89) have shown that this strategy is possible. Felleisen-Wright (rice 91/info-comp 94) have shown how to prove type-soundness for core ML. At POPL'98, Perhaps you mean that type-soundness was proved for an idealized language containing key constructs like those of core ML. Proving type-soundness of core ML is a completely different task. Flatt-Krishnamurthi-Felleisen show how to scale this approach to Java. Proving type soundness of Java + if-expressions using small-step subject-reduction is then straightforward. Do you mean Java or an idealized language with key contructs like those of Java? The Java definition is a big fat book with hundreds of constructs. A written-out proof of its soundness would probably be at least that long even if it didn't include the formalization itself. From types-errors@cs.indiana.edu Tue Jun 23 14:00:42 1998 Status: RO X-VM-v5-Data: ([nil nil nil nil nil nil nil nil nil] [nil "Tue" "23" "June" "1998" "08:09:45" "-0500" "Matthias Felleisen" "matthias@cs.rice.edu" nil "19" "Re: Subject reduction fails in Java" "^From:" nil nil "6" nil "Subject reduction fails in Java" nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id OAA12582; Tue, 23 Jun 1998 14:00:40 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id KAA15649 for ; Tue, 23 Jun 1998 10:53:10 -0500 (EST) Received: from cslinux1.cs.indiana.edu (cslinux1.cs.indiana.edu [129.79.244.160]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id KAA08039 for ; Tue, 23 Jun 1998 10:53:09 -0500 (EST) Received: (from pierce@localhost) by cslinux1.cs.indiana.edu (8.8.7/8.8.7) id KAA04660 for types-distrib@cs.indiana.edu; Tue, 23 Jun 1998 10:20:40 -0500 Message-Id: <199806231520.KAA04660@cslinux1.cs.indiana.edu> X-Authentication-Warning: cslinux1.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Tue, 23 Jun 1998 09:11:07 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id JAA29680 for ; Tue, 23 Jun 1998 09:11:05 -0500 (EST) Received: from cs.rice.edu (cs.rice.edu [128.42.1.30]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id IAA25461 for ; Tue, 23 Jun 1998 08:44:31 -0500 (EST) Received: from africa.cs.rice.edu (africa.cs.rice.edu [128.42.1.175]) by cs.rice.edu (8.9.0/8.9.0) with ESMTP id IAA10281; Tue, 23 Jun 1998 08:09:45 -0500 (CDT) Received: (from matthias@localhost) by africa.cs.rice.edu (8.9.0/8.9.0) id IAA06946; Tue, 23 Jun 1998 08:09:45 -0500 (CDT) In-reply-to: <199806231253.IAA02353@saul.cis.upenn.edu> (message from Carl Gunter on Tue, 23 Jun 1998 08:53:13 -0400 (EDT)) Reply-to: matthias@rice.edu Errors-To: types-errors@cs.indiana.edu From: Matthias Felleisen To: gunter@saul.cis.upenn.edu CC: types@cs.indiana.edu, mflatt@cs.rice.edu, shriram@cs.rice.edu Subject: Re: Subject reduction fails in Java Date: Tue, 23 Jun 1998 08:09:45 -0500 (CDT) [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] [This is a response to two people ...] Carl, yes, I meant "models" of the languages Ml and Java in the sense of physical models (ignore friction and let's study the rest). Apologies if this causes confusion, but the point of my message remains the same. Donald, the til & tal projects at Cornell and CMU use type information at ALL stages of compilation/implementation. They are successful in exploiting them. I don't think that this is an issue of theoreticians making strong assumptions. Furthermore, it is perfectly okay to formulate models that are good for one purpose (say, proving type soundness) and others that are good for other purposes (say, proving a jvm implementation correct). If you do so, you need to relate the models with (strong) adequacy theorems to ensure that the two evaluation sequences ("executions") preserves the correct "subject" so that your other theorems make sense. But that should be all. Regards -- Matthias From types-errors@cs.indiana.edu Tue Jun 23 15:58:34 1998 Status: RO X-VM-v5-Data: ([nil nil nil nil nil nil nil nil nil] [nil "Tue" "23" "June" "1998" "13:06:28" "-0400" "Robert Harper" "rwh@cs.cmu.edu" nil "81" "RE: Subject reduction fails in Java - Part 2" "^From:" nil nil "6" nil "Subject reduction fails in Java - Part 2" nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id PAA19683; Tue, 23 Jun 1998 15:58:33 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA17177 for ; Tue, 23 Jun 1998 12:24:18 -0500 (EST) Received: from shovelnose.cs.indiana.edu (pierce@shovelnose.cs.indiana.edu [129.79.244.203]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA15252 for ; Tue, 23 Jun 1998 12:24:17 -0500 (EST) Received: (from pierce@localhost) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) id MAA17169 for types-distrib@cs.indiana.edu; Tue, 23 Jun 1998 12:24:16 -0500 (EST) Message-Id: <199806231724.MAA17169@shovelnose.cs.indiana.edu> X-Authentication-Warning: shovelnose.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Tue, 23 Jun 1998 12:06:22 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.254.191]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA13665 for ; Tue, 23 Jun 1998 12:06:19 -0500 (EST) Received: from postoffice.srv.cs.cmu.edu (POSTOFFICE.SRV.CS.CMU.EDU [128.2.181.62]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with SMTP id MAA14491 for ; Tue, 23 Jun 1998 12:06:18 -0500 (EST) Received: from BANESTO.FOX.CS.CMU.EDU by postoffice.srv.cs.cmu.edu id aa02446; 23 Jun 98 13:05 EDT MMDF-Warning: Parse error in original version of preceding line at postoffice.srv.cs.cmu.edu MMDF-Warning: Parse error in original version of preceding line at postoffice.srv.cs.cmu.edu MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit X-Priority: 3 (Normal) X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook 8.5, Build 4.71.2173.0 Importance: Normal X-MimeOLE: Produced By Microsoft MimeOLE V4.72.2106.4 In-reply-to: <199806201812.NAA23522@shovelnose.cs.indiana.edu> Errors-To: types-errors@cs.indiana.edu From: Robert Harper To: "Gary T. Leavens" , kim@bull.cs.williams.edu Cc: types@cs.indiana.edu Subject: RE: Subject reduction fails in Java - Part 2 Date: Tue, 23 Jun 1998 13:06:28 -0400 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Can this be summarized by saying that a language ought to provide type abstraction mechanisms that allow you to reveal only that a type t is a subtype of another type T in a given context? The presence of such a construct is completely compatible with structural subtyping; it's just that in some contexts we hold a type t (partially) abstract by revealing only that t <: T. In other words: one shouldn't decide as a language design issue that types compare structurally or not, but rather whether the language should support constructs to restrict knowledge about subtyping relationships in certain contexts. Bob Harper -----Original Message----- From: Gary T. Leavens [mailto:leavens@cs.iastate.edu] Sent: Saturday, June 20, 1998 2:07 PM To: kim@bull.cs.williams.edu Cc: types@cs.indiana.edu; leavens@cs.iastate.edu Subject: Re: Subject reduction fails in Java - Part 2 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] Kim Bruce writes: > I'd be interested in hearing if anyone feels there are strong advantages > to "by declaration" subtyping versus structural subtyping. One possible advantage of "by declaration" (or "by name" or "occurrence") subtyping is that the programmer can inform the type system of behavioral subtype relationships. Most type systems do not express information about behavioral specifications, and most langauge implementations, even if they had such information, would not want to do the theorem proving required to prove behavioral subtyping relationships structurally, as that is undecideable in general. (An exception is Abadi and Leino's work [1].) Furthermore, it is useful to have the type system check that only behavioral subtypes are used as subtypes, as that automates part of the verification of OO programs. Moreover, when a language has a declaration that says that a type is a subtype of some other type(s), one can automatically introduce proof obligations for the subtype, or use specification inheritance to force behavioral subtype relationships (as in [2]). If potential supertypes are unknown, then a verification logic has no way to do introduce these proof obligations once and for all, but instead must introduce them at each point of use of one type as a subtype of another (as described above). That said, as a Java programmer, I've often wished for structural subtyping, as it's impossible to provide, for example, a reusable container class that relies on the elements implementing some interface. You simply can't expect that other people would know enough to implement that interface ahead of time. I expect that the same arguments also apply to behavioral subtyping, so it may be, in the end, that we want to make verification logics (like [1]) that do this structurally as well, trading complications in the logic for more reuse. REFERENCES [1] Martin Abadi and Rustan Leino. A Logic of Object-Oriented Programs. In Michel Bidoit and Max Dauchet (eds.), TAPSOFT '97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille, France, pages 682-696. Volume 1214 of Lecture Notes in Computer Science, Springer-Verlag 1997. [2] Krishna Kishore Dhara and Gary T. Leavens. Forcing Behavioral Subtyping Through Specification Inheritance. In Proceedings 18th International Conference on Software Engineering, Berlin, Germany, pages 258-267. IEEE, 1996. An extended and slightly revised version is Department of Computer Science, Iowa State University, TR #95-20c, March 1997. ftp://ftp.cs.iastate.edu/pub/techreports/TR95-20/TR.ps.gz Gary From types-errors@cs.indiana.edu Tue Jun 23 16:12:20 1998 Status: RO X-VM-v5-Data: ([nil nil nil nil nil nil nil nil nil] [nil "Tue" "23" "June" "1998" "11:40:35" "+0200" "Gang CHEN" "Chen.Gang@ens.fr" nil "115" "Subtyping with if" "^From:" nil nil "6" nil "Subtyping with if" nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id QAA20411; Tue, 23 Jun 1998 16:11:02 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA17285 for ; Tue, 23 Jun 1998 12:42:06 -0500 (EST) Received: from cslinux1.cs.indiana.edu (cslinux1.cs.indiana.edu [129.79.244.160]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id MAA15870 for ; Tue, 23 Jun 1998 12:42:06 -0500 (EST) Received: (from pierce@localhost) by cslinux1.cs.indiana.edu (8.8.7/8.8.7) id HAA04288 for types-distrib@cs.indiana.edu; Tue, 23 Jun 1998 07:37:59 -0500 Message-Id: <199806231237.HAA04288@cslinux1.cs.indiana.edu> X-Authentication-Warning: cslinux1.cs.indiana.edu: pierce set sender to types-errors@cs.indiana.edu using -f Delivery-Date: Tue, 23 Jun 1998 04:57:36 -0500 Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by whale.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id EAA13865 for ; Tue, 23 Jun 1998 04:57:34 -0500 (EST) Received: from nef.ens.fr (nef.ens.fr [129.199.96.12]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id EAA18029 for ; Tue, 23 Jun 1998 04:57:32 -0500 (EST) Received: from dmi.ens.fr (dmi.ens.fr [129.199.96.11]) by nef.ens.fr (8.8.7/jtpda-5.1) with ESMTP id LAA01356 for ; Tue, 23 Jun 1998 11:57:01 +0200 (MET DST) Received: from ens.fr (ppp-4.ens.fr [129.199.1.163]) by dmi.ens.fr (8.8.8/jtpda-5.1) with ESMTP id LAA21509 for ; Tue, 23 Jun 1998 11:57:00 +0200 (MET DST) X-Mailer: Mozilla 4.05 [en] (Win95; I) MIME-Version: 1.0 References: <4022.898574038@cslinux1.cs.indiana.edu> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Errors-To: types-errors@cs.indiana.edu From: Gang CHEN To: types@cs.indiana.edu Subject: Subtyping with if Date: Tue, 23 Jun 1998 11:40:35 +0200 [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] 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 CB < C->D A M[x:=N] (tt?M:N) -> M (ff?M:N) -> N From types-errors@cs.indiana.edu Wed Jun 24 01:24:56 1998 Status: RO X-VM-v5-Data: ([nil nil nil nil nil nil t nil nil] [nil "Tue" "23" "June" "1998" "18:31:42" "-0400" "Kim Bruce" "kim@bull.cs.williams.edu" nil "89" "abstraction with subtyping & Overloading considered harmful" "^From:" nil nil "6" nil "abstraction with subtyping & Overloading considered harmful" nil nil nil] nil) Received: from shovelnose.cs.indiana.edu (root@shovelnose.cs.indiana.edu [129.79.244.203]) by amber.ccs.neu.edu (8.8.6/8.8.6) with ESMTP id BAA14448; Wed, 24 Jun 1998 01:24:54 -0400 (EDT) Received: from moose.cs.indiana.edu (root@moose.cs.indiana.edu [129.79.252.123]) by shovelnose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id XAA20362 for ; Tue, 23 Jun 1998 23:09:16 -0500 (EST) Received: from cslinux1.cs.indiana.edu (ppierce.cs.indiana.edu [129.79.240.243]) by moose.cs.indiana.edu (8.8.7/8.8.7/IUCS_2.18) with ESMTP id XAA09127 for ; Tue, 23 Jun 1998 23:09:02 -0500 (EST) Received: (from pierce@localhost) by cslinux1.cs.indiana.edu (8.8.7/8.8.7) id WAA01319 for types-distrib@cs.indiana.edu; Tue, 23 Jun 1998 22:36:14 -0500 Message-Id: <199806240336.WAA01319@cslinux1.cs.indiana.edu> X-Authentication-Warning: cslinux1.cs.india