Re: [Caml-list] Applicative Functor Madness

[Arlen Cox <arlencox@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2938 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
> >
> >
>
>
>

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