From SCPSG@UOTTAWA.BITNET Tue Jul 9 16:31:30 1991 Received: from [137.122.24.39] by csi.UOttawa.CA with SMTP id AA20638 (5.65+/IDA-1.3.5 for holte); Tue, 9 Jul 91 16:25:01 -0400 Received: by UOTTAWA (Mailer R2.07) id 1731; Tue, 09 Jul 91 16:24:32 EDT Resent-Date: Tue, 09 Jul 91 16:24:19 EDT Resent-From: Phil Resent-To: Rob Holte , Luigi Logrippo Received: from MITVMA.MIT.EDU by ACADVM1.UOTTAWA.CA (Mailer R2.07) with BSMTP id 5824; Mon, 08 Jul 91 16:59:54 EDT Received: from MITVMA by MITVMA.MIT.EDU (Mailer R2.05) with BSMTP id 7170; Mon, 08 Jul 91 16:57:30 EDT Received: from theory.lcs.mit.edu by mitvma.mit.edu (IBM VM SMTP R1.2.1MX) with TCP; Mon, 08 Jul 91 16:57:23 EDT Received: from stork (STORK.LCS.MIT.EDU) by theory (4.1/TOC-1.2S) id AA01485; Mon, 8 Jul 91 16:24:25 EDT Received: by stork (4.1/TOC-1.2C) id AA16673; Mon, 8 Jul 91 16:22:52 EDT Date: Mon, 8 Jul 91 16:22:52 EDT Message-Id: <9107082022.AA16673@stork> To: types@theory.lcs.mit.edu Subject: ML with callcc is unsound From: Robert.Harper@GOTTLOB.TIP.CS.CMU.EDU Sender: meyer@theory.lcs.mit.edu Reply-To: Robert Harper Status: R ----------------------------Original message---------------------------- The TYPES forum policy is generally not to forward messages from other bboards. The message below seems to merit an exception to the general rule. Yours truly, Albert R. Meyer Moderator, types@theory.lcs.mit.edu ---------- To: sml-list@cs.cmu.edu Date: Mon, 08 Jul 91 12:38:25 EDT The Standard ML of New Jersey implementation of callcc is not type safe, as the following counterexample illustrates: fun left (x,y) = x; fun right (x,y) = y; let val later = (callcc (fn k => ( fn x => x, fn f => throw k (f, fn f => ()) ) )) in print (left(later)"hello world]\n"); right(later)(fn x => x+2) end (Running this example causes the NJ compiler to fail in unpleasant ways.) This example illustrates that the ML core language with polymorphism plus callcc with the typing rules: callcc : ('a cont -> 'a) -> 'a throw : 'a cont -> 'a -> 'b is unsound. Making callcc weakly polymorphic, callcc : ('1a cont -> '1a) -> '1a rules out the counterexample, and we conjecture that the resulting system is sound, but we currently have no proof of this. These results do not contradict those of the 1991 POPL paper by Duba, Harper, and MacQueen since the only soundness claim made there is for monomorphic ML with callcc. The counterexample was generated by considering the extension of the cps transform methods considered there to polymorphism. The counterexample does contradict a claim by Felleisen and Wright to the effect that the type system is sound; it is my understanding that they have repaired the proof by restricting the language. The restriction to weak polymorphism, if it is correct, is unsatisfactory, both because weak type variables are in general unsatisfactory, and because callcc, in contrast to ref's and exceptions, is unrelated to references. This suggests that there is a more general problem with the ML type system. We are currently developing an analysis of the problem, and an alternative to weak type variables, and hope to comment usefully on this subject in the near future. - Bob Harper Mark Lillibridge