#12994: Module and export level signature thinning in Backpack -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by ezyang: @@ -17,2 +17,1 @@ - it does not have any modules, and itself depends only on fully - instantiated packages or signature packages. + it does not export any modules. @@ -29,2 +28,3 @@ - By default, all signatures in scope at a name get merged to a name. We add - a pragma for controlling what declarations from packages get merged in: + By default, all signatures in scope at a name get merged to a name. + However, by specifying the export list of a signature, we can control + which declarations from signature packages come into scope: @@ -33,2 +33,1 @@ - signature A where - {-# MERGE "sig-pkg" (T, S, foo, bar, baz) #-} + signature A (T, foo) where @@ -36,1 +35,0 @@ - qux :: T -> T @@ -39,2 +37,4 @@ - This line means, "merge in the declarations T, foo, bar, baz from the - signature in sig-pkg." Two things to note: + Notice that `foo` is not mentioned in the body of the signature A: in this + case, foo is expected to come from a signature from a signature package. + If the signature from the signature package also require bar, that + requirement is NOT included in A. @@ -42,1 +42,3 @@ - 1. If `foo :: S`, you're obligated to also declare `S` in the import list, + Two things to note: + + 1. If `foo :: S`, you're obligated to also declare `S` in the export list, @@ -44,1 +46,2 @@ - always explicit what is going to be required in the end. + always explicit what is going to be required in the end. GHC will give an + error if this is not true. @@ -46,13 +49,5 @@ - 2. Even if `T` is in the merge list, you still have to declare it locally - if you want to make use of it. These are not imports! - - (:TODO: There is no provision for disambiguating between two signatures - from the same package, but mix-linked differently. This seems like a - pretty rare case.) - - The semantics is that we proceed as we do now, but when merging, we apply - the explicit import list to reduce the set of entities we actually - typecheck and merge in (checking, however, to ensure that these are all - well-formed.) - - That's it, I think. + 2. If you depended upon a library that had requirements and exposed + modules, you can't thin declarations from the signature this way: they are + always exported, no matter if they're specified in the export list or not. + But we'll attach warnings to these if you actually try to use them. (Maybe + we really should filter them out of things that are brought into scope) New description: **The problem.** We want to write signature packages to allow us to reuse signatures, but Backpack in its current incarnation forces us to depend on ALL of the signatures from the signature package. This is troublesome if we only really needed a subset of the signatures from the package. What we'd like is a way to "thin" out the signatures, keeping only the ones we need. In the original design of Backpack, this was not allowed, because if a signature was requiring a function so that a module from that package could use it, you're not permitted to just drop that requirement (someone really needs it!) But signature packages: packages that consist of only signatures (no modules) do not have any such requirement. So let's allow module and export level signature thinning here. **Design.** First, during the course of mix-in linking we infer if a package is a signature package or not. A package is a signature package if it does not export any modules. A signature package is eligible for requirement thinning. A signature package can be thinned at the module level using the `signature-mixins` field, by saying `include-signatures: sig-pkg (A)` (we don't reuse `mixins` field to distinguish signature packages from regular indefinite packages); this means that we only are bringing the signature `A` into scope. If `A` imports another signature `B`, the user is obligated to also bring that signature into scope (if they do not, we will error, although this can only be done by GHC.) By default, all signatures in scope at a name get merged to a name. However, by specifying the export list of a signature, we can control which declarations from signature packages come into scope: {{{ signature A (T, foo) where data T }}} Notice that `foo` is not mentioned in the body of the signature A: in this case, foo is expected to come from a signature from a signature package. If the signature from the signature package also require bar, that requirement is NOT included in A. Two things to note: 1. If `foo :: S`, you're obligated to also declare `S` in the export list, even if you are not otherwise using it. The reason for this is to make it always explicit what is going to be required in the end. GHC will give an error if this is not true. 2. If you depended upon a library that had requirements and exposed modules, you can't thin declarations from the signature this way: they are always exported, no matter if they're specified in the export list or not. But we'll attach warnings to these if you actually try to use them. (Maybe we really should filter them out of things that are brought into scope) -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12994#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler