Polymorphic variant typing
[
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:  20050215 (23:15) 
From:  Gilles Dubochet <gilles.dubochet@e...> 
Subject:  Re: [Camllist] Polymorphic variant typing 
>> let incr g x = match x with >>  `Int i > `Int (i+1) >>  x > (g x);; >> Receives type: >> (([> `Int of int ] as 'a) > ([> `Int of int ] as 'b)) > 'a > 'b > > Now, how about this : > > let incr x g = match x with >  `Int i > `Int (i+1) >  x > g x;; > > Doesn't it look like your code ? OCaml 3.08.2 types it as follows : > val incr : ([> `Int of int ] as 'a) > ('a > ([> `Int of int ] as > 'b)) > 'b = <fun> > > This is more like it ! I am afraid I can't agree with you: As far as I can tell, this type with the 'x g' version is exactly equivalent to the type I obtained with the 'g x' version. If you remember that "... as 'a" is the binding of a type variable, it is quite intuitive why. > incr (`Int 1) (fun (`Int i) > (`Int (i+1)));; >  : [> `Int of int ] = `Int 2 > incr (`Float 1.0) (fun x > match x with (`Float f) > (`Float (f +. > 1.0))  x > x);; >  : [> `Float of float  `Int of int ] = `Float 2. Yes, but in your case the g function you pass as a parameter has a last generic case. This means it has type "([> `Float of float ] as 'a) > 'a" which is an "at least" instead of a "at most" variant type. With that function it works also with my original 'g x' version. The goal is to be able to make this run: incr (`Float 1.0) (fun x > match x with (`Float f) > (`Float (f +. 1.0)));; And your solution doesn't more than mine. Just to make things clear, I am not looking for a workaround to this problem. I am rather looking for an explanation about why the mentioned type is inferred for this expression. I am developing a type inference system for a language with similar variants to O'Caml's polymorphic variants. My inference algorithm calculates a different type than O'Caml's for a equivalent expression. I try to understand why O'Caml does it that way to decide how I should do it. To make it even more clear, the type I obtain with my algorithm is (in row variable notation): (['a] > [#int:int  'b]) > [#int:int  'a] > [#int:int  'b] Voilà, but thanks for the answer anyway, Cheers, Gilles.