Manipulating Modules Modularly

[Arnaud Spiwack]

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

[Leo White]

module type M = sig  type t  val u:t  val p:t->t->t  end
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

[Leo White]

Post by 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
# type 'a m = { u : 'a; p : 'a -> 'a -> 'a };;
type 'a m = { u : 'a; p : 'a -> 'a -> 'a; }
val list : 'a list m = {u = []; p = <fun>}
Then we define the `me` as another record type and create a simple
# 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>
# 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>

Post by Leo White

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

[Arnaud Spiwack]

Post by Leo White
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?

[Leo White]

Post by Arnaud Spiwack
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.

Post by Arnaud Spiwack
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

[Arnaud Spiwack]

Post by Leo White
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


Post by Leo White
Note that your problem can also be worked around for a fixed number of
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

Post by Leo White
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.