Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Some bugs in generative functor #6581

Closed
vicuna opened this issue Sep 26, 2014 · 5 comments
Closed

Some bugs in generative functor #6581

vicuna opened this issue Sep 26, 2014 · 5 comments
Assignees
Milestone

Comments

@vicuna
Copy link

vicuna commented Sep 26, 2014

Original bug ID: 6581
Reporter: @garrigue
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2016-12-07T10:36:54Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.02.0
Target version: 4.02.1+dev
Fixed in version: 4.02.1+dev
Category: typing

Bug description

Reported by Mark Shinwell:

Problem 1 (see attached script): What is this Make(*)?
 File "incremental.ml", line 1:
 Error: The implementation incremental.ml
        does not match the interface incremental.cmi:
        In module Make:
        Modules do not match:
          functor () -> sig type 'a t end
        is not included in
          functor () -> Incremental_intf.S
        At position module Make(*) : <here>
        Modules do not match:
          sig type 'a t end
        is not included in
          Incremental_intf.S
        At position module Make(*) : <here>
        The value `sexp_of_t' is required but not provided
Problem 2 (see attached script): What is this Make(()), why do

we have generative functor application in type paths, and why does
building with -no-app-funct make this example work even though it
doesn't contain any applicative functor?

(Comment from Mark: as regards the error message at the end, I presume
it's two different instantiations of the functor. Maybe the error
messages should give some sort of numeric instantiation identifier, so
the user can see what's happening? I don't think we should ever give
an error that says "Type declarations do not match: FOO is not
included in FOO".)

 File "inline_tests_runner.ml", line 1:
 Error: The implementation inline_tests_runner.ml
        does not match the interface (inferred signature):
        ...
        At position
          module type S_Incremental_lib = sig module Std : <here> end
        Modules do not match:
          sig
            module Incremental :
              sig
                module Make :
                  functor () -> sig type 'a t = 'a

Incremental.Make(()).t end
end
end
is not included in
sig
module Incremental :
sig
module Make :
functor () -> sig type 'a t = 'a
Incremental.Make(()).t end
end
end
At position
module type S_Incremental_lib =
sig module Std : sig module Incremental : end end
Modules do not match:
sig
module Make :
functor () -> sig type 'a t = 'a Incremental.Make(()).t end
end
is not included in
sig
module Make :
functor () -> sig type 'a t = 'a Incremental.Make(()).t end
end
At position
module type S_Incremental_lib =
sig
module Std :
sig module Incremental : sig module Make : end end
end
Modules do not match:
functor () -> sig type 'a t = 'a Incremental.Make(()).t end
is not included in
functor () -> sig type 'a t = 'a Incremental.Make(()).t end
At position
module type S_Incremental_lib =
sig
module Std :
sig module Incremental : sig module Make(()) :
end end
end
Modules do not match:
sig type 'a t = 'a Incremental.Make(()).t end
is not included in
sig type 'a t = 'a Incremental.Make(()).t end
At position
module type S_Incremental_lib =
sig
module Std :
sig module Incremental : sig module Make(()) :
end end
end
Type declarations do not match:
type 'a t = 'a Incremental.Make(()).t
is not included in
type 'a t = 'a Incremental.Make(()).t

Problem 3: why can I have apply "struct end" to a functor that takes "()"?

module M() = struct end;;

include M(struct let x = 1 end);; (* doesn't type, ok *)

Error: This is a generative functor. It can only be applied to ()

include M(struct end);; (* types, unlike what the error above says, why?? *)

(Follow-up: we worked out that it seems "()" is an alias for "struct
end", but it seems confusing nonetheless.)

Problem 4 (see attached script): the given library compiles, but

only if the ALIAS line below is not commented out or if -no-app-funct
is not given on the command line. When it fails, it fails with:

File "incremental_unit_tests.ml", line 4, characters 10-29:
Error: This expression creates fresh types.
It is not allowed inside applicative functors.

So it looks like this library shouldn't compile, even with the alias
and without -no-app-funct.

File attachments

@vicuna
Copy link
Author

vicuna commented Sep 26, 2014

Comment author: @garrigue

Fixed in 4.02 at revision 15336.

Problem 1:
This is just a bug in the printing of the context: the parameter of generative functors has name "*".
When printing types this parameter is hidden, but here it was printed.

Problem 2:
Bug in the parser: in an early prototype the parameter was named "()" and it remained in the parser.
Fixed to "*".

Problem 3:
Indeed () is just an alias for struct end. Is forbidding it worth complicating the internal representation?

Problem 4:
Was a side-effect of 2: whether the name was "*" was used to determine whether the functor was generative of not, but here it ended up being "()"...

@vicuna
Copy link
Author

vicuna commented Oct 27, 2014

Comment author: @sliquister

By the way, there is the symmetric problem of problem 3:

module F(X : sig end) = ...
include F()

So essentially, the call site of a functor gives misleading information about the generativity of the functor (for those functors that are applied to struct end or ()).

One small argument in favor of a better representation is that ppx rewriters dealing with this part of the language have to know about the struct end hack (which is not documented in parsetree.mli by the way).

@vicuna
Copy link
Author

vicuna commented Oct 27, 2014

Comment author: @garrigue

So essentially, the call site of a functor gives misleading information about the generativity of the functor (for those functors that are applied to struct end or ()).

Actually, this is not the case: any functor applied to "()" (or any immediate structure) will behave generatively, notwithstanding whether it was defined as generative or applicative. This is precisely the rationale behind this syntax.

One small argument in favor of a better representation is that ppx rewriters dealing with this part of the language have to know about the struct end hack (which is not documented in parsetree.mli by the way).

Right. This should at least be documented.

@vicuna
Copy link
Author

vicuna commented Nov 7, 2014

Comment author: @sliquister

I don't think applying an applicative functor to (struct end) or () makes it generative when the appplication happens inside an other applicative functor. Example:

module F(X : sig end) = struct
type t
end
module G(X : sig end) = struct
include F()
end
module Empty = struct end
module A = G(Empty)
module B = G(Empty)
let _f (x : A.t) : B.t = x

If F was generative, G would have to be generative as well and A.t and B.t would be incompatible.

@vicuna
Copy link
Author

vicuna commented Nov 10, 2014

Comment author: @garrigue

OK, what you are saying is that if F is applicative, then we can still apply it to () inside an applicative functor, while this would be prohibited for a generative functor.
So actually, applying to () is only "locally generative", i.e. it will create new types, but not necessarily every time the functor is called.
This is true, but this does not break the semantics in any way: a generative functor can only be applied to (), and only inside a generative functor, which ensures that it is generative; there is neither of these restrictions on applicative functors, but if you respect them then they will behave generatively (since being generative is just that).

Seen another way, the point is that there is only one kind of functors, and they are applicative. But we can, at definition time, restrict some of them to be generative, which means you can only use them in generative contexts.

@vicuna vicuna closed this as completed Dec 7, 2016
@vicuna vicuna added the typing label Mar 14, 2019
@vicuna vicuna added this to the 4.02.1 milestone Mar 14, 2019
@vicuna vicuna added the bug label Mar 20, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants