ML with callcc is unsound

To: types
Subject: ML with callcc is unsound
From: Robert.Harper@gottlob.tip.cs.cmu.edu
Date: Mon, 8 Jul 91 16:22:52 EDT
Reply-To: Robert Harper <rwh@proof.ergo.cs.cmu.edu>
Sender: meyer@theory.lcs.mit.edu

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