[Caml-list] First-class modules in functor bodies

[Caml-list] First-class modules in functor bodies

[Markus Mottl]

Hi,

I've been wondering why the following is disallowed:

-----
module M (U : sig end) = struct
  module type S = sig val x : int end
  let a = ((module struct let x = 42 end : S))
  module A = (val a)
end
-----

The error message is:

-----
File "foo.ml", line 4, characters 13-20:
Error: This kind of expression is not allowed within the body of a functor.
-----

Making M a module by removing the functor argument works as expected.

Is there some inherent unsoundness issue with allowing this kind of
use of first-class modules within functor bodies, or would it just be
hard adding sound support for the above to the current type system?

Regards,
Markus

--
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

Re: [Caml-list] First-class modules in functor bodies

[Philippe Wang]

I'm curious because I don't quite understand: could you tell the
supposed semantic differences between your code and the following
code?
module M (U : sig end) = struct
  module type S = sig val x : int end
  let a = ((module struct let x = 42 end : S))
  module A = struct let a = a end
end

On Sun, May 19, 2013 at 4:14 PM, Markus Mottl <markus.mottl@gmail.com> wrote:
> Hi,
>
> I've been wondering why the following is disallowed:
>
> -----
> module M (U : sig end) = struct
>   module type S = sig val x : int end
>   let a = ((module struct let x = 42 end : S))
>   module A = (val a)
> end
> -----
>
> The error message is:
>
> -----
> File "foo.ml", line 4, characters 13-20:
> Error: This kind of expression is not allowed within the body of a functor.
> -----
>
> Making M a module by removing the functor argument works as expected.
>
> Is there some inherent unsoundness issue with allowing this kind of
> use of first-class modules within functor bodies, or would it just be
> hard adding sound support for the above to the current type system?
>
> Regards,
> Markus
>
> --
> Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs



-- 
Philippe Wang
   mail@philippewang.info

Re: [Caml-list] First-class modules in functor bodies

[Markus Mottl]

In my example "module A" should be bound to "struct let x = 42 end",
not to a module containing a first-class module binding "a".

But this reminds me of a further question.  The following is allowed:

-----
module M (U : sig end) = struct
  module type S = sig val x : int end
  let a = ((module struct let x = 42 end : S))
  module A = struct
    let x =
      let module A = (val a) in
      A.x
  end
end
-----

Wouldn't the above be essentially equivalent to what I want to do?
Maybe the current restriction covers some weird corner-case that I
can't think of right now.

On Sun, May 19, 2013 at 7:07 PM, Philippe Wang <mail@philippewang.info> wrote:
> I'm curious because I don't quite understand: could you tell the
> supposed semantic differences between your code and the following
> code?
> module M (U : sig end) = struct
>   module type S = sig val x : int end
>   let a = ((module struct let x = 42 end : S))
>   module A = struct let a = a end
> end
>
> On Sun, May 19, 2013 at 4:14 PM, Markus Mottl <markus.mottl@gmail.com> wrote:
>> Hi,
>>
>> I've been wondering why the following is disallowed:
>>
>> -----
>> module M (U : sig end) = struct
>>   module type S = sig val x : int end
>>   let a = ((module struct let x = 42 end : S))
>>   module A = (val a)
>> end
>> -----
>>
>> The error message is:
>>
>> -----
>> File "foo.ml", line 4, characters 13-20:
>> Error: This kind of expression is not allowed within the body of a functor.
>> -----
>>
>> Making M a module by removing the functor argument works as expected.
>>
>> Is there some inherent unsoundness issue with allowing this kind of
>> use of first-class modules within functor bodies, or would it just be
>> hard adding sound support for the above to the current type system?
>>
>> Regards,
>> Markus
>>
>> --
>> Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com
>>
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa.inria.fr/sympa/arc/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>
>
> --
> Philippe Wang
>    mail@philippewang.info



-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

Re: [Caml-list] First-class modules in functor bodies

[Alain Frisch]

On 05/19/2013 05:14 PM, Markus Mottl wrote:
> I've been wondering why the following is disallowed:
>
> -----
> module M (U : sig end) = struct
>    module type S = sig val x : int end
>    let a = ((module struct let x = 42 end : S))
>    module A = (val a)
> end
> -----
>
> The error message is:
>
> -----
> File "foo.ml", line 4, characters 13-20:
> Error: This kind of expression is not allowed within the body of a functor.
> -----
>
> Is there some inherent unsoundness issue with allowing this kind of
> use of first-class modules within functor bodies

Indeed, unpacking first-class modules does not interact nicely with 
applicative functors.  The problem is that with applicative functors, a 
path such as "F(M).t" must refer to a well-defined type, and always the 
same one for a given module M, but with first-class modules, you could 
apply the same functor F twice to the same argument M and dynamically 
get two different types F(M).t, thus breaking soundness.

Here is an counter-example provided by Didier Rémy:

     module type X = sig type t val x : t val bin : t -> t -> t end
     module X1 = struct type t = int let x = 0 let bin = (+) end
     module X2 = struct type t = string let x = "" let bin = (^) end

     let b = ref false

     module F(U:sig end) =
      (val (if !b then (module X1 : X) else (module X2 : X)) : X)

     module U = struct end;;
     b := false;;
     module Y1 = F(U);;
     b := true;;
     module Y2 = F(U);;

Then Y1.t = F(U).t = Y2.t, and the following would be well-typed:

     Y2.bin (Y1.bin Y1.x Y2.x) Y1.x



Jacques Garrigue has a proposal to extend the language with functors 
explicitly marked as generated:

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

In such functors, it is indeed allowed to unpack first-class modules.


Alain

Re: [Caml-list] First-class modules in functor bodies

[Markus Mottl]

On Mon, May 20, 2013 at 3:31 AM, Alain Frisch <alain@frisch.fr> wrote:
> Here is an counter-example provided by Didier Rémy:
[snip]
>     module F(U:sig end) =
>      (val (if !b then (module X1 : X) else (module X2 : X)) : X)

Ah, yeah, that's evil.  It's funny that even after years of using
OCaml the applicative nature of functors sometimes surprises me.  I
admit to having done some SML in my youth, but I thought I was clean
by now :)

--
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

Re: [Caml-list] First-class modules in functor bodies

[Jacques Carette]

On 13-05-20 10:01 AM, Markus Mottl wrote:
> On Mon, May 20, 2013 at 3:31 AM, Alain Frisch <alain@frisch.fr> wrote:
>> Here is an counter-example provided by Didier Rémy:
> [snip]
>>      module F(U:sig end) =
>>       (val (if !b then (module X1 : X) else (module X2 : X)) : X)
> Ah, yeah, that's evil.

If only there were an _option_ to have OCaml track state in its types, 
lots of this would be greatly simplified, at least for those OCaml 
programmers willing to do that.

I understand that not tracking state (or other effects) in OCaml types 
is a fundamental design decision that makes OCaml a hybrid 
functional-imperative language.  I just wish I had the option of using 
it purely functionally, and the compiler would then give me all the 
accompanying riches that comes with that choice.

Jacques