From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 64E77BC37 for ; Sun, 3 Jan 2010 00:09:51 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtoCAFJhP0vRVdzjkWdsb2JhbACCNY8KiUc/AQEBAQkLCgcTA6k/gTKDfIY1AQIDBYQsBA X-IronPort-AV: E=Sophos;i="4.47,490,1257116400"; d="scan'208";a="40898200" Received: from mail-fx0-f227.google.com ([209.85.220.227]) by mail3-smtp-sop.national.inria.fr with ESMTP; 03 Jan 2010 00:09:50 +0100 Received: by fxm27 with SMTP id 27so13260719fxm.3 for ; Sat, 02 Jan 2010 15:09:50 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:received:in-reply-to:references :date:message-id:subject:from:to:cc:content-type :content-transfer-encoding; bh=5+MV1ul+HTZ4+S1fGAwlGsJ8kxDUXofL4stgfV0LlXM=; b=gBYioM6y9eU8MbV1jxyZY9EV6kSyqqz+xa/U7floxziRkGnEhkpS4mb40YpABh8PTa 4iVQhfr4CfPIQv2nF9Di3q1hktfe0XxtajA6NJvNrWcjOJyIvxICm3QC1e7AEamJ1cIx JSdzo1bs0BlokqmoRbxG1TxyayaCtMC1ODHg8= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=kWcn4QmaK5et0oUp99DyTATlbdn3cun9L31PdbJ7VGLZ1gweqkGBd5sDsqUtdD4L/y 51w35TO/RJUMZrSUAzfxTaO+bpAzzzzJfXGpr0oHvZ8aJWA0yK2hbJzR0T+DtwYEZCCt LObjGGKDOOS9Ug3GNzGNdrBrVjQzs2SLBvI+I= MIME-Version: 1.0 Received: by 10.239.193.83 with SMTP id h19mr151977hbi.117.1262473790300; Sat, 02 Jan 2010 15:09:50 -0800 (PST) In-Reply-To: <7d8707de1001020846s29332a67j21878751ed3da22@mail.gmail.com> References: <7d8707de1001020846s29332a67j21878751ed3da22@mail.gmail.com> Date: Sun, 3 Jan 2010 00:09:50 +0100 Message-ID: <4d1b2df21001021509n70a98f23yf444f2e358276a69@mail.gmail.com> Subject: Re: [Caml-list] Re: value restriction From: Philippe Wang To: Andrej Bauer Cc: Jacques Le Normand , caml-list caml-list Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; andrej:01 andrej:01 foo:01 baz:01 baz:01 val:01 foo:01 val:01 decidable:01 caml's:01 runtime:01 cheers:01 wrote:01 caml-list:01 exceptions:01 On Sat, Jan 2, 2010 at 5:46 PM, Andrej Bauer wrot= e: >> on another note (but staying very much on the same topic), why won't the >> following generalize: >> # let foo =3D >> =A0=A0 =A0let counter =A0=3D ref 0 in >> =A0=A0 =A0let bar =3D !counter =A0in >> =A0=A0 =A0let baz =3D fun x -> bar >> =A0=A0 =A0in >> =A0=A0 =A0 =A0baz >> >> val foo : '_a -> int =3D > > It's even worse: > > =A0 =A0 =A0 =A0Objective Caml version 3.11.1 > > # let _ =3D ref () in fun x -> x ;; > - : '_a -> '_a =3D > > 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 =3D ref [ ] in x :=3D ["hello"] ; x :=3D [2]). So the algorithm =97 that prevents the generalization process of expressions such as (ref [ ]) =97 prevents the generalization of all application expressions. (actually, almost all because I think there are a few exceptions such as # let f =3D let x =3D ref [] in !x ;; val f : 'a list =3D []). 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, --=20 Philippe Wang mail@philippewang.info