Remove expansion from "unexpanded" module type of
#958
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Thanks Luke! Looks like it needs some rebasing (and maybe squashing?) |
lukemaurer
force-pushed
the
transparent-ascription
branch
from
49dfcdf to
88f484e
Compare
We've been keeping each `module type of` expression's expansion around, even in the nominally unexpanded version of the type. This was needed in case the expression was invalidated so that we had the expansion on hand as a fallback. However, it led to exponential blowup in the case of deeply nested `module type of`s. Happily, we can do without the expansion if we do a little more work when substituting: We already track in the `subst` which module paths have been invalidated. When we need to invalidate a module path, we can stash the expression for the module's type in that `subst`. This is effectively the same data that we were keeping in the "unexpanded" expansion. And then when we need to expand an invalidated `module type of`, we can use the stashed expression.
lukemaurer
force-pushed
the
transparent-ascription
branch
from
88f484e to
956f2ca
Compare
The resolution of `module type of` no longer need to be done incrementally and can be done while resolving module types in general. The `Type_of` module has no other purposes since the change in `U.TypeOf` and can be removed. Co-authored-by: Jon Ludlam <[email protected]>
|
With @jonludlam we figured that this makes the |
I like the idea of cutting down the test using
Can that be expressed neatly using |
Wow, reading the man page it's clear the answer to that question is nearly always "yes" :-) I'll cook something up |
In particular, in most cases it's crucial that the signature _not_ include the value `plus`, so we need to output the items in some form.
jonludlam
reviewed
May 18, 2023
src/xref2/subst.ml
Outdated
| @@ -142,6 +142,15 @@ let rename_class_type : Ident.path_class_type -> Ident.path_class_type -> t -> t | |||
| t.type_; | |||
| } | |||
|
|
|||
| let u_module_type_expr_of_module_type_expr (e : Component.ModuleType.expr) : | |||
There was a problem hiding this comment.
There's a similar function here: https://github.com/ocaml/odoc/blob/master/src/model/lang.ml#L533-L538
|
Found a bug. Converting back to draft for the moment. |
Given
```
module type S = sig
module A : <some module type expr>
module B : module type of A
end
module type S' = S with module A := M
```
we now have a nice story for invalidating `A` in the type of `B` and moving
`A`'s type over, evaluating `S'` to
```
sig
module B : <some module type expr>
end
```
There is, however, a problem if `B`'s type is something more complicated:
```
module type S = sig
module A : <some module type expr>
module B : module type of A.F
end
module type S' = S with module A := M
```
What can we evaluate `S'` to? We don't have a way to say
```
sig
module B : <some module type expr>.F
end
```
Note that `A` is gone - there is no name for it or its type anymore, so there's
no path `P` on which we can build `P.F`. If the type of `A` is something nice
like a signature, we can project `F` out, but it might not be that simple. And
we can't count on having an expansion for `A` or `B` on hand (anymore), so if
`<some module type expr>` is just a path, we're sunk: there's no syntax to
project a field out of a path to a module _type_. Even worse, `B`'s type could
be `module type of A(X)`, which we do _not_ want to sort out in the middle of
`subst.ml`.
The solution is simply to allow `<some module type expr>.F` and `<some module
type expr>(X)` as module type expressions after all. Specifically, both
`ModuleType.expr` and `ModuleType.U.expr` now have a `Project` constructor that
takes a _projection_, essentially a path suffix including submodule names and
arguments to pass, and a general module type expression. These projections are
easy to evaluate given the expansion of the expression, and thus they're easy to
compile away when computing expansions.
The only problem at the moment is that `ModuleType.U.expr` doesn't have a
`Functor` constructor, which means this patch can't handle
```
module type S = sig
module A : functor (X : T) -> U
module B : sig
include module type of struct include A(M) end
end
end
module type S' = S with module A := F
```
because `module type of struct include A(M)` will be a `ModuleType.U.expr` and
substitution needs to produce `((functor (X : T) -> U)(M))` which is not a
`ModuleType.U.expr` because `(functor (X : T) -> U)` isn't a functor literal.
My current plan is simply to add `Functor` as a constructor to
`ModuleType.U.expr`, which (IMO) has the added benefit of removing the awkward
asymmetry between `ModuleType.expr` and `ModuleType.U.expr`.
Required so that `Project(`Apply(`Here, path), expr` can be a `ModuleType.U.expr`.
Given
```
module type S = sig
module A : T
module type M : sig
include module type of struct include A end
end
end
module type P = S with module A = Int
```
we need to give `P.M` a strange type: `T` strengthened at `Int`. The
substitution operation has no way of computing this module type, so as with
`Project`, we need a new operator in the module-type language.
The original mechanism for dealing with substitution into unexpanded `module type of` expressions was to have them secretly be expanded after all and swap in the expansion when necessary. This necessarily meant that such a substitution always produced an expanded type - that is, either a signature or a functor whose body is a signature. This branch avoids this mechanism and can therefore produce a more informative type. It's not clear that this is an improvement, however, since it means the HTML can say something like `include T` when the user wrote no such thing. The old behaviour always produced `include sig ... end` instead (which _unambiguously_ wasn't something in the source). It's easy to go back to the old behaviour, however, simply by using the expansion when it's available. There are still cases where there's no expansion immediately available but we'd still rather say `sig ... end`: namely, if `Subst` has added a projection or strengthening operation, it will erase the expansion, so this mechanism won't kick in. However, these cases are currently always rendered as `include sig ... end` anyway. A more robust mechanism might be to simply add (yet) another constructor to the `ModuleType.expr` and `ModuleType.U.expr` grammars to explicitly mark that a sigature's inline form should always be rendered as `include sig ... end` (that is, that `is_elidable_with_u` in `generator.ml` should return `true`).
These are only generated when substituting into unexpanded module types, so the constructor for the expanded form was never actually used. The same can be said for `Strengthen`, but that's much more likely to see use in the future.
|
This is superceded by #1081 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We've been keeping each
module type ofexpression's expansion around, even in the nominally unexpanded version of the type. This was needed in case the expression was invalidated so that we had the expansion on hand as a fallback. However, it led to exponential blowup in the case of deeply nestedmodule type ofs.Happily, we can do without the expansion if we do a little more work when substituting: We already track in the
substwhich module paths have been invalidated. When we need to invalidate a module path, we can stash the expression for the module's type in thatsubst. This is effectively the same data that we were keeping in the "unexpanded" expansion. And then when we need to expand an invalidatedmodule type of, we can use the stashed expression.