Re: [Caml-list] Applicative Functor Madness

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

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