[Caml-list] Manipulating Modules Modularly

[Caml-list] Manipulating Modules Modularly

[Arnaud Spiwack]

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

Dear all,

Here is a puzzle I run way to often in (yesterday was one of these) and
have not good solution to.

Suppose I have a module signature such as monoids:

module type M = sig  type t  val u:t  val p:t->t->t  end

And a functor:

module type ME = sig  type t  val ps:t list -> t  end
module ME (M:M) : ME with type t := M.t

All good and well. I now want to reuse my functor for list, which are a
monoid. But I can only get:

module type TYPE = sig type t end
module LEF (T:TYPE) : ME with type t = T.t list

By the way, I have no intuition why I cannot use a := (substitution) above
and am stuck with a type definition.

But that's not my question. What I really want is a module

module LE : ME with type t := 'a list

There are two problems here. First, I don't know how to define the
signature (which, expanded would be   sig val ps : 'a list list -> 'a list)
without copying. Second I don't know how to do write the module LE itself,
without boilerplate proportional to the number of function in the signature.

With local modules it is reasonably easy to implement LE without modifying
ME, by re-exporting every function as a function which instantiates LEF
(though I guess [u] would only work because list is covariant). But I would
rather the module LE to extend automatically as I extend the signature of
ME.

The thing is, this is just the commutation between forall-s and product-s.
So provided the functor instantiation is pure, then it is always possible
to do that. But I don't know of any modular way to do it.

So here's my question: how do you/would you solve this problem. If the
solution is compatible with 3.12, it's a plus.



/Arnaud

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

Re: [Caml-list] Manipulating Modules Modularly

[Leo White]

> module type M = sig  type t  val u:t  val p:t->t->t  end
>
> And a functor:
>
> module type ME = sig  type t  val ps:t list -> t  end
> module ME (M:M) : ME with type t := M.t
>
> All good and well. I now want to reuse my functor for list, which are a monoid.
> What I really want is a module
>
> module LE : ME with type t := 'a list
>
> So here's my question: how do you/would you solve this problem. If the solution is compatible with 3.12, it's a plus.
>

Moving quantifiers around is awkward in the module system, but is also
not safe in general. We can clearly illustrate this by reencoding your
example without modules:

First we define `m` as a record type and create one for lists:

    # type 'a m = { u : 'a; p : 'a -> 'a -> 'a };;
    type 'a m = { u : 'a; p : 'a -> 'a -> 'a; }

    # let list = { u = []; p = (@) };;
    val list : 'a list m = {u = []; p = <fun>}

Then we define the `me` as another record type and create a simple
function for creating them from monoids:

    # type 'a me = { ps : 'a list -> 'a };;
    type 'a me = { ps : 'a list -> 'a; }

    # let me (m : 'a m) = { ps = List.fold_left m.p m.u };;
    val me : 'a m -> 'a me = <fun>

Now we can apply the `me` function to the `list` monoid:

    # let mel = me list;;
    val mel : '_a list me = {ps = <fun>}

But what we get is only weakly polymophic because of the value
restriction. This hints at the unsafety of what we are trying to
do. Whilst the above definition of `me` happens to be safe, consider the
following version:

    # let me (m : 'a m) =
        let r = ref m.u in
        let ps = function
        | [] -> !r
        | x :: xs ->
            let old = !r in
              r := x;
              List.fold_left m.p m.u (old :: xs)
        in
          {ps};;
                      val me : 'a m -> 'a me = <fun>

    # let mel = me list;;
    val mel : '_a list me = {ps = <fun>}

Here we use a reference to preserve elements of the monoid across
different calls to `ps`. If this were allowed to be polymorphic we could
end up mixing elements of different list types together. For example, if
we use `Obj.magic` to pretend that `mel` is polymorphic we can quickly
get a segfault:

    # let meli : int list me = Obj.magic mel;;
    val meli : int list me = {ps = <fun>}

    # let melf : float list me = Obj.magic mel;;
    val melf : float list me = {ps = <fun>}

    # meli.ps [[1; 2; 3]; [2; 3; 4]];;
    - : int list = [2; 3; 4]

    # melf.ps [[1.0; 2.0; 3.0]; [2.0; 3.0; 4.0]];;

    Process ocaml-toplevel segmentation fault

So hopefully, this illustrates why you cannot easily get what you want
in a language with side-effects. Since what you are fundementally trying
to do is safe, I suspect that a language with good support for
higher-rank polymorphism, higher-kinded polymorphism, and kind
polymorphism might be apply to encode it safely even in the presence of
side-effects, but the encoding is likely to be a bit involved.

Regards,

Leo

Re: [Caml-list] Manipulating Modules Modularly

[Leo White]

