[Caml-list] This ground coercion is not principal?

[Caml-list] This ground coercion is not principal?

[bob zhang]

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

Hi List,
  I have came across a corner case in ocaml typing here,
The source code is pasted below(extracted from a large code base), it
triggers the warning 18.
My question, is there any elegant solution without introducing local types?

------------------------------------------------------------------------------------------
type ant = [`Ant of string]
type 'a mlist =
    [ `LNil
    | `LCons of ('a * 'a mlist )
    | ant]
let a = object(self)
  method ant : ant -> ant=
    fun (`Ant a)  ->
      `Ant a
  method mlist: 'all_a0 'all_b0 .
      ('self_type -> 'all_a0 -> 'all_b0) ->
        'all_a0 mlist -> 'all_b0 mlist=
          fun (type t) mf_a  ->
            function
              | `LNil ->  `LNil
              | `LCons (a0,a1) ->
                  let a0 = mf_a self a0 in
                  let a1 = self#mlist mf_a a1 in `LCons (a0, a1)
              | #ant as a0 -> (((* Obj.magic *) self#ant a0) :> (* 'all_b0
*) t mlist)
end






















-- 
Regards
-- Bob

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

Re: [Caml-list] This ground coercion is not principal?

[Jeremie Dimino]

On Thu, 10 Jan 2013 15:15:31 -0500
bob zhang <bobzhang1988@gmail.com> wrote:

> Hi List,
>   I have came across a corner case in ocaml typing here,
> The source code is pasted below(extracted from a large code base), it
> triggers the warning 18.
> My question, is there any elegant solution without introducing local
> types?

