[GHC] #9256: Support automatic derivation of an hs-boot file from an hs file
I would settle for a solution where I annotate those entities in a module that would go in the hs-boot file. So instead of me having to go
#9256: Support automatic derivation of an hs-boot file from an hs file ------------------------------------+------------------------------------- Reporter: ezyang | Owner: ezyang Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: backpack | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- This is essentially augustss's proposal from ticket #1409: I would settle for a solution where I annotate those entities in a module that would go in the hs-boot file. So instead of me having to go through the trouble of creating an extra file I could just say, e.g., Replying to [comment:13 augustss]: through the trouble of creating an extra file I could just say, e.g.,
{{{ {-# MODULE_MUTUAL_RECURSION_BREAKER T, foo #-} data T = ... foo :: ... foo = ... }}}
The values that have an annotation would have to have a type signature.
This should be eminently doable. Here is a more fleshed out proposal. First, consider the definition of an hs-boot file in the absence of mutual recursion (i.e. no breakers are necessary). In this case, the hi-boot file for an hs file is precisely the hi file produced after ordinary renaming and typechecking of the module. As an optimization, we would like to avoid typechecking definitions if an explicit type signature is present (if the type signature is absent, we have no choice.) There are a few choices here: we can force users to give top-level declarations for all exported functions (so unconditionally error if something is missing, by filtering out the relevant value declarations from the source), or we can go ahead and do full typechecking when the signature is missing. (The former is probably the simplest.) Now, how to handle breakers? We need to avoid typechecking them, since their recursive dependence means that they would not type check properly. So we should also filter out their type signatures. (Furthermore, if we are inferring some signatures, we need to make sure that their definitions don't rely on any breakers. For this reason, it is probably simplest to just require explicit type signatures.) If the mechanism for specifying breakers is exclusionary (as opposed to an inclusionary method of saying what values are in the signature), there is an awkward problem of syntax for exporting only an abstract type: the logical choices mean the wrong thing (`T(..)` seem to imply the type is eliminated entirely, whereas `T` seems to imply that the type should be eliminated, but not eh constructors.) Summary: 1. Require top-level signatures in hs to hs-boot files(?) 2. Exclusionary or inclusionary signature pragma? 3. Filter out value declarations and excluded files, then rename/typecheck as normal, producing hi-boot file -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9256 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9256: Support automatic derivation of an hs-boot file from an hs file -------------------------------------+------------------------------------ Reporter: ezyang | Owner: ezyang Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Description changed by ezyang: Old description:
This is essentially augustss's proposal from ticket #1409:
I would settle for a solution where I annotate those entities in a module that would go in the hs-boot file. So instead of me having to go through the trouble of creating an extra file I could just say, e.g.,
I would settle for a solution where I annotate those entities in a module that would go in the hs-boot file. So instead of me having to go
Replying to [comment:13 augustss]: through the trouble of creating an extra file I could just say, e.g.,
{{{ {-# MODULE_MUTUAL_RECURSION_BREAKER T, foo #-} data T = ... foo :: ... foo = ... }}}
The values that have an annotation would have to have a type signature.
This should be eminently doable. Here is a more fleshed out proposal.
First, consider the definition of an hs-boot file in the absence of mutual recursion (i.e. no breakers are necessary). In this case, the hi- boot file for an hs file is precisely the hi file produced after ordinary renaming and typechecking of the module.
As an optimization, we would like to avoid typechecking definitions if an explicit type signature is present (if the type signature is absent, we have no choice.) There are a few choices here: we can force users to give top-level declarations for all exported functions (so unconditionally error if something is missing, by filtering out the relevant value declarations from the source), or we can go ahead and do full typechecking when the signature is missing. (The former is probably the simplest.)
Now, how to handle breakers? We need to avoid typechecking them, since their recursive dependence means that they would not type check properly. So we should also filter out their type signatures. (Furthermore, if we are inferring some signatures, we need to make sure that their definitions don't rely on any breakers. For this reason, it is probably simplest to just require explicit type signatures.)
If the mechanism for specifying breakers is exclusionary (as opposed to an inclusionary method of saying what values are in the signature), there is an awkward problem of syntax for exporting only an abstract type: the logical choices mean the wrong thing (`T(..)` seem to imply the type is eliminated entirely, whereas `T` seems to imply that the type should be eliminated, but not eh constructors.)
Summary:
1. Require top-level signatures in hs to hs-boot files(?) 2. Exclusionary or inclusionary signature pragma? 3. Filter out value declarations and excluded files, then rename/typecheck as normal, producing hi-boot file
I would settle for a solution where I annotate those entities in a module that would go in the hs-boot file. So instead of me having to go
New description: This is essentially augustss's proposal from ticket #1409: Replying to [comment:13 augustss]: through the trouble of creating an extra file I could just say, e.g.,
{{{ {-# MODULE_MUTUAL_RECURSION_BREAKER T, foo #-} data T = ... foo :: ... foo = ... }}}
The values that have an annotation would have to have a type signature.
This should be eminently doable. Here is a more fleshed out proposal. First, consider the definition of an hs-boot file in the absence of mutual recursion (i.e. no breakers are necessary). In this case, the hi-boot file for an hs file is precisely the hi file produced after ordinary renaming and typechecking of the module. As an optimization, we would like to avoid typechecking definitions if an explicit type signature is present (if the type signature is absent, we have no choice.) There are a few choices here: we can force users to give top-level declarations for all exported functions (so unconditionally error if something is missing, by filtering out the relevant value declarations from the source), or we can go ahead and do full typechecking when the signature is missing. (The former is probably the simplest.) Now, how to handle breakers? We need to avoid typechecking them, since their recursive dependence means that they would not type check properly. So we should also filter out their type signatures. (Furthermore, if we are inferring some signatures, we need to make sure that their definitions don't rely on any breakers. For this reason, it is probably simplest to just require explicit type signatures.) If the mechanism for specifying breakers is exclusionary (as opposed to an inclusionary method of saying what values are in the signature), there is an awkward problem of syntax for exporting only an abstract type: the logical choices mean the wrong thing (`T(..)` seem to imply the type is eliminated entirely, whereas `T` seems to imply that the type should be eliminated, but not eh constructors.) Summary: 1. Require top-level signatures in hs to hs-boot files(?) 2. Exclusionary or inclusionary signature pragma? 3. Filter out value declarations and excluded files, then rename/typecheck as normal, producing hi-boot file -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9256#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9256: Support automatic derivation of an hs-boot file from an hs file -------------------------------------+------------------------------------ Reporter: ezyang | Owner: ezyang Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Description changed by ezyang: Old description:
This is essentially augustss's proposal from ticket #1409:
I would settle for a solution where I annotate those entities in a module that would go in the hs-boot file. So instead of me having to go
Replying to [comment:13 augustss]: through the trouble of creating an extra file I could just say, e.g.,
{{{ {-# MODULE_MUTUAL_RECURSION_BREAKER T, foo #-} data T = ... foo :: ... foo = ... }}}
The values that have an annotation would have to have a type signature.
This should be eminently doable. Here is a more fleshed out proposal.
First, consider the definition of an hs-boot file in the absence of mutual recursion (i.e. no breakers are necessary). In this case, the hi- boot file for an hs file is precisely the hi file produced after ordinary renaming and typechecking of the module.
As an optimization, we would like to avoid typechecking definitions if an explicit type signature is present (if the type signature is absent, we have no choice.) There are a few choices here: we can force users to give top-level declarations for all exported functions (so unconditionally error if something is missing, by filtering out the relevant value declarations from the source), or we can go ahead and do full typechecking when the signature is missing. (The former is probably the simplest.)
Now, how to handle breakers? We need to avoid typechecking them, since their recursive dependence means that they would not type check properly. So we should also filter out their type signatures. (Furthermore, if we are inferring some signatures, we need to make sure that their definitions don't rely on any breakers. For this reason, it is probably simplest to just require explicit type signatures.)
If the mechanism for specifying breakers is exclusionary (as opposed to an inclusionary method of saying what values are in the signature), there is an awkward problem of syntax for exporting only an abstract type: the logical choices mean the wrong thing (`T(..)` seem to imply the type is eliminated entirely, whereas `T` seems to imply that the type should be eliminated, but not eh constructors.)
Summary:
1. Require top-level signatures in hs to hs-boot files(?) 2. Exclusionary or inclusionary signature pragma? 3. Filter out value declarations and excluded files, then rename/typecheck as normal, producing hi-boot file
I would settle for a solution where I annotate those entities in a module that would go in the hs-boot file. So instead of me having to go
New description: This is essentially augustss's proposal from ticket #1409: through the trouble of creating an extra file I could just say, e.g.,
{{{ {-# MODULE_MUTUAL_RECURSION_BREAKER T, foo #-} data T = ... foo :: ... foo = ... }}}
The values that have an annotation would have to have a type signature.
This should be eminently doable. Here is a more fleshed out proposal. First, consider the definition of an hs-boot file in the absence of mutual recursion (i.e. no breakers are necessary). In this case, the hi-boot file for an hs file is precisely the hi file produced after ordinary renaming and typechecking of the module. As an optimization, we would like to avoid typechecking definitions if an explicit type signature is present (if the type signature is absent, we have no choice.) There are a few choices here: we can force users to give top-level declarations for all exported functions (so unconditionally error if something is missing, by filtering out the relevant value declarations from the source), or we can go ahead and do full typechecking when the signature is missing. (The former is probably the simplest.) Now, how to handle breakers? We need to avoid typechecking them, since their recursive dependence means that they would not type check properly. So we should also filter out their type signatures. (Furthermore, if we are inferring some signatures, we need to make sure that their definitions don't rely on any breakers. For this reason, it is probably simplest to just require explicit type signatures.) If the mechanism for specifying breakers is exclusionary (as opposed to an inclusionary method of saying what values are in the signature), there is an awkward problem of syntax for exporting only an abstract type: the logical choices mean the wrong thing (`T(..)` seem to imply the type is eliminated entirely, whereas `T` seems to imply that the type should be eliminated, but not eh constructors.) Summary: 1. Require top-level signatures in hs to hs-boot files(?) 2. Exclusionary or inclusionary signature pragma? 3. Filter out value declarations and excluded files, then rename/typecheck as normal, producing hi-boot file -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9256#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9256: Support automatic derivation of an hs-boot file from an hs file -------------------------------------+------------------------------------ Reporter: ezyang | Owner: ezyang Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Don't let this hold you up, but I can't really understand the proposal above. Where is augustss's proposal in #1409? There's ''lots'' of text there. What is a "mutual recursion breaker"? Is it something that ''does'' appear in the hi-boot file? Or is it something that ''does not'' appear in the hi-boot file? (Sounds like the latter.) Are you proposing that every module, even in the absence of pragmas, now produce both a hi and a hi-boot file? Your proposal suggests that every top-level definition will now need a type signature, but I don't imagine you mean that. Is this only when some pragma is specified? Then, not quite understanding what breakers are, my understanding goes downhill from there. In your summary, is there something that distinguishes a "hs to hs-boot file" from a normal hs file? Sorry -- this is interesting to me, but I'm a little lost here. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9256#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9256: Support automatic derivation of an hs-boot file from an hs file -------------------------------------+------------------------------------ Reporter: ezyang | Owner: ezyang Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by ezyang): Replying to [comment:3 goldfire]:
Where is augustss's proposal in #1409? There's ''lots'' of text there.
What is a "mutual recursion breaker"? Is it something that ''does'' appear in the hi-boot file? Or is it something that ''does not'' appear in
Are you proposing that every module, even in the absence of pragmas, now
Your proposal suggests that every top-level definition will now need a type signature, but I don't imagine you mean that. Is this only when some
I quoted his comment, but it's this one: https://ghc.haskell.org/trac/ghc/ticket/1409#comment:13 the hi-boot file? (Sounds like the latter.) Yep, the latter. produce both a hi and a hi-boot file? Hm, that's probably bad. It should only generate an hi-boot file if there is some pragma. pragma is specified? Yep.
Then, not quite understanding what breakers are, my understanding goes downhill from there.
In your summary, is there something that distinguishes a "hs to hs-boot file" from a normal hs file?
Sorry -- this is interesting to me, but I'm a little lost here. Thanks!
So let's be a bit more concrete about the use case. 1. You're writing a pair of modules A and B, and you realize that you want some mutual recursion. 2. In the old world order, you'd pick one module to be loop-breaker (say A), create a boot file (A.hs-boot), and modify B's import to be a SOURCE import. 3. In the new world order, you instead add a pragma to A.hs which specifies which identifies would have been placed in the A.hs-boot file. B still receives a SOURCE import as before. 4. Now, when performing `--make` compilation, we notice that A.hs has a pragma, so we pretend as if an hs-boot file existed, and first compile A.hs as a boot file, then compiling B.hs and then A.hs normally. I haven't worked out how to adjust one-shot compilation to work with this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9256#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9256: Support automatic derivation of an hs-boot file from an hs file -------------------------------------+------------------------------------ Reporter: ezyang | Owner: ezyang Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Thanks. Let me try to spit back what you're saying: {{{ module A where import B data Arf = MkArf (Maybe Bar) }}} {{{ module B where import A data Bar = MkBar (Maybe Arf) }}} The above modules will currently fail to compile because of the import cycle. The current solution is to write an ''A.hs-boot'' file declaring `data Arf` and putting a `{-# SOURCE #-}` pragma in `B`. Your proposed solution is like this: {{{ module A where {-# BOOT_TYPES Arf #-} import B data Arf = MkArf (Maybe Bar) }}} {{{ module B where import {-# SOURCE #-} A data Bar = MkBar (Maybe Arf) }}} Is this correct? I like the idea in general, but there are some pitfalls I see: * An hs-boot file tends to have a mix of `{-# SOURCE #-}` imports and regular imports. The list of imports in the hs-boot file will be different than the list in the master file, and where the `{-# SOURCE #-}` pragma appears will be different. (There's a subset relationship between the import lists, of course.) How will this new syntax figure out which imports are necessary to type check the `BOOT_TYPES`? * It is sometimes desirable to include type ''definitions'' in hi-boot files. How does this syntax accommodate that need? * Similarly, one may want type synonyms and type families available in hi- boot files. How do these work? Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9256#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
An hs-boot file tends to have a mix of `{-# SOURCE #-}` imports and regular imports. The list of imports in the hs-boot file will be different
#9256: Support automatic derivation of an hs-boot file from an hs file -------------------------------------+------------------------------------ Reporter: ezyang | Owner: ezyang Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by ezyang): Bikeshedding syntax a little bit, here are two alternate way A.hs could be written: Inline annotations: {{{ module A where import B data Arf = MkArf (Maybe Bar) {-# BOOT_ABSTRACT #-} }}} Exclusionary (but as mentioned before, this syntax is a little problematic): {{{ module A where {-# BOOT_EXCLUDE Arf(..) #-} import B data Arf = MkArf (Maybe Bar) }}} Now to answer your questions: than the list in the master file, and where the `{-# SOURCE #-}` pragma appears will be different. (There's a subset relationship between the import lists, of course.) How will this new syntax figure out which imports are necessary to type check the `BOOT_TYPES`? I imagine we'll have to augment the syntax to get all of the necessary information: I don't think it would be right to automatically compute it. However, I think the most common case is that of a simple mutual recursive group of two modules, in which case no changes to the imports are necessary. So I don't mind if the syntax just says directly, "This is a concrete import in the hs version, but a source import in the hs-boot version." (In Backpack-land, this case is probably common enough that it merits a shortcut.
It is sometimes desirable to include type definitions in hi-boot files. How does this syntax accommodate that need?
I am not really sure what you mean by type definitions here, but surely they must still be defined in some way in the source file? Then we can annotate it to say that it should be included in the boot. Ditto with type synonyms and type families. I agree, there's a lot of syntax to be bikeshed here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9256#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9256: Support automatic derivation of an hs-boot file from an hs file -------------------------------------+------------------------------------- Reporter: ezyang | Owner: ezyang Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: invalid | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by ezyang): * status: new => closed * resolution: => invalid Comment: I'm going to terminate this proposal: the crux of the issue is that you really do want the imports of the new hs-boot file to be computed automatically. I think I have a way to deal with this, but it really is a different proposal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9256#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC