Implement importing paths as Location #585

f-f · 2019-06-10T05:54:24Z

This standardizes native support for reading import locations into Dhall, as specified by @Gabriel439 in #71 (comment)

So e.g. if you do

./some/import as Location

..then you'd have it read in Dhall as

< Local : Text | Remote : Text | Environment : Text | Missing >.Local "./some/import"

The main reason why this is useful as a builtin is that we can exploit the canonicalization and chaining that Dhall uses for imports so that relative paths stay correct over relative importing of other Dhall expressions. This sounds like a mouthful, so here's an example (there is also a test about this):

if ./nested/import.dhall contains missing
if ./nested/importLocation.dhall contains ./import.dhall as Location
and here.dhall contains ./nested/importLocation.dhall (note that this is a normal import)
then resolving here.dhall in the current directory will give:

< Local : Text | Remote : Text | Environment : Text | Missing >.Local "./nested/import.dhall"

-- Note: `./nested/import.dhall` is never resolved!

I also noted that missing will not fail to resolve when imported as Location, so e.g. the ? operator will not have the usual behaviour (there's a test about this too)

(missing as Location) ? 42

-- This resolves to:
< Local : Text | Remote : Text | Environment : Text | Missing >.Missing

Things I'm unsure of in this PR:

I was lazy and did not introduce a judgement to convert from non-Dhall import locations to the Dhall value containing the import location. I'm also afraid this might mean formalizing how imports need to be formatted?
Maybe though it's enough to specify that locations are to be represented as they are parsed, except that this doesn't hold, because the paths are being canonicalized and chained. But maybe it's ok to slightly handwave here, as I feel there are not many other interpretations

f-f · 2019-06-10T05:55:39Z

Note that there's no B side of the parser test yet as there's no implementation to produce it yet 😄

standard/imports.md

ocharles · 2019-06-10T09:55:35Z

standard/imports.md

+
+    parent </> import₀ = import₁
+    canonicalize(import₁) = child
+    ε ⊢ child : < Local : Text | Remote : Text | Environment : Text | Missing >


I'm not sure this is really what I'm after. Firstly, I want normalisation to rule out impossible paths, so Missing is no good. Next, it seems like Local doesn't produce an absolute path, which is also what I'm interested in (though maybe less so than ruling out missing files).

But can't I recover Missing myself with ?? Can't I write

let add-missing : Location -> Location-With-Missing = ... in (add-missing (./foo.dhall as Location)) ? Location-With-Missing.Missing

@ocharles would you want Dhall to check if a file exists or not? I would like to represent possibly non-existent paths (e.g. for the case in which you're configuring a tool that will create these paths)

Re making the paths absolute: I don't have a strong opinion on it as it's just about attaching the CWD to the relative paths, I just feel that it would be special casing, and I have the same feeling about failing on the missing keyword instead of including it as a constructor.
Do you have a use-case for which you cannot handle Missing and you cannot handle relative paths?

would you want Dhall to check if a file exists or not?

Yes.

I would like to represent possibly non-existent paths (e.g. for the case in which you're configuring a tool that will create these paths)

Ok, but I think that is covered by using ? missing as mentioned in my comment above.

I will have to page in exactly how I want to use this feature to see if I can handle Missing. It's probably stuff in my Dhall interpreter, so that could throw errors accordingly at runtime. I would, naturally, prefer to avoid runtime errors though.

I would like to represent possibly non-existent paths (e.g. for the case in which you're configuring a tool that will create these paths)

Ok, on further thought I think I see what you're getting at. We'd like to be able to write

{ config-dir = ./config as Location }

Under my proposal, that is an import failure if ./config doesn't already exist. Using ? we don't really have the tools to construct a Location, the best we can do is:

{ config-dir = (< Existing = ./config as Location | New : Text >) ? (< New = "./config" | Existing : Location >) }

which is a bit meh.

However, what if we had syntax for constructing Locations? Then we could

{ config-dir = Location "./config" }

The lack of an import here clarifies that this Location might not exist.

Ok, but I think that is covered by using ? missing as mentioned in my comment above

I don't see how? I want the path information, not a Missing. The Missing constructor would only be used to represent the missing keyword

Yea, I think I made a mistake in that original comment. I replied to myself with hopefully a bit more clarification.

I see. But what's wrong in them looking like imports? The semantics are very close - they are parsed like imports and get canonicalized and chained at import-resolution time - and the only thing that would change would be the semantics of ?, which will never fail on Locations

EDIT: and right, the other difference which is related to the change of the ? semantics is that the paths might not exist, which is why you want to differentiate them, I see now

One suggestion is that as Location could also return another Bool field specifying whether or not the file was present. Then, later on, once we have dependent types you could assert that the file was present using something like this:

let path = ./example.dhall as Location let _ = Assert : path.present ≡ True …

So we had a chat with @ocharles yesterday, and I think we'd like different enough features that they'd warrant different syntax (rather than trying to cram everything in the same syntax):

"Path representation":

this is just about representing locations in Dhall

the syntax could be ./some/import as Location

it would return a union like proposed by @Gabriel439 above < Local : Text | Remote : Text | Environment : Text | Missing >

it would only canonicalize and chain

it would never resolve (as it's only about representing locations), so it would never fail

this is what this PR implements

"Absolute paths resolution":

this is about having a path resolve to its absolute representation

the syntax could be ./some/path as AbsolutePath

it would return a Text with the absolute path to a file and it would do the full blown canonicalization, chaining and resolution

it would fail if the file doesn't exist, if the file is on a remote location, and in case of missing

this is what @ocharles would like to have (please correct any inaccuracies)

Co-Authored-By: Ollie Charles <ollie@ocharles.org.uk>

Gabriella439 · 2019-06-10T15:07:00Z

Another thing we could do is have the type of the result depend on the type of the import

For example:

an absolute path or home-anchored path could always return a < Local : Text > (or just Text)
a missing could always return a < Missing >
an environment variable could always return a < Environment : Text > (or just Text)
a URL could always return a < Remote : Text > (or just Text)
a relative path could return a < Local : Text | Remote : Text >

singpolyma · 2019-06-11T01:19:50Z

Remote : Text seems like a waste when the URL has already been parsed. Why not use URL : { scheme : Text, authority : Text, path: [Text], query: Text } sort of thing if we're going to expose bits of the AST this way?

philandstuff · 2019-06-11T04:58:26Z

Remote : Text seems like a waste when the URL has already been parsed. Why not use URL : { scheme : Text, authority : Text, path: [Text], query: Text } sort of thing if we're going to expose bits of the AST this way?

I can think of two reasons against this:

I’m hoping to get rid of URL parsing as part of Proposal: return to standard RFC 3986 URLs #581
if you have a { scheme : Text, authority : Text, path: [Text], query: Text }, Dhall doesn’t give you the tools to turn it back into a URL, which is probably a quite important use case. In particular, you can’t percent-encode the raw path segments.

singpolyma · 2019-06-15T22:45:57Z

It seems to me the only real difference between the two is the desire to resolve, or not. Maybe ./blah as ‎Location Raw ./blah as Location Resolved or SomeBuiltin/readlink (./blah as Location) When you don't want it to work on URLs you can achieve that with merge. I'm fairly hesitant about all versions of this feature, but especially about two totally separate ones.

ocharles · 2019-06-16T10:03:14Z

@singpolyma We did have a little chat about what is essentially a "flag" to the import type, but I'm not huge on - especially as you could just have distinctly named import types and achieve the same thing.

Gabriella439

We're at the 7 day mark for making a decision, so I'll decide to approve. I feel that if we have additional substantive changes we wish to make to improve this feature they should be made as subsequent proposals.

I think the discussion has strayed a bit from the problem that @f-f was originally trying to solve for spago, which I understood as: "provide a path that is referentially transparent". I support that goal because providing language support for referentially transparent paths is a security feature: if users try to refer to paths as Text fields within their configurations then it risks the host program accidentally reading in the wrong file if the Dhall configuration is interpreted from the wrong location.

As @singpolyma noted: there is a separate discussion about whether or not we should resolve the path to verify that it is there, but I think that should be out of scope for this proposal because:

(A) it's not addressing the original requirement
(B) it's not a feature that spago needs and I haven't seen an open source tool that does need it (yet)
(C) we can always add it later via a new keyword as noted in this thread, so we're not painting ourselves into a corner by not supporting it yet

ocharles · 2019-06-17T21:54:22Z

It's good that we've got some approval on this, but I'm still a bit unsure on this. I'll try and double check this again tomorrow, and see how it reconciles with mine and @f-f's discussion at ZuriHac.

ocharles · 2019-06-19T10:51:40Z

I'm still pretty uneasy with the semantics of missing as Location, particularly due to its interaction with ?. What is the motivation for resolving missing?

f-f · 2019-06-19T11:27:46Z

I'm still pretty uneasy with the semantics of missing as Location, particularly due to its interaction with ?. What is the motivation for resolving missing?

I don't have a strong opinion on it, but I feel it should be there for the same reason we have it in the language in the first place: completeness. More specifically:

it should be there to cover the whole range of possible import types
it should not fail, because failing on missing would imply that we'd do resolution here, while we don't

On the other hand I agree with you that it's a bit weird that missing, the import that should always fail resolution, seems to change behaviour once you add as Location (but it's not very weird once you frame as Location as a "pure operation" that doesn't do resolution)

f-f · 2019-06-25T17:24:48Z

I finally managed to put together a proof of concept of this in dhall-lang/dhall-haskell#1019

The implementation was simpler than I expected, as all the machinery is already there

joneshf · 2019-06-26T13:51:46Z

Do I understand correctly that this change means you can concatenate strings together to import expressions? Or, is this something else entirely?

f-f · 2019-06-26T14:01:15Z

@joneshf this is something entirely different: you can think of it as "reflection for imports", where at "runtime" you have an import path (or url, etc) available as a Text, properly canonicalized and chained (if you don't want that you can always just use a string).
Once you get this representation though, you cannot go back and compose another import, because the import phase happens before runtime

So this is effectively just a "smart newtype" for representing locations (paths and URLs) in Dhall

joneshf · 2019-06-26T14:25:09Z

Gotcha. Thanks for explaining!

f-f · 2019-06-26T14:32:43Z

You're welcome 🙂

A couple of fixes for tests: - rename the `asLocation` parser test I introduced in #585 to the correct path - bind the variables in the normalization tests introduced in #592 (normalization tests cannot contain unbound variables because it makes sense to normalize an expression only if it typechecks first)

f-f added 2 commits June 10, 2019 08:29

Implement importing paths as Location

a6afaac

Merge branch 'master' into f-f/implement-location

8636282

This was referenced Jun 10, 2019

Import path as absolute path to file #71

Closed

Local dependency paths are incorrect when packages.dhall is in another directory purescript/spago#244

Closed

ocharles reviewed Jun 10, 2019

View reviewed changes

Update standard/imports.md

159d880

Co-Authored-By: Ollie Charles <ollie@ocharles.org.uk>

f-f mentioned this pull request Jun 10, 2019

Proposal: return to standard RFC 3986 URLs #581

Closed

5 tasks

Gabriella439 approved these changes Jun 17, 2019

View reviewed changes

f-f added 2 commits June 19, 2019 02:13

Add Location to the grammar

d7e6d34

Specify the binary encoding too

7a76cd9

f-f added 4 commits June 19, 2019 13:28

Merge branch 'master' into f-f/implement-location

2167b20

Fix tests, add parser test

045fe42

Merge branch 'master' into f-f/implement-location

a9bec96

Merge branch 'master' into f-f/implement-location

45b7840

f-f mentioned this pull request Jun 25, 2019

Implement importing as Location dhall-lang/dhall-haskell#1019

Merged

f-f merged commit b3a374d into master Jun 25, 2019

f-f mentioned this pull request Jun 25, 2019

Fix normalization tests containing unbound variables #605

Merged

f-f mentioned this pull request Sep 13, 2019

Have a hash built-in function? #739

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement importing paths as Location #585

Implement importing paths as Location #585

f-f commented Jun 10, 2019 •

edited

Loading

f-f commented Jun 10, 2019 •

edited

Loading

ocharles Jun 10, 2019 •

edited

Loading

f-f Jun 10, 2019

ocharles Jun 10, 2019 •

edited

Loading

ocharles Jun 10, 2019

f-f Jun 10, 2019

ocharles Jun 10, 2019

f-f Jun 10, 2019 •

edited

Loading

Gabriella439 Jun 10, 2019

f-f Jun 15, 2019 •

edited

Loading

Gabriella439 commented Jun 10, 2019

singpolyma commented Jun 11, 2019

philandstuff commented Jun 11, 2019

singpolyma commented Jun 15, 2019 via email

ocharles commented Jun 16, 2019

Gabriella439 left a comment •

edited

Loading

ocharles commented Jun 17, 2019

ocharles commented Jun 19, 2019

f-f commented Jun 19, 2019

f-f commented Jun 25, 2019

joneshf commented Jun 26, 2019

f-f commented Jun 26, 2019 •

edited

Loading

joneshf commented Jun 26, 2019

f-f commented Jun 26, 2019

Implement importing paths as Location #585

Implement importing paths as Location #585

Conversation

f-f commented Jun 10, 2019 • edited Loading

f-f commented Jun 10, 2019 • edited Loading

ocharles Jun 10, 2019 • edited Loading

Choose a reason for hiding this comment

f-f Jun 10, 2019

Choose a reason for hiding this comment

ocharles Jun 10, 2019 • edited Loading

Choose a reason for hiding this comment

ocharles Jun 10, 2019

Choose a reason for hiding this comment

f-f Jun 10, 2019

Choose a reason for hiding this comment

ocharles Jun 10, 2019

Choose a reason for hiding this comment

f-f Jun 10, 2019 • edited Loading

Choose a reason for hiding this comment

Gabriella439 Jun 10, 2019

Choose a reason for hiding this comment

f-f Jun 15, 2019 • edited Loading

Choose a reason for hiding this comment

Gabriella439 commented Jun 10, 2019

singpolyma commented Jun 11, 2019

philandstuff commented Jun 11, 2019

singpolyma commented Jun 15, 2019 via email

ocharles commented Jun 16, 2019

Gabriella439 left a comment • edited Loading

Choose a reason for hiding this comment

ocharles commented Jun 17, 2019

ocharles commented Jun 19, 2019

f-f commented Jun 19, 2019

f-f commented Jun 25, 2019

joneshf commented Jun 26, 2019

f-f commented Jun 26, 2019 • edited Loading

joneshf commented Jun 26, 2019

f-f commented Jun 26, 2019

f-f commented Jun 10, 2019 •

edited

Loading

f-f commented Jun 10, 2019 •

edited

Loading

ocharles Jun 10, 2019 •

edited

Loading

ocharles Jun 10, 2019 •

edited

Loading

f-f Jun 10, 2019 •

edited

Loading

f-f Jun 15, 2019 •

edited

Loading

Gabriella439 left a comment •

edited

Loading

f-f commented Jun 26, 2019 •

edited

Loading