Browse thread
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: | -- (:) |
| From: | Gilles Dubochet <gilles.dubochet@e...> |
| Subject: | Re: [Caml-list] 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.