Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Preparing Dhall.Import for "Semi-semantic" caching #1113

Merged
merged 16 commits into from
Jul 17, 2019

Conversation

EggBaconAndSpam
Copy link
Collaborator

@EggBaconAndSpam EggBaconAndSpam commented Jul 15, 2019

This PR consists of a number of smaller changes I would like to make to Dhall.Import to prepare for the next step, which is to reorganise the code to load imports recursively. I copy the commit messages of the two main commits below.

There are a few questions that came up along the way:

  • I believe Local parent (File (Directory dir) file) to be equivalent to Local Here (File (Directory (".." : dir)) file); if that is the case, could we not just get rid of the Parent constructor entirely?
  • Is there a reason for using throwIO as well as throwM, and not simply sticking with the latter?

Finally, I feel that 'resolved' would be the best way to describe fully 'chained' imports whose headers have been typechecked and normalised, in analogy to 'DNS resolution'; Chained is very much a compromise. It is a shame that Resolved was already appropriated to mean something a bit more vague... ;)

Commit: Add Chained type to capture fully chained imports

Until now we used Import two mean two different things:

  • The syntactic construct; e.g. ./a.dhall corresponds to the following
    AST:

    Embed
      (Import
        (ImportHashed Nothing (Local Here (Directory ["."]) "a.dhall"))
        Code)
    
  • The physical location the import is pointing to, computed by
    'chaining' the syntactical import with the the 'physical' parent import.
    For example the syntactic import ./a.dhall might actually refer to the
    remote file http://host/directory/a.dhall.

This commit adds a Chained newtype on top of Import to make this
distinction explicit at type level.

Commit: Typecheck and normalise http headers earlier

Previously we would typecheck and normalise http headers in
exprFromImport, i.e. while loading the import. This commit adds the
invariant that any headers in 'Chained' imports are already typechecked
and normalised, and moves this step into loadWith accordingly.

This causes a subtle difference in behaviour when importing remote files
with headers as Location: previously, nonsensical expressions like
http://a using (0 0) as Location were valid, while they would now cause
a type error.

Frederik Ramcke added 5 commits July 15, 2019 13:13
Until now we used `Import` two mean two different things:
- The syntactic construct; e.g. `./a.dhall` corresponds to the following
  AST:
  ```
  Embed
    (Import
      (ImportHashed Nothing (Local Here (Directory ["."]) "a.dhall"))
      Code)
  ```

- The physical location the import is pointing to, computed by
'chaining' the syntactical import with the the 'physical' parent import.
For example the syntactic import `./a.dhall` might actually refer to the
remote file `http://host/directory/a.dhall`.

This commit adds a `Chained` newtype on top of `Import` to make this
distinction explicit at type level.
I claim that `HTTPHeaders` is more readable and informative than the
unfolded type `(CI ByteString, ByteString)`.
Previously we would typecheck and normalise http headers in
`exprFromImport`, i.e. while loading the import. This commit adds the
invariant that any headers in 'Chained' imports are already typechecked
and normalised, and moves this step into `loadWith` accordingly.

This causes a subtle difference in behaviour when importing remote files
with headers `as Location`: previously, nonsensical expressions like
`http://a using 0 0 as Location` were valid, while they would now cause
a type error.
dhall/src/Dhall/Import.hs Show resolved Hide resolved
dhall/src/Dhall/Import/Types.hs Outdated Show resolved Hide resolved
Frederik Ramcke added 5 commits July 16, 2019 11:09
Do not expose the `Chained` constructor; we don't want external code
breaking our invariants! Also further clarifies the comment describing
the `Chained` type.
Since we are no longer able to construct `Chained` imports directly we
need to export a few additional helper functions from Dhall.Import.
Furthermore, since VSCode (and presumably the other editors out there
implementing the LSP protocol) does not support opening remote files
anyway we can get rid of some complications by dropping support for
remote files entirely on the back-end.
@Gabriella439
Copy link
Collaborator

@f-f: See the Travis failure on this pull request. The build appears to time out during uploading the cache: https://travis-ci.org/dhall-lang/dhall-haskell/builds/559476240

dhall/src/Dhall/Import.hs Outdated Show resolved Hide resolved
@f-f
Copy link
Member

f-f commented Jul 16, 2019

@Gabriel439 oh wow. Caches are 800MB in size, which is less than what we get in Spago, but it's the first time I see this error. I tried removing caching for ~/.local/bin, which isn't really needed

@EggBaconAndSpam
Copy link
Collaborator Author

There are a few questions that came up along the way:

* I believe `Local parent (File (Directory dir) file)` to be equivalent to `Local Here (File (Directory (".." : dir)) file)`; if that is the case, could we not just get rid of the `Parent` constructor entirely?

* Is there a reason for using `throwIO` as well as `throwM`, and not simply sticking with the latter?

Any insights on this, @Gabriel439?

@mergify mergify bot merged commit d5d0224 into master Jul 17, 2019
@mergify mergify bot deleted the frederik/resolve-imports branch July 17, 2019 15:21
@Gabriella439
Copy link
Collaborator

I believe Local parent (File (Directory dir) file) to be equivalent to Local Here (File (Directory (".." : dir)) file); if that is the case, could we not just get rid of the Parent constructor entirely?

See: #718

Is there a reason for using throwIO as well as throwM, and not simply sticking with the latter?

As far as I know, we use throwM for code that is polymorphic over MonadThrow and throwIO for code that is either IO or polymorphic over MonadIO.

For the case of IO code, there's no particular reason we prefer throwIO over throwM. It's just that a lot of that code predates the use of MonadThrow in Dhall.Import

@EggBaconAndSpam
Copy link
Collaborator Author

Thanks for the clarifications!

@Gabriella439
Copy link
Collaborator

Gabriella439 commented Jul 17, 2019

@EggBaconAndSpam: You're welcome! 🙂

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants