[Caml-list] Help with recursive modules and functors

[Caml-list] Help with recursive modules and functors

[Phil Scott]

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

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

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

[Robert Atkey]

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
>

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

[Phil Scott]

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.