On Sat, Jan 2, 2010 at 5:46 PM, Andrej Bauer <andrej.bauer@andrej.com> wrote:
>> on another note (but staying very much on the same topic), why won't the
>> following generalize:
>> # let foo =
>>     let counter  = ref 0 in
>>     let bar = !counter  in
>>     let baz = fun x -> bar
>>     in
>>       baz
>>
>> val foo : '_a -> int = <fun>
>
> It's even worse:
>
>        Objective Caml version 3.11.1
>
> # let _ = ref () in fun x -> x ;;
> - : '_a -> '_a = <fun>
>
> I am sure this makes sense in France. Happy new year!
>
> Andrej

The idea is to prevent potentially wrong programs.
It is bad to write (let x = ref [ ] in x := ["hello"] ; x := [2]).
So the algorithm — that prevents the generalization process of
expressions such as (ref [ ]) — prevents the generalization of all
application expressions. (actually, almost all because I think there
are a few exceptions such as # let f = let x = ref [] in !x ;; val f :
'a list = []).

Making a perfect algorithm that generalizes only and always when
permitted is very hard (maybe it's impossible because not decidable?).

This example shows a program that is rejected because its type is not
computable in Caml's type system :
(fun x -> x x) (fun x -> x) (fun x -> x)
It could be a valid program (i.e. it wouldn't lead to a type crash at
runtime), but it is rejected because the type system is not capable of
asserting its correctness.

(I am not certain I am not off topic)

Cheers,

-- 
Philippe Wang
   mail@philippewang.info