> Moving quantifiers around is awkward in the module system, but is also
> not safe in general. We can clearly illustrate this by reencoding your
> example without modules:
>
> First we define `m` as a record type and create one for lists:
>
>     # type 'a m = { u : 'a; p : 'a -> 'a -> 'a };;
>     type 'a m = { u : 'a; p : 'a -> 'a -> 'a; }
>
>     # let list = { u = []; p = (@) };;
>     val list : 'a list m = {u = []; p = <fun>}
>
> Then we define the `me` as another record type and create a simple
> function for creating them from monoids:
>
>     # type 'a me = { ps : 'a list -> 'a };;
>     type 'a me = { ps : 'a list -> 'a; }
>
>     # let me (m : 'a m) = { ps = List.fold_left m.p m.u };;
>     val me : 'a m -> 'a me = <fun>
>
> Now we can apply the `me` function to the `list` monoid:
>
>     # let mel = me list;;
>     val mel : '_a list me = {ps = <fun>}
>
> But what we get is only weakly polymophic because of the value
> restriction.

It is worth noting we can eta-expand to avoid the value restriction:

    # type 'a me = 'a list -> 'a;;
    type 'a me = 'a list -> 'a

    # let me (m : 'a m) : 'a me = List.fold_left m.p m.u;;
    val me : 'a m -> 'a me = <fun>

    # let mel : 'a list me = fun l -> me list l;;
    val mel : 'a list me = <fun>

Which is just equivalent to the solution you already described:

>> With local modules it is reasonably easy to implement LE without modifying ME, by re-exporting every function as a
>> function which instantiates LEF (though I guess [u] would only work because list is covariant). But I would rather the
>> module LE to extend automatically as I extend the signature of ME.

However, since we are using the core language instead of the module
language, we get type inference and can avoid repeating ourselves so
much. Perhaps this is an acceptable solution for your use cases.

Regards,

Leo

Re: [Caml-list] Manipulating Modules Modularly

[Arnaud Spiwack]

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

> Perhaps this is an acceptable solution for your use cases.
>

It isn't, I'm afraid.

By the way, I'm well aware of the problem with effects and value
restriction and such (hence my qualification above, with purity). However,
I don't care if it fails from time to time (and I think I remember some
check about purity being done somewhere in the module system). For my
use-case, I don't care if I need to have access to the original source-code
-- I mean to see the concrete definition of the functor rather than its
signature -- either (though it seems a limitation in general).

Am I weird to run into this issue all the time or is it common?


PS: now that there are both applicative functors and generative functors,
could applicative functors be restricted to being pure, so that this sort
of manipulation become possible in a generic way?

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

Re: [Caml-list] Manipulating Modules Modularly

[Leo White]

> Am I weird to run into this issue all the time or is it common?

Depends which issue you mean.

People run into the value restriction quite frequently but eta-expansion
is usually considered an acceptable solution, although it does require a
certain amount of boilerplate.

Note that your problem can also be worked around for a fixed number of
type parameters by defining your module types as:

    module type M = sig
        type 'a t
        val u : 'a t
        val p : 'a t -> 'a t -> 'a t
      end

    module type ME = sig
       type 'a t
       val ps: 'a t list -> 'a t
    end

which will now work for types with 0 or 1 parameters.

> PS: now that there are both applicative functors and generative functors, could applicative functors be restricted to
> being pure, so that this sort of manipulation become possible in a generic way?

That would break a lot of existing code and wouldn't work very well
without a full effect system in the core language.

Regards,

Leo

Re: [Caml-list] Manipulating Modules Modularly

[Arnaud Spiwack]

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

> Depends which issue you mean.
>

I mean having a functor which compiles with several signatures and wanting
to leverage that fact with minimal fuss. But obviously, it does not seem to
stir the passions of the ocaml list readers. I'm going for weird…


> Note that your problem can also be worked around for a fixed number of
> type parameters by defining your module types as:
>
>     module type M = sig
>         type 'a t
>         val u : 'a t
>         val p : 'a t -> 'a t -> 'a t
>       end
>
>     module type ME = sig
>        type 'a t
>        val ps: 'a t list -> 'a t
>     end
>
> which will now work for types with 0 or 1 parameters.
>

It's not very modular, but indeed. It requires signature duplication
however, because (for some reason), we cannot do things like "S with type
'a t := int", and I happen to use substitution. I guess I could use more
powerful ways to manipulate signatures. Like taking a module signature with
a type [t], and turn it into the same signature of type ['a t] (with 'a
universally bound at each function). This is always well defined, isn't it?

The other way around sound easier to do however (replacing a Signature on
['a t] by a signature in [t]), as it it just requires loosening the
restriction on "same parameters" in member substitution to "a subset of the
parameters". But it's less modular and not as good for documentation. But
it would be sufficient for many use-cases.

 That would break a lot of existing code and wouldn't work very well
> without a full effect system in the core language.
>

I don't think it would break that much (and if it breaks something the fix
is two characters long…). I mean, the functions exported by the functor
need not be pure. It's just the functor application which has to (that is
no reference or such at toplevel). I don't think an effect system is
required for that. But my question is mostly theoretical, anyway.

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