Re: mutable and polymorphism

[Radu Grigore <radugrigore@gmail.com>]

Thanks Kaustuv! For whoever may bump into this thread, here's a brief
summary that includes info from
  http://scholar.google.com/scholar?cluster=15692213376116771285
  http://scholar.google.com/scholar?cluster=7879701537639090355

Given (let x = e1 in e2), it is not safe to generalize the type
variables for x when e1 has side-effects. After all e1 performs its
side-effects only once, but a polymorphic type on x may let it be used
as if it does them multiple times. For example,
  let x = ref [] in x := ()::!x; 1::!x
would seem to work if you think about it as
  ref []; (ref [] := () :: !(ref []); 1::!(ref []))
and that's exactly how the type system "thinks" about it if it
generalizes types for x. But, of course, that's not the semantics:
only *one* reference is created at runtime.

Some solutions:
1. Never generalize type variables that appear under ref. (OCaml,
before 1995.) Too restrictive.
2. Keep track of side-effects, for example by using type system
with... effects :). (Many people, before 1995.) The problem is that in
interfaces you need to write types, so you'd need to say whether you
implement something using imperative features or not.
3. Only generalize type variables if e1 clearly doesn't have
side-effects because it's not a computation. (Wright 1995, OCaml up to
3.06.)
4. If it's not clear that e1 doesn't have side-effects, you can still
generalize type variables when they appear only in covariant
positions. (Garrigue 2004, OCaml since 3.07.)

So, in my example
  let f = let x = ref () in fun y -> ()
the type checker finds the type '_a->unit for f, but does not
generalize to 'a->unit because '_a in a contravariant position. On the
other hand, in
  let f = let x = ref [] in fun () -> !x
the type is unit->'_a list so it does generalize.

regards,
  radu