[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