You can use an explicit coercion: (self#ant a0 : ant :> _ mlist)

Cheers,
Jeremie

Re: [Caml-list] This ground coercion is not principal?

[bob zhang]

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

Yes, it works, thanks. :-)
Actually I tried
((self#ant a0 : ant) :> _ mlist) before, the parens matter here

On Thu, Jan 10, 2013 at 4:06 PM, Jeremie Dimino <jeremie@dimino.org> wrote:

> On Thu, 10 Jan 2013 15:15:31 -0500
> bob zhang <bobzhang1988@gmail.com> wrote:
>
> > Hi List,
> >   I have came across a corner case in ocaml typing here,
> > The source code is pasted below(extracted from a large code base), it
> > triggers the warning 18.
> > My question, is there any elegant solution without introducing local
> > types?
>
> You can use an explicit coercion: (self#ant a0 : ant :> _ mlist)
>
> Cheers,
> Jeremie
>



-- 
Regards
-- Bob

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

[Caml-list] "this ground coercion is not principal"

[Martin DeMello]

What does this warning mean? I got it while compiling some code off
github [https://github.com/JoeDralliam/OcsfmlExamples/blob/master/Examples/sockets.ml]
and by experimenting it seems to be related to this bit from the
manual

Note that the coercion ( expr :>  typexpr ) is actually an abbreviated
form, and will only work in presence of private abbreviations if
neither the type of expr nor typexpr contain any type variables. If
they do, you must use the full form ( expr :  typexpr1 :>  typexpr2 )
where typexpr1 is the expected type of expr. Concretely, this would be
(x : N.t :> int) and (l : N.t list :> int list) for the above
examples.

but I could not find anything on google for either "ground coercion"
or "principal type coercion" that would explain what it was actually
saying. Could someone please point me to a reference?

martin

Re: [Caml-list] "this ground coercion is not principal"

[Jeremie Dimino]

On Wed, Feb 25, 2015 at 4:47 AM, Martin DeMello <martindemello@gmail.com> wrote:
> but I could not find anything on google for either "ground coercion"
> or "principal type coercion" that would explain what it was actually
> saying. Could someone please point me to a reference?

I don't know of a reference but there is a mantis ticket to improve
this error message:

  http://caml.inria.fr/mantis/view.php?id=5523

-- 
Jeremie

Re: [Caml-list] "this ground coercion is not principal"

[Jeremy Yallop]

On 25 February 2015 at 04:47, Martin DeMello <martindemello@gmail.com> wrote:
> What does this warning mean?

[tl;dr: the message means "The type of the expression is not known.
Add type annotations for the variables in the expression."]

Background: a private type abbreviation is defined by a type alias
definition with the word 'private'.  For example, the following
definition

   type t = private int

makes t a kind of half alias for int: you can convert from type t to
int, but you can't convert from int to t.  Coercions are performed
with the ':>' operator, so you can write things like this

   let f (x : t) = (x :>  int)

to convert from the private type t to the abbreviated type int.

Now, in order to check whether the following coercion is valid

   (x :> int)

the compiler needs to know the type of x.  There might be several
candidates: for example, with the private type abbreviation above in
scope, the coercion is valid if x has type t, but do-nothing coercions
are also allowed, so int is another reasonable possibility.  How can
the compiler choose between these alternatives to find the type of x?
In the definition of f above choosing is easy: x is a function
argument with an annotation, so the compiler just uses that
annotation.  Here's a slightly trickier case:

   let g (y : t) = ()

   let h x = (g x, (x :> int))

What's the type of x here?  The compiler's inference algorithm checks
the elements of a pair from left to right, so here's what happens:

  (1) Initially, when type checking for h starts, the type of x is unknown
  (2) The subexpression g x is checked, assigning x the type t, i.e.
the type of g's argument
  (3) The coercion (x :> int) is checked, and determined to be correct
since t can be coerced to int.

However, if the inference algorithm instead checked the elements of a
pair from right to left we'd have the following sequence of steps:

  (1) Initially, when type checking for h starts, the type of x is unknown
  (2) The coercion (x :> int) is checked, and the compiler guesses the
type of x.  In the absence of other information it guesses int.
  (3) The subexpression g x is checked and rejected, because x has
type int, not t.

Indeed, if we exchange the elements of the pair to simulate this
second behaviour

   let h2 x = ((x :> int), g x)

then the coercion is rejected:

    let h x = ((x :> int), g x);;
                             ^
    Error: This expression has type int but an expression was expected of type t

Since it's better for programs not to depend on the particular order
used by the inference algorithm, the compiler emits a warning.  You
can address the warning by annotating the binding for x:

   let h (x : t) = (g x, (x :> int))

Jeremy.

Re: [Caml-list] "this ground coercion is not principal"

[Martin DeMello]

Thanks, that explained everything very nicely!

I'm still curious about where the term "ground coercion" came from,
but I understand what the warning is saying now.

martin

On Wed, Feb 25, 2015 at 2:38 AM, Jeremy Yallop <yallop@gmail.com> wrote:
> On 25 February 2015 at 04:47, Martin DeMello <martindemello@gmail.com> wrote:
>> What does this warning mean?
>
> [tl;dr: the message means "The type of the expression is not known.
> Add type annotations for the variables in the expression."]
>
> Background: a private type abbreviation is defined by a type alias
> definition with the word 'private'.  For example, the following
> definition
>
>    type t = private int
>
> makes t a kind of half alias for int: you can convert from type t to
> int, but you can't convert from int to t.  Coercions are performed
> with the ':>' operator, so you can write things like this
>
>    let f (x : t) = (x :>  int)
>
> to convert from the private type t to the abbreviated type int.
>
> Now, in order to check whether the following coercion is valid
>
>    (x :> int)
>
> the compiler needs to know the type of x.  There might be several
> candidates: for example, with the private type abbreviation above in
> scope, the coercion is valid if x has type t, but do-nothing coercions
> are also allowed, so int is another reasonable possibility.  How can
> the compiler choose between these alternatives to find the type of x?
> In the definition of f above choosing is easy: x is a function
> argument with an annotation, so the compiler just uses that
> annotation.  Here's a slightly trickier case:
>
>    let g (y : t) = ()
>
>    let h x = (g x, (x :> int))
>
> What's the type of x here?  The compiler's inference algorithm checks
> the elements of a pair from left to right, so here's what happens:
>
>   (1) Initially, when type checking for h starts, the type of x is unknown
>   (2) The subexpression g x is checked, assigning x the type t, i.e.
> the type of g's argument
>   (3) The coercion (x :> int) is checked, and determined to be correct
> since t can be coerced to int.
>
> However, if the inference algorithm instead checked the elements of a
> pair from right to left we'd have the following sequence of steps:
>
>   (1) Initially, when type checking for h starts, the type of x is unknown
>   (2) The coercion (x :> int) is checked, and the compiler guesses the
> type of x.  In the absence of other information it guesses int.
>   (3) The subexpression g x is checked and rejected, because x has
> type int, not t.
>
> Indeed, if we exchange the elements of the pair to simulate this
> second behaviour
>
>    let h2 x = ((x :> int), g x)
>
> then the coercion is rejected:
>
>     let h x = ((x :> int), g x);;
>                              ^
>     Error: This expression has type int but an expression was expected of type t
>
> Since it's better for programs not to depend on the particular order
> used by the inference algorithm, the compiler emits a warning.  You
> can address the warning by annotating the binding for x:
>
>    let h (x : t) = (g x, (x :> int))
>
> Jeremy.

Re: [Caml-list] "this ground coercion is not principal"

[Jeremy Yallop]

On 25 February 2015 at 21:35, Martin DeMello <martindemello@gmail.com> wrote:
> I'm still curious about where the term "ground coercion" came from,

It comes from the term "ground type".  A ground type is a type which
doesn't contain type variables, like the types 't' and 'int' in the
example.