[Caml-list] Limitations of first-class modules

[Caml-list] Limitations of first-class modules

[Lauri Alanko]

When first-class modules were announced for OCaml 3.12, I cheered them
as a sorely needed extension, and I have now begun to make heavy use
of them. I certainly prefer them over objects, even if I do find the
syntax of first-class modules a bit awkward. I would much prefer to
see a completely unified object-module system a la Scala, but I guess
such drastic changes are beyond the scope of OCaml's development
nowadays.

Anyway, I'm now beginning to stumble into the limitations of the
extension, and I'm a bit curious about their rationale.

In a type (module S), S must be a path to a named module type, and if
A and B are two different paths, (module A) and (module B) are
distinct even if A and B are transparent definitions for exactly the
same module types. This nominalism is quite surprising since one is
used to transparent definitions being just shorthands for signatures
that are compared structurally. In particular, this means that it is
no longer harmless to include a signature definition to compose a
convenience module from several submodules:

module A = struct 
  module type S = sig end
  type t = (module S)
  module M : S = struct end
  let v = (module M : S)
end

module B = struct
  include A
end

# module X : A.S = B.M;;
module X : A.S

# let x : A.t = B.v;;
Error: This expression has type (module B.S)
       but an expression was expected of type A.t = (module A.S)

Also, the limitations of package type constraints were also somewhat
surprising. The limitation about unpacking first-class modules in
functors was thankfully explained in the documentation, and it made
sense after a moment's reflection. No such rationale was included for
the rest of the design, so I'd be interested in hearing what's behind
it.


Lauri

[Caml-list] Generative functors how?

[Lauri Alanko]

On Wed, Jan 19, 2011 at 02:33:35PM +0200, Lauri Alanko wrote:
> Also, the limitations of package type constraints were also somewhat
> surprising. The limitation about unpacking first-class modules in
> functors was thankfully explained in the documentation, and it made
> sense after a moment's reflection. No such rationale was included for
> the rest of the design, so I'd be interested in hearing what's behind
> it.

Regarding the functor restriction, I found this explained in

<http://caml.inria.fr/pub/papers/xleroy-applicative_functors-popl95.pdf>,

section 2.7. It would be nice to have these sorts of background
references mentioned in the manual.

This brings me to a related issue. Functors in O'Caml are applicative,
as described in the above paper. However, I have a bit of
side-effectful magic code whose type-safety depends on functors being
generative (details at the end). What should I do?

One option is using the brand new -no-app-funct compiler option, which
I haven't seen advertised very much. However, this is a global change
(or can -no-app-funct be used consistently with only some modules?),
and although I don't currently see any need for applicative functors,
I dislike the idea of disabling them completely just for the
occasional need for generativity.

The other option is to use first-class modules. Instead of

module F(M : S1) : S2

one would use

val f : (module S1) -> (module S2)

This is arguably a more faithful interface, since the result module
initialization does have side effects, and I think the usual custom is
that functor applications are not really supposed to be observably
effectful. (But is type generation an "effect"?)

The problem with this is firstly that the expressible constraints are
limited. One can do stuff like:

val f : (module S1 with type t = 'a) -> (module S2 with type u = 'a)

but nothing more complex. The second problem is simply that because of
the above functor limitation with first class module unpacking, no
functor can directly use a generative module function like this, so I
have to cascade the change into all my functors that even indirectly
depend on generativity. Again, this is arguably a good thing since
then the generativity is directly expressed in the interfaces, but
it's just much nicer to write:


module F(M : S1) : S2 = struct
  ...
  module MA : SA = ...
  module MB : SB = G(MB)
  ...
end

rather than

let f m =
  let module M = (val m : S1) in
  let module FM = struct
    ...
    module MA : SA = ...
    module MB : SB = (val g (module MA : SA) : SB)
    ...
  end in
  (module FM : S2)

The extra level of indentation is almost a deal-breaker. :)

So, any recommendations for the best approach?


Lauri

P.S. Oh yes, here's a rough sketch of the magic:

module TypeId(Unit : sig end) : sig
  type 'a t
  val gen : unit -> 'a t
  val cast : 'a t -> 'b t -> 'a -> 'b option
end = struct
  type 'a t = int
  let next = ref 0
  let gen () = incr next; !next
  let cast ka kb a =
    if ka = kb then
      Some (Obj.magic a)
    else
      None
end

In this particular case, obviously a single module would be
sufficient, but I want to be able to have generatively multiple
distinct type constructors 'a t, so that typeids used in one context
cannot accidentally be confused by those used in another.

Re: [Caml-list] Limitations of first-class modules

[Jacques Garrigue]

On 2011/01/19, at 21:33, Lauri Alanko wrote:

