imports: allow local imports for DHALL_HEADERS expression

[timbertson]

As discussed in dhall-lang/dhall-haskell#2236, many authentication-related use cases of DHALL_HEADERS will rely on importing environment variables (e.g. GITHUB_TOKEN). So we want to allow local imports, but we don't want to allow remote imports (since that could get stuck in a loop).

@Gabriel439 I've added prose and tests, but I might need your help to understand what pseudocode to update and how 🙏

[Gabriella439]

The first step to standardizing this formally is to add a new boolean flag to the import resolution function that controls whether or not remote imports are enabled.

Right now, the "type" of the import resolution function is:

Import resolution is a function of the following form:

(Δ, here) × Γ₀ ⊢ e₀ ⇒ e₁ ⊢ Γ₁

... where

• (Δ, here) (an input) is an ordered non-empty list of visited imports used to
  detect import cycles
  • here is the current import
  • Δ is the ordered history of 0 or more imports in the visited set that
    the interpreter visited along the way to here
• Γ₀ (an input) is an unordered map from imports to expressions representing
  the state of the filesystem/environment/web before the import
  • Γ₀(import) means to retrieve the expression located at import
• e₀ (an input) is the expression to resolve
• e₁ (an output) is the import-free resolved expression
• Γ₁ (an output) is an unordered map from imports to expressions representing
  the state of the filesystem/environment/web after the import
  • Γ₁, import = x means to save x to the resource identified by import

… and you'd be changing it to add a boolean flag like this:

Import resolution is a function of the following form:

(Δ, here) × r × Γ₀ ⊢ e₀ ⇒ e₁ ⊢ Γ₁

... where

• (Δ, here) (an input) is an ordered non-empty list of visited imports used to
  detect import cycles
  • here is the current import
  • Δ is the ordered history of 0 or more imports in the visited set that
    the interpreter visited along the way to here
• r (an input) is a boolean that is true if remote imports are enabled and false if they are disabled
• Γ₀ (an input) is an unordered map from imports to expressions representing
  the state of the filesystem/environment/web before the import
  • Γ₀(import) means to retrieve the expression located at import
• e₀ (an input) is the expression to resolve
• e₁ (an output) is the import-free resolved expression
• Γ₁ (an output) is an unordered map from imports to expressions representing
  the state of the filesystem/environment/web after the import
  • Γ₁, import = x means to save x to the resource identified by import

Then you will need to add and thread that flag through all of the import-resolution-related code

Once you've done that then I'll show you how to update the headers.dhall logic to use that flag

[timbertson]

OK, I think I've done the above. There were some cases I wasn't sure whether I should write true or an unbound variable because it's not necessarily relevant, or I couldn't tell if the code was specific to remote imports. For the unbound variable I used allowImports but I get the feeling I should be using.. something greek? It may not surprise you to hear I really don't understand what I'm doing in the judgement sections, so if you want to take over I'd be very happy about that 😉

Threading this flag through everything that touches imports seems kind of arduous, and I'm scared it might also cause us to fork the code (e.g. do we need to make as Location work differently based on this new flag?)

Is there a way to restrict the additional logic to the headers resolution code? i.e. what if we always allow remote imports, but if you're silly enough to have a remote import in the headers expression itself then that import would be loaded with an empty "userheaders" context.

I don't how how to put that in pseudocode, and I get the feeling you might be less comfortable with that because it's slightly closer to allowing infinite recursion, even though it still prevents it.

[timbertson]

Actually, I just had a thought. The import judgement already forbids cycles, doesn't it? What if we just lean on that? If we don't special-case the header resolution at all, wouldn't the existing rules cause it to fail on cyclic imports? As long as we include the relevant location (env:DHALL_HEADERS / ~/.config/dhall/headers.dhall) as a first class part of the import chain, any attempt to do a remote import from the headers expression would fail due to cyclic imports.

Implementations would be free to provide a more useful error message in this specific case, but it wouldn't need to be standardised.

[Gabriella439]

@timbertson: Yeah, I like that idea even better. Just to make sure I understand: you're proposing that headers.dhall would be added to the import chain when transitively resolving its own imports?

[timbertson]

Yep, exactly. I'll update the PR later today

[Gabriella439]

This might help clarify what here is supposed to refer to

Suggested change

	Γ(env:DHALL_HEADERS ? "${XDG_CONFIG_HOME}/dhall/headers.dhall" ? ~/.config/dhall/headers.dhall ? []) = userHeadersExpr
	(ε, here) × Γ₀ ⊢ userHeadersExpr ⇒ userHeaders ⊢ Γ₁ ; Resolve userHeadersExpr with an empty import context,
	headersPath = env:DHALL_HEADERS ? "${XDG_CONFIG_HOME}/dhall/headers.dhall" ? ~/.config/dhall/headers.dhall ? []
	Γ(headersPath) = userHeadersExpr
	(ε, headersPath) × Γ₀ ⊢ userHeadersExpr ⇒ userHeaders ⊢ Γ₁

[timbertson]

I've updated the pseudocode to resolve the expression, although I am discarding Γ₁. It doesn't seem necessary to thread it through to the remaining imports, but maybe I should for cleanliness?

[timbertson]

👋 any more feedback on this? Does it look reasonable to you @Gabriel439

[Gabriella439]

Sorry for the delay. This looks great! 🙂