Discussion: Add language support for alternative imports

[Gabriella439]

I've gotten a couple of requests for supporting mirrors (i.e. alternative ways to retrieve an import) and I wanted to propose a more general solution for addressing this and other issues.

We could add a new ? operator to separate two arbitrary expressions (not necessarily imports) where:

e₀ ? e₁

... means try to resolve expression e₀ and if that fails then resolve expression e₁. You would also be able to chain these operators and the parentheses would be optional since this fallback behavior is associative:

(e₀ ? e₁) ? e₂ = e₀ ? (e₁ ? e₂)

There would also be a corresponding identity of the ? operator called missing that is an import that always fails to resolve:

missing ? e = e

e ? missing = e

One motivation for providing ? is to improve resilience, such as in #162 where @f-f mentioned using GitLab as a mirror for the Prelude in case GitHub goes down. Using this ? operator users wouldn't need to modify their code whenever GitHub goes down if they specify their import like this:

    let sum
          = https://raw.githubusercontent.com/dhall-lang/Prelude/e44284bc37a5808861dacd4c8bd13d18411cb961/Natural/sum
          ? https://gitlab.com/dhall-lang/Prelude/raw/e44284bc37a5808861dacd4c8bd13d18411cb961/Natural/sum

in ...

This would also solve another feature request in #70 where a person could provide an environment variable fallback if a URL was not available:

http://some.svc/ ? env:SERVICE_FALLBACK

... where SERVICE_FALLBACK might contain a Dhall expression or a new URL to import

You could also use the same operator to fall back to a pure expression. For example, if you wanted to gracefully fall back if an environment variable is missing, you could make the environment variable Optional, like this:

[ env:USER as Text ] : Optional Text ? [] : Optional Text

[f-f]

This sounds like a really good idea that would fix a bunch of problems at once, nice 👏

Some questions:

We could add a new ? operator to separate two arbitrary expressions (not necessarily imports)

As I understand it, we want <|> but at the "import resolution" stage, which is "before" compile time.
So if we chain N operations with ?, the first N - 1 should be imports, otherwise the first "pure" expression would shortcut, and this might lead to unintended bugs (OTOH messing up the order of any alternative selection leads to bugs..)

Unrelated: how about the proposal from #70 of having <|> for Bool? Would it make sense to reuse ? (from the semantics and UX points of view)?

[quasicomputational]

Unrelated: how about the proposal from #70 of having <|> for Bool? Would it make sense to reuse ? (from the semantics and UX points of view)?

I don't think reusing ? would be a good idea because ? can be lazy and avoid hitting mirrors if the primary source succeeds, but <|> would presumably not be able to do that without being a phase violation.

[Gabriella439]

@f-f: Yeah, this would be like <|> in the import resolution phase. This also implies that any expression free of imports would short-circuit the chain, but I think that is the desired behavior.

I think whether or not to add (<|>) is an orthogonal decision