From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id CAB46BC58 for ; Fri, 17 Sep 2010 16:04:01 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Am8BAKYSk0zRVdc0kGdsb2JhbACDG5EZjWcIFQEBAQEJCQwHEQMfp1yJADyCFIZ6LYhVAQEDBYEdgytzBIoz X-IronPort-AV: E=Sophos;i="4.56,383,1280700000"; d="scan'208";a="59448198" Received: from mail-ew0-f52.google.com ([209.85.215.52]) by mail2-smtp-roc.national.inria.fr with ESMTP; 17 Sep 2010 16:04:01 +0200 Received: by ewy20 with SMTP id 20so1365307ewy.39 for ; Fri, 17 Sep 2010 07:04:01 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:received:received:in-reply-to :references:date:message-id:subject:from:to:content-type; bh=8O53CQu8ltTPShsUtU5P6boj8hQq7vwrbGQ4PXP4KQU=; b=AaMFVZj7j6ICiJfpTt2M4suuqs55PLmNKZGXeCHabFdXcyxfFqH44qHQiKGqjv3AIJ 54lPlKuSqpfCyixeFWK9rZR/8EzoRG1yh+45lg4NerM6xJ622CpOdqeNCc8KvxfZzOZV o8jxjG36pqJkIjAsVu/DT7yKHXukVnVtOz4dM= 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 :content-type; b=d/ex3zj8aELz2p3cDdJ9/fCP+8m/wZeBIp8MBQM2cGmquPL6hW3BRD7nz/tVsk20ri Bx5Lz9bjrj6trc4UllwCRFqiIYCWCp8eWEUb+eC8iFDZLccE49OaB2wZ1T1S+uRXmASy Aeu5d9hWtdrqxrBvbMDDDAeNYUUsLI+vpQtF4= MIME-Version: 1.0 Received: by 10.213.2.139 with SMTP id 11mr6099388ebj.81.1284732241248; Fri, 17 Sep 2010 07:04:01 -0700 (PDT) Received: by 10.14.18.148 with HTTP; Fri, 17 Sep 2010 07:04:00 -0700 (PDT) In-Reply-To: References: Date: Fri, 17 Sep 2010 15:04:00 +0100 Message-ID: Subject: Re: mutable and polymorphism From: Radu Grigore To: caml-list@yquem.inria.fr Content-Type: text/plain; charset=UTF-8 X-Spam: no; 0.00; mutable:01 polymorphism:01 semantics:01 runtime:01 ocaml:01 restrictive:01 ocaml:01 checker:01 'a-:01 unit-:01 polymorphic:01 computation:01 imperative:01 interfaces:01 covariant:02 Thanks Kaustuv! For whoever may bump into this thread, here's a brief summary that includes info from http://scholar.google.com/scholar?cluster=15692213376116771285 http://scholar.google.com/scholar?cluster=7879701537639090355 Given (let x = e1 in e2), it is not safe to generalize the type variables for x when e1 has side-effects. After all e1 performs its side-effects only once, but a polymorphic type on x may let it be used as if it does them multiple times. For example, let x = ref [] in x := ()::!x; 1::!x would seem to work if you think about it as ref []; (ref [] := () :: !(ref []); 1::!(ref [])) and that's exactly how the type system "thinks" about it if it generalizes types for x. But, of course, that's not the semantics: only *one* reference is created at runtime. Some solutions: 1. Never generalize type variables that appear under ref. (OCaml, before 1995.) Too restrictive. 2. Keep track of side-effects, for example by using type system with... effects :). (Many people, before 1995.) The problem is that in interfaces you need to write types, so you'd need to say whether you implement something using imperative features or not. 3. Only generalize type variables if e1 clearly doesn't have side-effects because it's not a computation. (Wright 1995, OCaml up to 3.06.) 4. If it's not clear that e1 doesn't have side-effects, you can still generalize type variables when they appear only in covariant positions. (Garrigue 2004, OCaml since 3.07.) So, in my example let f = let x = ref () in fun y -> () the type checker finds the type '_a->unit for f, but does not generalize to 'a->unit because '_a in a contravariant position. On the other hand, in let f = let x = ref [] in fun () -> !x the type is unit->'_a list so it does generalize. regards, radu