[Prev][Next][Index][Thread]

Polymorphism and side effects



Date: Wed, 5 Oct 88 14:12:00 BST

Having seen my name pop up on the types mailing list, I would like
to point out a couple of properties of the type inference system
I have suggested in my thesis:

(1) Every purely applicative expression typable with Milner polyporphism
    is typable (with the same inference tree) in my system, which I call
    the imperative system. In addition, one can type a  large class
    of programs that use a store. It turns out that the reason
    why Milner's polymorphism does not immediately work for
    programs with side effects is a simple technical point
    regarding capture of type variables that occur free in
    the types of stored values.

(2) I have proved the existence of principal types; the type checker
    is a straightforward extension of Milner's algorithm W, using
    a slightly modified unification algorithm;

(3) The soundness of the imperative inference system has been
    proved using operational semantics and a simple, but powerful
    proof technique concerning maximal fixed points of monotonic
    operators.

(4) The basic ideas have been extended to polymorphic exceptions
    and adopted in the definition of Standard ML.

Of these items, (1)--(3) are documented in my thesis (CST-52-88,
University of Edinburgh, 1987), except the soundness proof of
(2). The details of (4) can be found in ``The Definition of Standard ML,
Version 2,'', (ECS-LFCS-88-62, Dept. of C.S, Edinburgh Univ.).
Moreover, I have just finished writing a paper on polymorphic
references in which I eplain why  Milner's system does 
not generalise without modification in the presence of a store,
present the imperative type discipline and prove it sound.
I will now submit this paper  for publication in ``Information
and Computation''.

Regards, 
  Mads Tofte