generalization in tuples

David Monniaux

Didier Remy
 Didier Remy

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:   (:) 
From:  Didier Remy <Didier.Remy@i...> 
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 nonexpansive expression could be also generalized here. (BTW, the context "let x = v in [ ]" is nonexpansive 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 nonexpansive. 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 > nonexpansive expressions. Hence it is dangerous can cannot be generalized. Funny! it is so difficult to stop type generalization... Didier