Re: [Caml-list] Re: "module type of" on sub-module of functor result

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2012/02/23, at 3:49, Andreas Rossberg wrote:

> On Feb 22, 2012, at 18.24 h, Gabriel Scherer wrote:
>>> [A(B)] and  [A.B] are syntacticly valid module_expr's but
>>> [A(B).C] isn't. Is this because of an inherent limitation in the
>>> module system?
>> 
>> I believe so. When you apply a functor, you may get fresh types as a
>> result -- the generative (abstract, algebraic) types of the functor
>> image. If you write `module M = A(B)`, the fresh types have a clear
>> identity: M.t, M.q etc; similarly if you pass A(B) to a functor with
>> formal parameter X, it is X.t, X.q etc. But if you write `module M =
>> A(B).C`, there is no syntactic way to name the fresh types generated
>> by the functor application; in particular, naming them A(B).t would be
>> incorrect -- because you could mix types of different applications.
>> 
>> For example, what would be the signature of A(B).C with:
>> 
>> module B = struct end
>> module A(X : sig end) = struct
>>   type t
>>   module C = struct type q = t end
>> end
>> 
>> ?
> 
> Are you perhaps thinking of SML-style generative functors here? Because with Ocaml's applicative functors F(A) in fact always returns the same abstract types, and you _can_ actually refer to types via the notation F(A).t ;-)

This is not strictly correct, because of the possibility of avoidance.
I.e. you are allowed to apply a functor to a structure rather than a path, and in that case the behavior of the functor becomes generative,
so the problem described by Gabriel really applies in that case.

Going back to the question of "module type of", it is currently implemented by typing the module expression in the usual way.
So extending it to a stronger form of module expression would require changing that, and introduce extra complexity.
Doable, but don't hold your breath...

Jacques Garrigue