This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

generalization in tuples
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2000-10-18 (08:36) From: Didier Remy Subject: Re: generalization in tuples
```>         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

```