Re: [Caml-list] Help with recursive modules and functors

[Robert Atkey <bob.atkey@gmail.com>]

Hi Phil,

I'm not sure if this solves your problem, but the following seems to 
work. It rewraps 'F' as 'X' in the recursive declaration, whilst 
ensuring that 'X' gives the same answers as 'F' does.

   module type Foo = functor(S : sig type s val foo : s -> s end) ->
   sig
     type t
   end

   module Bar = functor(F: Foo) ->
   struct
     module rec S : sig
       type s = int
       type baz = Baz of X(S).t
       val foo : s -> s
     end =
     struct
       type s = int
       type baz = Baz of X(S).t
       let foo x = x
     end
     and X : functor(S : sig type s val foo : s -> s end) ->
     sig
       type t = F(S).t
     end = F
   end

I think this is the expected behaviour:

# module B = Bar (functor (S : sig type s val foo : s -> s end) ->
                                 struct type t = [ `X of S.s ] end);;
module B : sig
   module rec S :
       sig type s = int type baz = Baz of X(S).t val foo : s -> s end
   and X :
       functor (S : sig type s val foo : s -> s end) ->
         sig type t = [ `X of S.s ] end
end
# B.S.Baz (`X 5);;
- : B.S.baz = B.S.Baz (`X 5)

I'm not sure what the rules for typing recursive modules are, so I'm not 
sure why mine type checks and yours doesn't.

Bob

On 07/02/17 12:50, Phil Scott wrote:
> Hi all.
>
> Suppose I have the following code:
>
>   module type Foo = functor(S : sig type s val foo : s -> s end) ->
>     sig
>       type t
>     end
>
>   module Bar =
>     functor(F: Foo) ->
>     struct
>       module rec S :
>                    sig
>                      type s = int
>                      type baz = Baz of F(S).t
>                      val foo : s -> s
>                    end =
>         struct
>           type s = int
>           type baz = Baz of F(S).t
>           let foo x = x
>         end
>     end
>
> Here, I want my Bar module to apply its supplied Foo to a recursive
> module S. However, I am being told that the functor application F(S) in
> the signature for S is ill-typed. The problems are apparently due to the
> type of baz in the signature. If I change the type so that it doesn't
> involve F(S), the type-checker is happy:
>
>   module Bar =
>     functor(F: Foo) ->
>     struct
>       module rec S :
>                    sig
>                      type s = int
>                      type baz = Baz
>                      val foo : s -> s
>                    end =
>         struct
>           type s = int
>           type baz = Baz
>           let foo x = x
>         end
>     end
>
> But this is odd to me, since baz is not even in the signature of Foo's
> argument, so I don't understand how it's type could affect the type
> correctness of the functor application. Can anyone explain to me what
> the problem is? I understand that I'm probably pushing what recursive
> modules can do, but would like some details if anyone can clear it up
> for me.
>
> Thanks!
>
> --
> Phil Scott
> Centre for Intelligent Systems and their Applications
> University of Edinburgh
>