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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id DE195BC58 for ; Wed, 15 Sep 2010 22:44:46 +0200 (CEST) X-IronPort-AV: E=Sophos;i="4.56,372,1280700000"; d="scan'208";a="69590092" Received: from mail-qw0-f52.google.com ([209.85.216.52]) by mail4-relais-sop.national.inria.fr with ESMTP/TLS/RC4-MD5; 15 Sep 2010 22:44:46 +0200 Received: by qwf6 with SMTP id 6so607034qwf.39 for ; Wed, 15 Sep 2010 13:44:44 -0700 (PDT) MIME-Version: 1.0 Received: by 10.229.189.195 with SMTP id df3mr1529974qcb.143.1284583479070; Wed, 15 Sep 2010 13:44:39 -0700 (PDT) Received: by 10.229.85.196 with HTTP; Wed, 15 Sep 2010 13:44:39 -0700 (PDT) In-Reply-To: References: <878w32g6wh.fsf@frosties.localdomain> Date: Wed, 15 Sep 2010 22:44:39 +0200 Message-ID: Subject: Re: [Caml-list] mutable and polymorphism From: Kaustuv Chaudhuri To: caml-list Content-Type: text/plain; charset=UTF-8 X-Spam: no; 0.00; mutable:01 polymorphism:01 polymorphism:01 reasoned:01 constructors:01 constructors:01 mutable:01 ocaml:01 ocaml's:01 ocaml:01 mutation:01 val:01 04.:98 equality:01 polymorphic:01 On Wed, Sep 15, 2010 at 9:38 PM, Radu Grigore wrote: > In any case, I'm more interested in an explanation of what happens, As you are probably aware, ML-style languages have a so-called "value restriction" on polymorphism, which in its most vanilla form can be stated simply as: only values can have a polymorphic type. The expression let x = e in fun y -> () (1) is not a value, meaning that it can reduce further, and therefore the vanilla value restriction says that it cannot have a polymorphic type. Now, some very clever people have reasoned that in certain cases the expression (1) is indistinguishable from a value and by Leibniz's principle of equality of indistinguishables should therefore be allowed to have the polymorphic type its equivalent value does. As an example, one such situation is if e is built from only pure constructors (i.e., constructors with no mutable fields) and values, such as: let x = () in fun y -> () One might even say that (1) should be treated as a value when it is equivalent to the value expression: fun y -> let x = e in () There are a number of scenarios in which OCaml can deduce that a certain non-value expression can have a polymorphic type. For a comprehensive list of such situations, you can read Jacques Garrigue's paper on this topic, which also has a great section on the history of the value restriction [1]. However, OCaml's implementation is conservative -- it doesn't cover all cases where this fun/let permutation doesn't change the denotation. You can easily discover that one kind of expression that OCaml doesn't allow for this "value-interpretation" of (1) is if e is a function application. After all, this expression let x = infinite_loop () in fun y -> () and this: fun y -> let x = infinite_loop () in () are easily distinguished. That your function is called "ref" instead of "infinite_loop" is irrelevant. Mutation is a red herring. You would get the same result for a completely pure expressions for e; for example: # let z = let x = fst (1, 2) in fun y -> () ;; val z : '_a -> unit = -- Kaustuv [1] http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.ps.gz