generalization in tuples

generalization in tuples

[David Monniaux]

(En français: pourquoi ne pas généraliser le type d'un tuple pour cause de
non-généralisabilité d'une des parties du tuple si de toute façon les
variables de type à généraliser n'y interviennent pas?)

Some typing problem has been bothering me for the week-end.

Let us consider the following code:
# let extractor f = f ~foo:"aaa" ~bar:"bbb";;
val extractor : (foo:string -> bar:string -> 'a) -> 'a = <fun>
# let grostruc = List.map string_of_int [1; 2; 3];;
val grostruc : string list = ["1"; "2"; "3"]
# let zoinx = grostruc, extractor;;
val zoinx : string list * ((foo:string -> bar:string -> 'a) -> 'a) =
  ["1"; "2"; "3"], <fun>

Very logical, and what I wanted: a tuple with some big computed stuff in
the first member and a polymorphic function in the second (this is of
course a simplified example of the actual production code).

Now I do not want to pollute my namespace defining extractor and grostruc,
since all I'm interested in is zoinx.

# let bidule = let extractor f = f ~foo:"aaa" ~bar:"bbb" and grostruc =
List.map string_of_int [1; 2; 3] in grostruc,extractor;;
val bidule : string list * ((foo:string -> bar:string -> '_a) -> '_a) =

The function application in the definition of grostruc prevents 'a from
being generalized. This code is nevertheless equivalent to the precedent
one except from the namespace pollution.

So I actually have two questions:

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 CamlP4-generated
code).

(acceptable kludges include the use of Obj.magic)

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?

David Monniaux            http://www.di.ens.fr/~monniaux
Laboratoire d'informatique de l'École Normale Supérieure,
Paris, France

Re: generalization in tuples

[Didier Remy]

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 CamlP4-generated
> 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 value-only polymorphism
restriction. 

Expressions need to be partitioned into two sets: expansive and
non-expansive expressions, such that the evaluation of non-expansive is
guaranteed not to create any storage. 

For instance, non-expansive expressions may include variables, values (hence
functions), as well as constructors applied to non-expansive expressions.

Note that subexpressions of non-expansive expression are often expansive
(e.g. typically when the expression is under lambda-abstraction).

Given an expression e, we are only interested in outer expansive
sub-expressions of e, i.e. those that are not sub-expressions of a
non-expansive sub-expression 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 sub-expression 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
non-expansive and since variable "'b" only appear in the type of this
non-expansive 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
non-expansive expressions. Hence it is dangerous can cannot be generalized. 

        let x = fun x -> ref x
                 : ('a -> 'a ref)

The expression is protected, i.e. non-expansive 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 non-expansive part of a
let-bound expression, and if not, make its variable non-generalizable.

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
value-only polymorphism restriction.

Re: generalization in tuples

[Didier Remy]

>         let x = (let y = fun x -> x in ref y, y)
>                  : ('a -> 'a) ref * ('a -> 'a)

Indeed, as Michel Mauny pointed out to me, this expression would have type:

          let x = (let y = fun x -> x in ref y, y)
                   : ('a -> 'a) ref * ('b -> 'b)

thus 'b appearing only in a non-expansive expression could be also
generalized here. (BTW, the context "let x = v in [ ]" is non-expansive
whenever v is)

I meant to create the situation where a type variable appears on both
side of a product, when one side is expansive, this other is not, and the
context of the product is non-expansive. But I can't think of a ``natural''
example of this. The usual trick: 

          let x = (fun (y : 'a) -> ref y, y) (fun x -> x)
                   : ('a -> 'a) ref * ('a -> 'a)

does not work, because the whole expression becomes an application and is
expansive. I can only think of using an artifial typing constraint:

          let x = (let y = fun x -> x in ref (y : 'a), (y : 'a))
                   : ('a -> 'a) ref * ('a -> 'a)

> Here 'a appears both in an outer expansive expansive expression and in a
> non-expansive expressions. Hence it is dangerous can cannot be generalized. 

Funny! it is so difficult to stop type generalization...

        Didier