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

value restriction

[Jacques Carette]

I am wondering if there is a (nice) way around the value restriction in 
a particular case we have encountered.
Inside a Functor, we compute a value as

let make_result =
	match IF.R.fin with
	| Some rank_action ->
	function m -> perform
		      rank <-- rank_action ();
		      ret (Tuple.tup2 m.matrix rank)
        | None -> failwith "Rank is not computed here"

(where the above uses the campl4 extension for monadic notation).
By design, we _want_ the failure to happen at Functor instantiation time 
(if it will fail), so the usual 'fix' of having make_result () does not 
help.
But the code above does not work because of the value restriction :-(

Instead, we currently resort to

let make_result m = perform
    rank <-- fromJust IF.R.fin ();
    ret (Tuple.tup2 m.matrix rank)
(* Initialization: check the preconditions of instantiation of this struct*)
let () = notNone IF.R.fin "Rank is not computed here"

where
let fromJust = function Some x -> x | None -> failwith "Can't happen"
let notNone v str = match v with None -> failwith str | Some _ -> ()

which is clearly very ugly.  So ugly that when 'Obj.magic' came up as a 
possibility around this, it was not immediately rejected.  Yes, that ugly.

The one possibility we have considered is to make IF.R.fin of type  unit 
-> 'a monad (no option) and instead of having None, we'd have
    fin () = failwith "Rank is not computed"

Then we would have to do

let make_result m = perform
    rank <-- IF.R.fin ();
    ret (Tuple.tup2 m.matrix rank)
(* Initialization: check the preconditions of instantiation of this struct*)
let _ = IF.R.fin ()

That would invoke IF.R.fin speculatively, and if that works, then invoke 
it 'for real' (but monadically the second time) later, when we know it 
will work.  That certainly works, and has a certain appeal.  And yet...

Jacques