Browse thread
value restriction
-
Jacques Le Normand
-
Jacques Le Normand
-
Andrej Bauer
- Philippe Wang
- Kaustuv Chaudhuri
-
Andrej Bauer
-
Jacques Le Normand
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2010-01-02 (23:09) |
From: | Philippe Wang <philippe.wang.lists@g...> |
Subject: | Re: [Caml-list] Re: value restriction |
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