> When first-class modules were announced for OCaml 3.12, I cheered them
> as a sorely needed extension, and I have now begun to make heavy use
> of them. I certainly prefer them over objects, even if I do find the
> syntax of first-class modules a bit awkward. I would much prefer to
> see a completely unified object-module system a la Scala, but I guess
> such drastic changes are beyond the scope of OCaml's development
> nowadays.
> 
> Anyway, I'm now beginning to stumble into the limitations of the
> extension, and I'm a bit curious about their rationale.
> 
> In a type (module S), S must be a path to a named module type, and if
> A and B are two different paths, (module A) and (module B) are
> distinct even if A and B are transparent definitions for exactly the
> same module types. This nominalism is quite surprising since one is
> used to transparent definitions being just shorthands for signatures
> that are compared structurally. In particular, this means that it is
> no longer harmless to include a signature definition to compose a
> convenience module from several submodules:
> 
> module A = struct 
>  module type S = sig end
>  type t = (module S)
>  module M : S = struct end
>  let v = (module M : S)
> end
> 
> module B = struct
>  include A
> end
> 
> # module X : A.S = B.M;;
> module X : A.S
> 
> # let x : A.t = B.v;;
> Error: This expression has type (module B.S)
>       but an expression was expected of type A.t = (module A.S)

I think there are two reasons for this limitation:
* avoiding having to run a full module type comparison during unification
  (potentially costly)
* in case the first-class module has type variables in its parameters,
   the original algorithm for module type comparison cannot be applied directly

I'm not sure the first reason matters that much.
The second one is more problematic, but clearly does not apply to your case.
So it should at least be possible to check module type equality structurally for
parameter-less first-class module types.

Note that if you use the trunk version (3.13), you need less annotations, so
you could write:
   let x : A.t = (module (val B.v))
A bit verbose, but no extra type annotations.

> Also, the limitations of package type constraints were also somewhat
> surprising.

The main goal of package type constraints is to allow connecting
types in the signature with type variables in the context.
Since type variables cannot have higher-order kinds in ocaml,
allowing to specify parameterized types in with constraints would
not make sense from that point of view.
It may still be useful, but there may be difficulties in connection with
the new implicit pack/unpack mecanism.

Jacques Garrigue

Re: [Caml-list] Limitations of first-class modules

[Alain Frisch]

On 01/19/2011 01:33 PM, Lauri Alanko wrote:
> When first-class modules were announced for OCaml 3.12, I cheered them
> as a sorely needed extension, and I have now begun to make heavy use
> of them. I certainly prefer them over objects, even if I do find the
> syntax of first-class modules a bit awkward.

As Jacques mentioned, OCaml 3.13 will allow a lighter syntax, with a lot 
less explicit type annotations. Hopefully, this will make it less awkward.

> I would much prefer to
> see a completely unified object-module system a la Scala, but I guess
> such drastic changes are beyond the scope of OCaml's development
> nowadays.

Indeed.

> Anyway, I'm now beginning to stumble into the limitations of the
> extension, and I'm a bit curious about their rationale.
>
> In a type (module S), S must be a path to a named module type, and if
> A and B are two different paths, (module A) and (module B) are
> distinct even if A and B are transparent definitions for exactly the
> same module types.

One could indeed declare that (module A) and (module B) are equal
as soon as A and B refer to equal module types (that is, two module 
types subtype of each other without any coercion). I don't think there 
is any deep obstacle in doing that. One would need to be a little bit 
careful with mutually recursive types and module types (introduced with 
a recursive module).  As for the implementation strategy, I'm a little 
bit concerned of having a low-level module in the type-checker (Ctype), 
in charge of things like type equality check or unification, calling a 
function in a higher-level module (Includemod), but I don't see 
immediately any concrete problem in doing that.

What would be much more difficult is to declare that general package 
type (with constraints, like (module A with type t1 = T1)) are equal if 
the module types obtained by "applying the constraints" are equal. 
Indeed, the type T1 above can contain type variables, and a constraint 
"with type t1 = T1" is then not supported by the module system (there is 
no module type with free type variables).


There is a branch fstclassmod_parametrized in the SVN which allows more 
kinds of constraints; in particular, it allows constraints on 
parametrized types (module A with type 'a t1 = T1). See e.g.

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

This extension does not seem very useful to me in practice (because 
there is no polymorphism on type constructors in OCaml). Moreover, it 
isn't trivially combined with Jacques' work mentioned above. So it's 
probably not going to be integrated upstream.


Feel free to open entries in the bug tracker with specific examples of 
things you'd like to do but which are not possible or difficult with the 
current design.  My initial work on first-class modules was driven by 
our internal use at LexiFi (for which the nominal aspect has never been 
a problem) and also by the constraint of keeping the patch small enough 
(to increase the odds of being accepted upstream).



Alain

Re: [Caml-list] Limitations of first-class modules

[Jamie Brandon]

> There is a branch fstclassmod_parametrized in the SVN which allows more
> kinds of constraints; in particular, it allows constraints on parametrized
> types (module A with type 'a t1 = T1)
...
> This extension does not seem very useful to me in practice (because there is
> no polymorphism on type constructors in OCaml).

I was trying to do exactly that last week:

http://zheng.li/buzzlogs-ocaml/2011/01/13/irc.html

It allows working with abstract collections without using functors,
which is fairly useful.