generalization in tuples

David Monniaux
 Didier Remy
[
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:  20001017 (15:58) 
From:  Didier Remy <Didier.Remy@i...> 
Subject:  Re: generalization in tuples 
On Mon, Oct 16, 2000 at 02:42:11PM +0200, David Monniaux wrote: > 1/ Is it possible to do what I want to do, even if it means using a > kludge? The above code, using multiple let's, is not good: it's not > useable in the middle of an expression (this is for CamlP4generated > code). > > (acceptable kludges include the use of Obj.magic) In principle, Obj.magic should do the job, but it does not: Obj.magic (fun x > x) is treated as an application and returns a weak type ;( The problem is that "Obj.magic" is defined as a primitive and the above is typed as any other application, but I don't see any reason except technical to treat Obj.magic as a constructor. Anyway, I don't think Obj.magic is a good fix... > 2/ Is there a finer notion of a "generalizable" expression that > encompasses the above code, and could the "let generalization" procedure > in the compiler be improved so that the above code gets a polymorphic > type? Yes, there is a very simple generalization of the valueonly polymorphism restriction. Expressions need to be partitioned into two sets: expansive and nonexpansive expressions, such that the evaluation of nonexpansive is guaranteed not to create any storage. For instance, nonexpansive expressions may include variables, values (hence functions), as well as constructors applied to nonexpansive expressions. Note that subexpressions of nonexpansive expression are often expansive (e.g. typically when the expression is under lambdaabstraction). Given an expression e, we are only interested in outer expansive subexpressions of e, i.e. those that are not subexpressions of a nonexpansive subexpression of e (in which case, they are protected from evaluation). When typing an expression e, all type variables appearing in at least one outer expansive subexpression of e may also be the type of a store cell allocation and should not be generalized. All other type variables can be generalized. For instance, in (a simpler version of) your example: let x = (ref [], fun x > x);; The expression (ref [], fun x > x) has type 'a ref * ('b > 'b); here, "ref []" is an application, hence an (outer) expansive expression and 'a appearing in its type cannot be generalized. Conversely, "fun x > x" is nonexpansive and since variable "'b" only appear in the type of this nonexpansive subexpression, it can be generalized. A few more examples:  let x = (let y = fun x > x in ref y, y) : ('a > 'a) ref * ('a > 'a) Here 'a appears both in an outer expansive expansive expression and in a nonexpansive expressions. Hence it is dangerous can cannot be generalized. let x = fun x > ref x : ('a > 'a ref) The expression is protected, i.e. nonexpansive and "'a" can be generalized. (Note that this is a strict generalization of the actual solution.() The implementation  This is actually quite simple: while typeckecking an expression, just keep track of whether the expression is the outermost nonexpansive part of a letbound expression, and if not, make its variable nongeneralizable. In fact, I experimented this in MLART a while ago: #morgon:~/caml/camlart/src$ ./camlrun ./camltop I lib > Caml Light version 0.5 (modified with extensible records) #(ref 1, fun x > x);;  : int ref * ('a > 'a) = ref 1, <fun> or, using extensible records :) #{!a = fun x > x};; > Toplevel input: >{!a = fun x > x};; >^^^^^^^^^^^^^^^^^^^ > Cannot generalize 'a in {a : mut. 'a > 'a; abs. 'b} #{!a =1; b = fun x > x};;  : {a : mut. int; b : pre. 'a > 'a; abs. 'b} = {!a = 1; b = <fun>} # Didier PS: This has never been implemented in Ocaml, probably because, besides me, you are one of first persons to complain about the drastic implementation of valueonly polymorphism restriction.