Polymorphic variant typing

Polymorphic variant typing

[Gilles Dubochet]

Hello everyone,

The following O'Caml expression:
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

Why? I am quite astonished. I would have expected a type more like:
([> ] -> [> ]) -> [> `Int of int ] -> [> `Int of int ]

or in Wand or Rémy-like row variable notation with which I am a little 
more comfortable (I am not exactly sure the preceding type is correct 
in the 'at leat - at most' notation of O'Caml):
([ 'a ] -> [ 'b ]) -> [ `Int of int | 'a ] -> [ `Int of int | 'b ]

Could anyone be kind enough to give me some clues about where to look 
at to find an explanation or even better, explain me what is going on? 
I am particularly puzzled by the fact that the g function's *argument* 
type is 'at least `Int of int'. This rejects the following code which 
seems intuitively correct:
incr (function `Float f -> `Float (f+.1.));;

Thank you.
Cheers,
Gilles.

Re: [Caml-list] Polymorphic variant typing

[Olivier Pérès]

Gilles Dubochet a écrit :

> 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 !

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.

    It remains to understand why the type of incr should depend upon the 
order in which the arguments are given...

    Yours,

    Olivier.

Re: [Caml-list] Polymorphic variant typing

[Gilles Dubochet]

>> 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.

Re: [Caml-list] Polymorphic variant typing

[Jacques Garrigue]

From: Gilles Dubochet <dubochet@urbanet.ch>

> The following O'Caml expression:
> 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
> 
> Why? I am quite astonished. I would have expected a type more like:
> ([> ] -> [> ]) -> [> `Int of int ] -> [> `Int of int ]
> 
> or in Wand or Rémy-like row variable notation with which I am a little 
> more comfortable (I am not exactly sure the preceding type is correct 
> in the 'at leat - at most' notation of O'Caml):
> ([ 'a ] -> [ 'b ]) -> [ `Int of int | 'a ] -> [ `Int of int | 'b ]

The reason is simple enough: variants in ocaml are not based on Remy's
rows, but on a type system with kinded variables, more in Ohori's style.
This is described in detail in "Simple type inference for structural
polymorphism", which you can find at
  http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/

The main reason for this choice is avoiding making rows explicit,
i.e. having a multi-sorted type algebra. Note also that ocaml object
types, while originally based on Remy's system, are hiding their
row-variables, and can be described in the same formalism.

> Could anyone be kind enough to give me some clues about where to look 
> at to find an explanation or even better, explain me what is going on? 
> I am particularly puzzled by the fact that the g function's *argument* 
> type is 'at least `Int of int'. This rejects the following code which 
> seems intuitively correct:
> incr (function `Float f -> `Float (f+.1.));;

Pragmatic reasons for this choice are given in Section 3 of
  "Typing deep pattern-matching in presence of polymorphic variants"
which you can find at the same place.

Cheers,

Jacques Garrigue

Re: [Caml-list] Polymorphic variant typing

[Gilles Dubochet]

Thanks: that was exactly what I was looking for.

> The reason is simple enough: variants in ocaml are not based on Remy's
> rows, but on a type system with kinded variables, more in Ohori's 
> style.
> This is described in detail in "Simple type inference for structural
> polymorphism", which you can find at
>   http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/
>
> The main reason for this choice is avoiding making rows explicit,
> i.e. having a multi-sorted type algebra. Note also that ocaml object
> types, while originally based on Remy's system, are hiding their
> row-variables, and can be described in the same formalism.
Just to make it crystal clear for me: You say that the "main reason for 
this choice is avoiding making rows explicit", does this mean that the 
O'Caml team feels that row-based type information is too complicated 
for an average user since you either steer away of hide it in an object 
model?

> Pragmatic reasons for this choice are given in Section 3 of
>   "Typing deep pattern-matching in presence of polymorphic variants"
> which you can find at the same place.

Sincerely,
Gilles Dubochet.

Re: [Caml-list] Polymorphic variant typing

[Jacques Garrigue]

From: Gilles Dubochet <dubochet@urbanet.ch>
> > The main reason for this choice is avoiding making rows explicit,
> > i.e. having a multi-sorted type algebra. Note also that ocaml object
> > types, while originally based on Remy's system, are hiding their
> > row-variables, and can be described in the same formalism.

> Just to make it crystal clear for me: You say that the "main reason for 
> this choice is avoiding making rows explicit", does this mean that the 
> O'Caml team feels that row-based type information is too complicated 
> for an average user since you either steer away of hide it in an object 
> model?

Basically yes. Hence the clever tricks to have types containing hidden
row variables, like #t, [< t], [> t]. Having explicit row variables
was considered at some point, but it was not done because types would
become much more verbose. Consider for instance that with variants,
presence/absence information is needed for each tag.

On the other hand, advanced features like explicit polymorphism require
some understanding of the presence of hidden variables, and how they
interact, so at that level of proficiency it's not clear whether
hiding them really helps. And I'm now playing with abstract rows,
which makes the decision even less clear...

Jacques Garrigue

Re: [Caml-list] Polymorphic variant typing

[Radu Grigore]

On Wed, 16 Feb 2005 15:40:22 +0900 (JST), Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> From: Gilles Dubochet <dubochet@urbanet.ch>
> > Just to make it crystal clear for me: You say that the "main reason for
> > this choice is avoiding making rows explicit", does this mean that the
> > O'Caml team feels that row-based type information is too complicated
> > for an average user since you either steer away of hide it in an object
> > model?
> 
> Basically yes. Hence the clever tricks to have types containing hidden
> row variables, like #t, [< t], [> t]. [...]

Perspective from an ocaml beginner & someone who doesn't know about
row variables (that would be me): the [> t] and [< t] notations seem
very intuitive. However, now that I know they hide something, I'd like
to know what (and I'll have to rely on google instead of the ocaml
compiler for that).

-- 
regards,
 radu
http://rgrig.idilis.ro/

Re: [Caml-list] Polymorphic variant typing

[David Brown]

On Tue, Feb 15, 2005 at 09:28:52PM +0000, Gilles Dubochet wrote:
> Hello everyone,
> 
> The following O'Caml expression:
> 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
> 
> Why? I am quite astonished. I would have expected a type more like:
> ([> ] -> [> ]) -> [> `Int of int ] -> [> `Int of int ]
>
> or in Wand or Rémy-like row variable notation with which I am a little 
> more comfortable (I am not exactly sure the preceding type is correct 
> in the 'at leat - at most' notation of O'Caml):
> ([ 'a ] -> [ 'b ]) -> [ `Int of int | 'a ] -> [ `Int of int | 'b ]
> 
> Could anyone be kind enough to give me some clues about where to look 
> at to find an explanation or even better, explain me what is going on? 
> I am particularly puzzled by the fact that the g function's *argument* 
> type is 'at least `Int of int'. This rejects the following code which 
> seems intuitively correct:
> incr (function `Float f -> `Float (f+.1.));;

We know that 'incr' can take a [> `Int of int] for 'x', since it matches
is.  The only way to know that it isn't going to call 'g' with one of these
would be to do a flow analysis of the code.  The type system is not based
on this type of analysis, but is determined statically.

The polymorphic types are not really dynamic types.  A particular type used
in a given call will have a specific type, and in this instance, it must
always contain [> `Int of int].

Dave