[Caml-list] Applicative Functor Madness

[Caml-list] Applicative Functor Madness

[Arlen Cox]

[-- Attachment #1: Type: text/plain, Size: 1736 bytes --]

Hi everyone,

I'm having some trouble getting some code that relies heavily on
applicative functors to type check.  Does anyone know what I'm doing wrong
with this?

module type S = sig
  module T : Set.OrderedType
  module ST : module type of Set.Make(T)
end

module Make(T_in : Set.OrderedType) : S (* <- ERROR *)
  with module T = T_in
   and module ST = Set.Make(T_in)
= struct
  module T = T_in
  module ST = Set.Make(T_in)
end

I get the following error message referencing the above point in the
program.

Error: In this `with' constraint, the new definition of ST
       does not match its original definition in the constrained signature:
       ...
       Type declarations do not match:
         type t = Set.Make(T_in).t
       is not included in
         type t = Set.Make(T).t
       File "set.mli", line 68, characters 4-10: Expected declaration
       File "set.mli", line 68, characters 4-10: Actual declaration

It seems to me that since T = T_in, but applicative functors should make
the type of Set.Make(T) = Set.Make(T_in).  Does this not work this way?

Note that if I change the definition of S slightly, the same definition of
Make now type checks:

module type S = sig
  module T : Set.OrderedType
  module ST : Set.S with type elt = T.t
end

This solution is undesirable because I have a number of modules whose types
would require an excessive number of "with module ... = ..." constraints to
constrain in this way.  Is there a better way of getting this to type check?

Thank you,
Arlen

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

[-- Attachment #2: Type: text/html, Size: 2050 bytes --]

Re: [Caml-list] Applicative Functor Madness

[Arlen Cox]

[-- Attachment #1: Type: text/plain, Size: 2816 bytes --]

Based on some initial feedback, I'm providing some further information:

What I have is a whole bunch of functors that look like this:

module Make(S : OrderedType) = struct
  module SM = Map.Make(S)
  module SS = Set.Make(S)
  module SC = CustomFunctor.Make(S)
  (* where SC has exposed maps and sets in its interface *)
  ...
  (* many more similar modules/functors *)
  ...
  let foo () : SS.t =
    SC.run SS.empty
end

I don't really want to define the type of Make because I have to constrain
that SS, SM, and SC all preserve applicative identity in a type
constraint.  Then I have to do the same thing for every CustomFunctor as
well.  Worst, it's difficult to tell when things have been broken because
exactly which equality is missing is completely opaque in the type checking
-- especially when most of the uses of these modules is just plumbing (to
preserve applicative identity).

Thanks all,
Arlen

On Thu, Sep 20, 2018 at 10:29 AM Arlen Cox <arlencox@gmail.com> wrote:

> Hi everyone,
>
> I'm having some trouble getting some code that relies heavily on
> applicative functors to type check.  Does anyone know what I'm doing wrong
> with this?
>
> module type S = sig
>   module T : Set.OrderedType
>   module ST : module type of Set.Make(T)
> end
>
> module Make(T_in : Set.OrderedType) : S (* <- ERROR *)
>   with module T = T_in
>    and module ST = Set.Make(T_in)
> = struct
>   module T = T_in
>   module ST = Set.Make(T_in)
> end
>
> I get the following error message referencing the above point in the
> program.
>
> Error: In this `with' constraint, the new definition of ST
>        does not match its original definition in the constrained signature:
>        ...
>        Type declarations do not match:
>          type t = Set.Make(T_in).t
>        is not included in
>          type t = Set.Make(T).t
>        File "set.mli", line 68, characters 4-10: Expected declaration
>        File "set.mli", line 68, characters 4-10: Actual declaration
>
> It seems to me that since T = T_in, but applicative functors should make
> the type of Set.Make(T) = Set.Make(T_in).  Does this not work this way?
>
> Note that if I change the definition of S slightly, the same definition of
> Make now type checks:
>
> module type S = sig
>   module T : Set.OrderedType
>   module ST : Set.S with type elt = T.t
> end
>
> This solution is undesirable because I have a number of modules whose
> types would require an excessive number of "with module ... = ..."
> constraints to constrain in this way.  Is there a better way of getting
> this to type check?
>
> Thank you,
> Arlen
>
>
>

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

[-- Attachment #2: Type: text/html, Size: 3561 bytes --]

Re: [Caml-list] Applicative Functor Madness

[Jacques Garrigue]

A first remark: this use of module type of is probably not a good idea in the long term, as module type of is brittle, and its semantics could change.

Then why it doesn’t work: for soundness reasons, module aliases to functor arguments are not allowed, so actually in the body of the functor T and T_in are not equal, they are just modules with the same signature, so of course Set.Make(T).t and Set.Make(T_in).t are not equal.

A way around this limitation is to remove T from the return type:

module Make(T_in : Set.OrderedType) :
    S with module T := T_in and module ST = Set.Make(T_in)
  = struct module ST = Set.Make(T_in) end

Do you see a problem with this version?

Jacques Garrigue

On 2018/09/20 23:29, Arlen Cox wrote:
> 
> Hi everyone,
> 
> I'm having some trouble getting some code that relies heavily on applicative functors to type check.  Does anyone know what I'm doing wrong with this?
> 
> module type S = sig
>   module T : Set.OrderedType
>   module ST : module type of Set.Make(T)
> end
> 
> module Make(T_in : Set.OrderedType) : S (* <- ERROR *)
>   with module T = T_in
>    and module ST = Set.Make(T_in)
> = struct
>   module T = T_in
>   module ST = Set.Make(T_in)
> end
> 
> I get the following error message referencing the above point in the program.
> 
> Error: In this `with' constraint, the new definition of ST
>        does not match its original definition in the constrained signature:
>        ...
>        Type declarations do not match:
>          type t = Set.Make(T_in).t
>        is not included in
>          type t = Set.Make(T).t
>        File "set.mli", line 68, characters 4-10: Expected declaration
>        File "set.mli", line 68, characters 4-10: Actual declaration
> 
> It seems to me that since T = T_in, but applicative functors should make the type of Set.Make(T) = Set.Make(T_in).  Does this not work this way?
> 
> Note that if I change the definition of S slightly, the same definition of Make now type checks:
> 
> module type S = sig
>   module T : Set.OrderedType
>   module ST : Set.S with type elt = T.t
> end
> 
> This solution is undesirable because I have a number of modules whose types would require an excessive number of "with module ... = ..." constraints to constrain in this way.  Is there a better way of getting this to type check?
> 
> Thank you,
> Arlen
> 
> 



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

Re: [Caml-list] Applicative Functor Madness

[Arlen Cox]

[-- Attachment #1: Type: text/plain, Size: 3159 bytes --]

Hi Jacques,
Thank you for your reply.  I have some further questions inlined:


> A first remark: this use of module type of is probably not a good idea in
> the long term, as module type of is brittle, and its semantics could change.
>

Duly noted.


> Do you see a problem with this version?
>

Not immediately.  I'll have to think about what limitations that imposes on
my design.  It is good to know more of the rules.  Are the actual rules of
module equality documented somewhere in the OCaml manual?

It seems like Section 8.12 documents this (at least partially):

There are several restrictions on module-path:
>   1. it should be of the form M0.M1...Mn (i.e. without functor
> applications);
>   2. inside the body of a functor, M0 should not be one of the functor
> parameters;
>   3. inside a recursive module definition, M0 should not be one of the
> recursively defined modules.


Obviously in doing this inside a functor, I violated rule #2.  What I don't
understand is if there are clear syntactic rules, should there not be at
least a warning when the rules are violated?  Second, how does your
solution not still violate rule #1?

Thank you very much for your help,
Arlen


On 2018/09/20 23:29, Arlen Cox wrote:
> >
> > Hi everyone,
> >
> > I'm having some trouble getting some code that relies heavily on
> applicative functors to type check.  Does anyone know what I'm doing wrong
> with this?
> >
> > module type S = sig
> >   module T : Set.OrderedType
> >   module ST : module type of Set.Make(T)
> > end
> >
> > module Make(T_in : Set.OrderedType) : S (* <- ERROR *)
> >   with module T = T_in
> >    and module ST = Set.Make(T_in)
> > = struct
> >   module T = T_in
> >   module ST = Set.Make(T_in)
> > end
> >
> > I get the following error message referencing the above point in the
> program.
> >
> > Error: In this `with' constraint, the new definition of ST
> >        does not match its original definition in the constrained
> signature:
> >        ...
> >        Type declarations do not match:
> >          type t = Set.Make(T_in).t
> >        is not included in
> >          type t = Set.Make(T).t
> >        File "set.mli", line 68, characters 4-10: Expected declaration
> >        File "set.mli", line 68, characters 4-10: Actual declaration
> >
> > It seems to me that since T = T_in, but applicative functors should make
> the type of Set.Make(T) = Set.Make(T_in).  Does this not work this way?
> >
> > Note that if I change the definition of S slightly, the same definition
> of Make now type checks:
> >
> > module type S = sig
> >   module T : Set.OrderedType
> >   module ST : Set.S with type elt = T.t
> > end
> >
> > This solution is undesirable because I have a number of modules whose
> types would require an excessive number of "with module ... = ..."
> constraints to constrain in this way.  Is there a better way of getting
> this to type check?
> >
> > Thank you,
> > Arlen
> >
> >
>
>
>

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

[-- Attachment #2: Type: text/html, Size: 4479 bytes --]

Re: [Caml-list] Applicative Functor Madness

[Jacques Garrigue]

On 2018/09/21 10:25, Arlen Cox wrote:
> 
> Are the actual rules of module equality documented somewhere in the OCaml manual?

It seems you found them. Unfortunately, the OCaml manual does not provide a formal specification of OCaml, and it sometimes omits some implementation details. In this case I think it suffices.

> It seems like Section 8.12 documents this (at least partially):
> 
> There are several restrictions on module-path:
>   1. it should be of the form M0.M1...Mn (i.e. without functor applications);
>   2. inside the body of a functor, M0 should not be one of the functor parameters;
>   3. inside a recursive module definition, M0 should not be one of the recursively defined modules.
> 
> Obviously in doing this inside a functor, I violated rule #2.

Indeed

>  What I don't understand is if there are clear syntactic rules, should there not be at least a warning when the rules are violated?

The problem is that module aliases were only introduced recently, and reuse the syntax for module definitions.
While “module M = Arg” in a module is not typed as a module alias, it is still a module definition, and as such there is no reason to warn. (But you have a point that at least optionally warning about this could be a good idea.)
Another reason is that originally module aliases were introduced as an optimization to allow referring to other compilation units without including their whole type in the cmi. This is used in 4.07 to provide a Stdlib module, which contains just pointers to the modules of the standard library. From that point of view, it seemed reasonable to keep the same syntax.

>  Second, how does your solution not still violate rule #1?

Because it doesn’t use a module alias, but a destructive substitution.
A destructive substitution substitutes a module path for a path in the signature, removing this path.
Since it removes it, it doesn’t create an alias, and there is no need for restricting the form of the substituted path.
There are other restrictions on where this path is allowed to appear, and some signatures just cannot be inhabited, though.

Jacques Garrigue

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