Radu Grigore <radugrigore@gmail.com> writes:

> On Wed, Sep 15, 2010 at 6:40 PM, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
>> Have a look at this variant of c.ml and its "potential" if it type-checked:
>>>  let f = let xs = ref [] in fun x -> xs := x :: !xs in f 1; f 'a'
>
> Interesting. If I would be a type checker, here's what I'd do.
> 1. "ref []" tells me that (xs : '_a), because I know refs can't be polymorphic.
> 2. "x :: !xs" tells me that (xs : '_a list) and (x : '_a)
> 3. "x -> x :: !xs" tells me that (f : '_a -> '_a list)
> 4. "f 1" tells me that (f : int -> int list)
> 5. "f 'a'" tells me... OOPS
>
> Moreover, I'd have similar thoughts about a variant of a.ml (and a.ml
> does typecheck!)
>   let xs = ref [] in let f = fun x -> xs:=x::!xs in f 1; f 'a'

In your original a.ml you didn't use the reference inside f so f was
polymorphic. That is was then further below the scope of a reference
didn't matter since the application of f was too.

> On the other hand, here's what I'd do for the original c.ml, which
> with a few names added is
>   let f = let x = ref () in fun y -> () in f 1; f 'a'
> 1. "ref ()" tells me that (x : unit ref)
> 2. "y -> ()" tells me that (f : 'a -> unit)

2. "y -> ()" tells me that (f : '_a -> unit)

Because the compiler is stupid and things with a ref can't
polymorphic. It isn't smart enough to see that the type of the ref is
independent of the type of the function and there could remain
polymorphic.

> 3. "f 1" returns ()
> 4. "f 'a'" return ()
>
> In other words, I would have thought that in your example the problem
> is that you tried to use a polymorphic reference. (And this problem
> even appears in the FAQ.)

The solution is called lifting I think?

Anyway, you need to move the polymorphic argument outside the scope of
the reference:

let f y = let x = ref () in (fun y -> ()) y in f 1; f 'a'

> regards,
>   radu

MfG
        Goswin