Changes between Version 6 and Version 7 of Ticket #10681


Ignore:
Timestamp:
Jul 31, 2015 12:59:01 AM (2 years ago)
Author:
ezyang
Comment:

Updated description with some remarks about handling type system features which are not supported by boot files.

@goldfire: Intuitively, it seems like if you can figure out your universe hierarchy, you can just write as many levels of hs-boot files as you need. Unfortunately, because types and kinds are syntactically merged in your nokinds branch, it's not immediately obvious prior to typechecking what the universes are (the pain of de-stratifying!) which makes it much more difficult to plan compilation. So it seems like it would be much simpler to just not include these types of declarations in hs-boot files.

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #10681 – Description

    v6 v7  
    66662. This facility actually makes `{-# SOURCE #-}` a lot more attractive for increasing separate compilation: you can mark an import `{-# SOURCE #-}` to ensure that if its implementation changes, you don't have to recompile this module / you can build the module in parallel with that module.  The downside is that when the imported file is modified, we have to regenerate the `hs-boot` stub before we conclude that the types have not changed (as opposed to with separate `hs-boot` files, where a modification to `hs` would not bump the timestamp on `hs-boot`.
    6767
    68 3. This seems to definitely suggest that you should never need more than two levels of hs-boot nesting, or perhaps three with kinding. (But maybe someone has a fancy type system feature for which this is not true!)  Maybe this applies to signature files too.
     683. With Haskell98, you should never need more than two levels of hs-boot nesting.  However, with data kind promotion, you may need arbitrarily many levels of nesting. You could simply exclude promoted data kinds ala **Handling unsupported boot features**; however an alternate thing to do is generalize hs-boot to arbitrarily many levels. However, this might be annoying to implement because dependency analysis needs to know how to determine universe stratification so it can tell how many levels of hs-boot are necessary.
    6969
    70704. We can't force the first level of `hs-boot` files to be abstract types, for two reasons: (1) a source file importing the hs-boot file may really need the selector/constructor, and (2) the `hs-boot` files will reflect any cycles from the source files, that's no good! Rolling out to the second level breaks the cycle because abstract types never need any imports.
     
    8080}}}
    8181   In this case, `C` would NOT see the `Eq` instance for functions defined in `A`.
     82
     83**Handling unsupported boot features.**  Some type-level features in Haskell are not supported at the boot-level (type families, etc), so the automatic generation of `hs-boot` needs a way of transitively(!) excluding these definitions from `hs-boot` files.  We can exclude things from the boot file in the following way:
     84
     851. If a declaration is not liftable to the `hs-boot` file, we replace it with a "not bootable" declaration, which specifies that there is something with this `Name`, but we don't have any information about it. (This is a sort of generalized version of an abstract type).
     86
     872. If we are type-checking a declaration and make reference to a not bootable declaration, the full declaration itself is considered not bootable.
     88
     89Alternately, we can just make sure all language features are supported in boot files.