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

[Phil Scott <phil.scott@ed.ac.uk>]

Cheers Bob (and Tom Ridge)! I'm through the type-checker. I'll have a
play tomorrow and see if it does what I need.

Robert Atkey writes:

> 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
>>


-- 
Phil Scott
Centre for Intelligent Systems and their Applications
University of Edinburgh

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.