Support automatic derivation of an hs-boot file from an hs file

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.,

{-# 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

mentioned in issue #1409

changed weight to 5

added Tfeature request Trac import backpack labels

changed the description

changed the description

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!

Replying to [ticket:9256#comment:84473 goldfire]:

Where is augustss's proposal in #1409? There's lots of text there.

I quoted his comment, but it's this one: #1409##9256 (closed)

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.)

Yep, the latter.

Are you proposing that every module, even in the absence of pragmas, now 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.

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?

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.

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!

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:

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?

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.

closed

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.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

added Pnormal label