value restriction

value restriction

[Jacques Le Normand]

[-- Attachment #1: Type: text/plain, Size: 327 bytes --]

Hello caml-list,
with respect to the value restriction, what exactly constitutes a value?
the textbook definition doesn't seem to hold, since the following
generalizes:

let f = let x = 1 in fun g h x -> g (h x);;

while this won't:

let f () = let x = (fun x -> x) (fun x -> x) in fun g h x -> g (h x);;

cheers

--Jacques L.

[-- Attachment #2: Type: text/html, Size: 490 bytes --]

Re: value restriction

[Jacques Le Normand]

[-- Attachment #1: Type: text/plain, Size: 772 bytes --]

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>


baz clearly has a polymorphic type, yet foo doesn't.
Is there any way around this ?

--Jacques L.

On Fri, Jan 1, 2010 at 6:05 PM, Jacques Le Normand <rathereasy@gmail.com>wrote:

> Hello caml-list,
> with respect to the value restriction, what exactly constitutes a value?
> the textbook definition doesn't seem to hold, since the following
> generalizes:
>
> let f = let x = 1 in fun g h x -> g (h x);;
>
> while this won't:
>
> let f () = let x = (fun x -> x) (fun x -> x) in fun g h x -> g (h x);;
>
> cheers
>
> --Jacques L.
>

[-- Attachment #2: Type: text/html, Size: 1370 bytes --]

Re: [Caml-list] Re: value restriction

[Andrej Bauer]

> 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

Re: [Caml-list] Re: value restriction

[Philippe Wang]

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

Re: [Caml-list] Re: value restriction

[Kaustuv Chaudhuri]

On Sat, Jan 2, 2010 at 5:46 PM, Andrej Bauer <andrej.bauer@andrej.com> wrote:
> 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.

I'm not sure why you're singling out France.

% sml
Standard ML of New Jersey v110.69 [built: Sun Jun  7 19:18:24 2009]
- let val _ = ref () in fn x => x end ;
stdIn:1.1-1.36 Warning: type vars not generalized because of
   value restriction are instantiated to dummy types (X1,X2,...)
val it = fn : ?.X1 -> ?.X1

This shouldn't be surprising: a let form is "expansive" and therefore
cannot have a polymorphic type. OCaml is much more liberal than SML
about what forms it considers "non-expansive" [1].

-- Kaustuv

[1] http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf