[Caml-list] A confusing example with modules and polymorphic variants

[Caml-list] A confusing example with modules and polymorphic variants

[Yaron Minsky]

Sorry for the previous incomplete message.  Over-eager return key.

We've been running into some troubles with polymorphic variants,
modules, and the value restriction, that we're not quite able to
unravel.  Here's a stripped down version of the problem.

    module type S = sig
      val z : [< `Foo ]
    end

    let f z =
      let module M : S = struct let z = z end in ()

Roughly speaking, we have a module signature S with a value that's a
polymorphic variant type that is not exact (i.e., has some
polymorphism in it.)

The function f then tries to construct a module of that type, by
taking the input value and stuffing it into a locally defined module.
When we do this, however, we're hit by a non-generalizable value
complaint.

    Modules do not match: sig val z : '_a end is not included in S
    Values do not match: val z : '_a is not included in val z : [< `Foo ]
    File "z.ml", line 2, characters 2-19: Expected declaration
    File "z.ml", line 7, characters 8-9: Actual declaration

Any thoughts on why this doesn't work, and how one could get it to?

Re: [Caml-list] A confusing example with modules and polymorphic variants

[Jeremy Yallop]

On 19 October 2012 22:18, Yaron Minsky <yminsky@janestreet.com> wrote:
> We've been running into some troubles with polymorphic variants,
> modules, and the value restriction, that we're not quite able to
> unravel.  Here's a stripped down version of the problem.
>
>     module type S = sig
>       val z : [< `Foo ]
>     end
>
>     let f z =
>       let module M : S = struct let z = z end in ()

I believe the problem here is the monomorphic parameter restriction: the type
of S requires the field z to be polymorphic, but type inference only assigns
monomorhpic types to function parameters.  That is, your example doesn't type
check for essentially the same reason that the following code doesn't type
check:

    type s = {
      z : 'a. 'a -> 'a
    }

    let f z =
      let s = {
        z = z
      } in
      ()

One way to work around the monomorphic parameter assumption is to wrap the
parameter in a record with a polymorphic field.

    type z_type = { field : 'a. 'a -> 'a}

    let f z =
      let s = {
        z = z.field
      } in
      ()

The parameter is still assigned a monomorphic type (z_type), but the projected
field is polymorphic, as required.

I don't see how to make that work in your case, though, because of the nature
of the polymorphism -- i.e. it's based on a row variable rather than a
standard type variable, and there isn't any syntax for quantifying it.

However, you *can* modify your example so that it passes type checking by
wrapping the argument in a first-class module, since module fields can be
row-polymorphic.  The easiest way in the cut-down example is to reuse the
signature you already have:

    module type S = sig
      val z : [< `Foo ]
    end

    let f (module Z : S) =
      let module M : S =
          struct
            let z = Z.z
          end
      in ()

Re: [Caml-list] A confusing example with modules and polymorphic variants

[Yaron Minsky]

Thanks!  That all makes perfect sense, now that you say it.  Not sure
why it was so hard for me to figure it out on my own.

One interesting bit is that a very similar example can be made to work
without resorting to these kinds of tricks.  In particular, if we
change the [< `Foo] to [> `Foo], then, we can get the polymorphism we
need back by using a cast:

    module type S = sig
      val z : [> `Foo ]
    end

    let f z =
      let module M : S = struct
        let z = (z : [`Foo] :> [> `Foo])
      end in
      ()

But this doesn't really help in the case I'm after.

y


On Fri, Oct 19, 2012 at 6:10 PM, Jeremy Yallop <yallop@gmail.com> wrote:
> On 19 October 2012 22:18, Yaron Minsky <yminsky@janestreet.com> wrote:
>> We've been running into some troubles with polymorphic variants,
>> modules, and the value restriction, that we're not quite able to
>> unravel.  Here's a stripped down version of the problem.
>>
>>     module type S = sig
>>       val z : [< `Foo ]
>>     end
>>
>>     let f z =
>>       let module M : S = struct let z = z end in ()
>
> I believe the problem here is the monomorphic parameter restriction: the type
> of S requires the field z to be polymorphic, but type inference only assigns
> monomorhpic types to function parameters.  That is, your example doesn't type
> check for essentially the same reason that the following code doesn't type
> check:
>
>     type s = {
>       z : 'a. 'a -> 'a
>     }
>
>     let f z =
>       let s = {
>         z = z
>       } in
>       ()
>
> One way to work around the monomorphic parameter assumption is to wrap the
> parameter in a record with a polymorphic field.
>
>     type z_type = { field : 'a. 'a -> 'a}
>
>     let f z =
>       let s = {
>         z = z.field
>       } in
>       ()
>
> The parameter is still assigned a monomorphic type (z_type), but the projected
> field is polymorphic, as required.
>
> I don't see how to make that work in your case, though, because of the nature
> of the polymorphism -- i.e. it's based on a row variable rather than a
> standard type variable, and there isn't any syntax for quantifying it.
>
> However, you *can* modify your example so that it passes type checking by
> wrapping the argument in a first-class module, since module fields can be
> row-polymorphic.  The easiest way in the cut-down example is to reuse the
> signature you already have:
>
>     module type S = sig
>       val z : [< `Foo ]
>     end
>
>     let f (module Z : S) =
>       let module M : S =
>           struct
>             let z = Z.z
>           end
>       in ()

Re: [Caml-list] A confusing example with modules and polymorphic variants

[Gabriel Scherer]

> I don't see how to make that work in your case, though, because of the nature
> of the polymorphism -- i.e. it's based on a row variable rather than a
> standard type variable, and there isn't any syntax for quantifying it.

You can capture the whole type "as" the polymorphic variable.

  type s = { z : 'a . [< `Foo ] as 'a }

  module type S = sig
    val z : [< `Foo ]
  end

  let f s =
    let module M : S = struct
      let z = s.z
    end in ()

This is essentially the same as your solution, using a polymorphic
field in a record instead of a polymorphic structure item in a
first-class module. I'm not exactly sure if/why this would solve or
not Yaron's problem, but in any regard I would consider the two
solutions equivalent.

On Sat, Oct 20, 2012 at 12:10 AM, Jeremy Yallop <yallop@gmail.com> wrote:
> On 19 October 2012 22:18, Yaron Minsky <yminsky@janestreet.com> wrote:
>> We've been running into some troubles with polymorphic variants,
>> modules, and the value restriction, that we're not quite able to
>> unravel.  Here's a stripped down version of the problem.
>>
>>     module type S = sig
>>       val z : [< `Foo ]
>>     end
>>
>>     let f z =
>>       let module M : S = struct let z = z end in ()
>
> I believe the problem here is the monomorphic parameter restriction: the type
> of S requires the field z to be polymorphic, but type inference only assigns
> monomorhpic types to function parameters.  That is, your example doesn't type
> check for essentially the same reason that the following code doesn't type
> check:
>
>     type s = {
>       z : 'a. 'a -> 'a
>     }
>
>     let f z =
>       let s = {
>         z = z
>       } in
>       ()
>
> One way to work around the monomorphic parameter assumption is to wrap the
> parameter in a record with a polymorphic field.
>
>     type z_type = { field : 'a. 'a -> 'a}
>
>     let f z =
>       let s = {
>         z = z.field
>       } in
>       ()
>
> The parameter is still assigned a monomorphic type (z_type), but the projected
> field is polymorphic, as required.
>
> I don't see how to make that work in your case, though, because of the nature
> of the polymorphism -- i.e. it's based on a row variable rather than a
> standard type variable, and there isn't any syntax for quantifying it.
>
> However, you *can* modify your example so that it passes type checking by
> wrapping the argument in a first-class module, since module fields can be
> row-polymorphic.  The easiest way in the cut-down example is to reuse the
> signature you already have:
>
>     module type S = sig
>       val z : [< `Foo ]
>     end
>
>     let f (module Z : S) =
>       let module M : S =
>           struct
>             let z = Z.z
>           end
>       in ()
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] A confusing example with modules and polymorphic variants

[Yaron Minsky]