Re: [Caml-list] Bug in the module system of version 3.12.0+beta1

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

From: Dumitru Potop-Butucaru <dumitru.potop_butucaru@inria.fr>
> However, I still did not understand this statement of
> Jeremy Yallop:
>>> module type Abc =
>>>    functor (M:Simple) ->
>>>    sig
>>>       val x : M.t
>>>    end
>>>      
>> You're trying to treat Abc as a functor from signatures to signatures
>> (i.e. as a parameterised signature). In fact, it's something quite
>> different: it's the *type* of a functor from structures to structures.
>>    
> If I understand well, what I try to do is impossible for
> some deep theoretical reason. Can someone explain this
> to me, or point me to a relevant paper explaining it?

I think this is not a question of impossibility, rather of
misunderstanding of the relation between modules and signatures.
A module type describes modules, it does not replace them.
In particular, in another mail you asked for the construct:

  module type MyModuleType(Param:ParamType) = sig ... end

But this just doesn't make sense. The type of a functor is not a
functor between module types. Just like the type "t1 * t2" describes
pairs of values of type t1 and t2, but it is not itself a pair of
types, but rather a product.

Note of course that one might want to play on the conceptual
similarity to write the two in the same way. Haskell does that a lot,
writing (t1,t2) for the product of the types t1 and t2. But if
you look at languages like Coq, where types are also values, this
kind of overloading seems dangerous.

Another similar misunderstanding is when you write
      include Abc(module type of IntSet)
This statement is doubly wrong: first you cannot apply a module type,
but even if Abc were a functor, it could only be applied to a module,
not a module type.
Others have explained how you can do what you intended, in two
different ways. 
The classical way is to use a real functor, returning a signature
enclosed in a module, since there is no way to return a signature
alone. There is nothing against applying functors inside signatures.
The new solution in 3.12 is to use a variant of the "with"
construct, which does exactly what you want, i.e. it turns a
signature into a "function" returning a signature.

Hope this helps,

Jacques Garrigue