polymorphic variants and promotion

polymorphic variants and promotion

[Johannes Kanig]

[-- Attachment #1: Type: text/plain, Size: 1547 bytes --]

Hi,

I ran into the following problem using polymorphic variants. Suppose I have
2 functions f and g (the function definitions don't make much sense - they
are just there for typing purposes) :

# let f (`A a) (`A i) = `A i ;;
val f : [< `A of 'a ] -> [< `A of 'b ] -> [> `A of 'b ] = <fun>
# let g (`A a) = (`B a) ;;
val g : [< `A of 'a ] -> [> `B of 'a ] = <fun>

For simplicity I assume that the type variables all instantiate to "int".
Now, I want to construct a function h that takes an accumulator a and a list
of `A's (for example [`A 1; `A 2; ...]) that produces either an object of
type `A of int or an object of type `B of int in the following way:

# let h a = function
    | [] -> g a
    | xs -> List.fold_left f a xs;;

But this doesn't type:

This expression has type [ `A of 'a ] but is here used with type
  [> `B of 'a ]
The first variant type does not allow tag(s) `B

I understand that the fold_left fixes the type of f the result of f to [`A
of int] instead of [>`A of int]. The example as above can be easily repaired
by replacing the second branch of the pattern matching by:

let `A _ as x = List.fold_left f a xs in x

which is fair enough (thanks to Romain Bardou for pointing this out).

What I don't understand is why the promotion of [`A of int] to [> `A of int]
is not possible in general:

# `A 1;;
- : [> `A of int ] = `A 1
# (`A 1 : [`A of int]) ;;
- : [ `A of int ] = `A 1
# ((`A 1 : [`A of int]) : [> `A of int]) ;;
- : [ `A of int ] = `A 1

Does anyone have an answer?

-- 
Johannes Kanig
johannes.kanig@lri.fr

[-- Attachment #2: Type: text/html, Size: 1874 bytes --]

Re: [Caml-list] polymorphic variants and promotion

[Julien Signoles]

Hello Johannes,

> What I don't understand is why the promotion of [`A of int] to [> `A of int]
> is not possible in general:
>
> # `A 1;;
> - : [> `A of int ] = `A 1
> # (`A 1 : [`A of int]) ;;
> - : [ `A of int ] = `A 1
> # ((`A 1 : [`A of int]) : [> `A of int]) ;;
> - : [ `A of int ] = `A 1
>
> Does anyone have an answer?

You have to use coercion in order to promote:
# (`A 1 : [ `A of int ] :> [> `A of int ]);;
- : [> `A of int ] = `A 1

--
Julien

Re: [Caml-list] polymorphic variants and promotion

[Keiko Nakata]

Hello,

indeed we need to use double coercion, instead of single:

# ((`A 1 : [ `A of int ]) : [ `A of int ] :> [> `A of int ]);;
- : [> `A of int ] = `A 1
# ((`A 1 : [ `A of int ]) :> [> `A of int ]);;
- : [ `A of int ] = `A 1

This explains a little to me about the differences 
between double and single coercions.
Thanks. 

With best,
Keiko

Re: [Caml-list] polymorphic variants and promotion

[Christophe Raffalli]

Keiko Nakata a écrit :
> Hello,
>
> indeed we need to use double coercion, instead of single:
>
> # ((`A 1 : [ `A of int ]) : [ `A of int ] :> [> `A of int ]);;
> - : [> `A of int ] = `A 1
> # ((`A 1 : [ `A of int ]) :> [> `A of int ]);;
> - : [ `A of int ] = `A 1
>
>   
To me this looks like a bug ? Should not we always have that "e :> t" 
has type "t" (if it typechecks) ?

Cheers,
Christohe
> This explains a little to me about the differences 
> between double and single coercions.
> Thanks. 
>
> With best,
> Keiko
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>   

Re: [Caml-list] polymorphic variants and promotion

[Jacques Garrigue]

From: Christophe Raffalli <christophe.raffalli@univ-savoie.fr>
> Keiko Nakata a écrit :
> > indeed we need to use double coercion, instead of single:
> >
> > # ((`A 1 : [ `A of int ]) : [ `A of int ] :> [> `A of int ]);;
> > - : [> `A of int ] = `A 1
> > # ((`A 1 : [ `A of int ]) :> [> `A of int ]);;
> > - : [ `A of int ] = `A 1
> >
> >   
> To me this looks like a bug ? Should not we always have that "e :> t" 
> has type "t" (if it typechecks) ?

No, it should have type "an instance of t", like for all type
annotations in ocaml. And [`A of int] happens to be an instance of
[> `A of int].

Jacques Garrigue

Re: polymorphic variants and promotion

[Remi Vanicat]

"Johannes Kanig" <johannes.kanig@lri.fr> writes:

> Hi,
>
> I ran into the following problem using polymorphic variants. Suppose I have
> 2 functions f and g (the function definitions don't make much sense - they
> are just there for typing purposes) :
>
> # let f (`A a) (`A i) = `A i ;;
> val f : [< `A of 'a ] -> [< `A of 'b ] -> [> `A of 'b ] = <fun>
> # let g (`A a) = (`B a) ;;
> val g : [< `A of 'a ] -> [> `B of 'a ] = <fun>
>
> For simplicity I assume that the type variables all instantiate to "int".
> Now, I want to construct a function h that takes an accumulator a and a list
> of `A's (for example [`A 1; `A 2; ...]) that produces either an object of
> type `A of int or an object of type `B of int in the following way:
>
> # let h a = function
>     | [] -> g a
>     | xs -> List.fold_left f a xs;;
>
> But this doesn't type:
>
> This expression has type [ `A of 'a ] but is here used with type
>   [> `B of 'a ]
> The first variant type does not allow tag(s) `B

Well, you have to explicitly coerce :

let h a = function                                              
      | [] -> g a                                                 
      | xs -> (List.fold_left f a xs : [ `A of _ ] :> [> `A of _ | `B of _ ]) ;;

What I don't understand is why this :

let h a = function                                              
      | [] -> g a                                                 
      | xs -> (List.fold_left f a xs :> [> `A of _ | `B of _ ]) ;;

do not work ? I understood that we need to explicitly coerce, but the 
[ `A of _ ] is just the information the compiler will find by itself,
why must we give it to it again ?

-- 
Rémi Vanicat

Re: [Caml-list] Re: polymorphic variants and promotion

[Jacques Garrigue]

From: Remi Vanicat <vanicat@debian.org>
> Well, you have to explicitly coerce :
> 
> let h a = function                                              
>       | [] -> g a                                                 
>       | xs -> (List.fold_left f a xs : [ `A of _ ] :> [> `A of _ | `B of _ ]) ;;
> 
> What I don't understand is why this :
> 
> let h a = function                                              
>       | [] -> g a                                                 
>       | xs -> (List.fold_left f a xs :> [> `A of _ | `B of _ ]) ;;
> 
> do not work ? I understood that we need to explicitly coerce, but the 
> [ `A of _ ] is just the information the compiler will find by itself,
> why must we give it to it again ?

Because we cannot always be sure that the compiler will infer it at
the right time. I.e., we would end up with some programs having
different typing behaviours when the above application is inferred as
[`A of _] and when a less precise type is inferred, which could cause
unification errors somewhere else...

We are currently considering allowing the above kind of abbreviation
when both the source and target are ground types (i.e. do not contain
type variables). But this would not include the above example.

Jacques Garrigue