This is fix correct, but to more closely match the judgment I'd suggest putting the betaNormalize in the definition of t₁. i.e. let t₁ = betaNormalize (Operator …)

This seems like an idiosyncracy of the Haskell implementation. I'd like to require that unlimited precision is supported even if the Haskell implementation needs to be fixed

One standard test failed until I implemented the logic that 00:00:00.000 is kept like this with 3 digits of precision even though it's the same as 00:00:00. Then I tried more digits and discovered this unexpected 12-digit cutoff.

I agree that it is more in the spirit of Dhall to support unlimited precision here. But it's out of scope for this PR and also beyond my capacity to fix the Haskell implementation (and presumably other implementations need to be fixed).

Would you like me to change the standard to specify unlimited precision? Something like this:

⊢ let t = 09:00:00.0987654321098765432109876543210000000000 in " let t = " ++ Time/show t

" let t = 09:00:00.0987654321098765432109876543210000000000"

@Gabriella439 I have updated this PR, removing changes in imports.md and making the change you indicated, specifying arbitrary precision for fractional seconds in time literals.

Note that there is no import keyword in Dhall like there is in Nix. Maybe use https://example.com here as a sample import

One thing I just realized is that if x is not in the free variables of T₀ then ↑(-1, x, 0, T₀) is a no-op (i.e. it evaluates to T₀) since the shift operator only shifts free variables.

It's a bit confusing to me. Can T₀ contain x@1 as a free variable? In that case, ↑(-1, x, 0, T₀) is not a no-op. But my understanding of free variables is that they must have a zero de Bruijn index. Is that correct? In the requirement x ∉ freeVars(T₀), is it implied that T₀ also may not contain x@1 as a free variable?

@Gabriella439 Do you agree with these changes? I'm not sure what's the best way to make this clear. The original text doesn't say what userHeadersExpr means. And I couldn't figure out what it means to have Γ(headersPath) = userHeadersExpr and then twice using Γ₀ and Γ₁. It's not clear how you can have a judgment with premises that reuse the same Γ₀ and Γ₁. So, I replaced the final context with Γ₂.

To me, it seems that imports.md needs more work. I'll finish implementing imports and then maybe I will have more material for another PR with corrections.

For now, I'm still trying to understand the standard where it says "Γ₀(import) means to retrieve the expression located at import". It is not clear what "retrieve" means. If it means just to download the contents of the URL, to read the file, etc., then we don't need any Γ₀ while doing that. If it means to fetch the expression from the context Γ₀ then it's not clear from the text of imports.md how that expression got there.

I believe it is necessary to introduce a new symbol, such as READ(import_path) = expr, to denote reading a given external resource that exists at import_path and converting it into a Dhall expression expr.

I will move the imports.md changes to another PR. I will have several more corrections for imports.md that will need to be taken care of separately.

I have retained only a couple of minor changes in imports.md that I think should be clearly an improvement. The entire imports.md could benefit from a rewrite, it's too complicated and has a different style from other specifications in the standard.

After implementing the import system, I have some understanding of how it works but I'm not sure I understand why imports.md is the way it is. Maybe I will just add "implementation notes" to imports.md in another PR, showing a step-by-step pseudocode of how the import judgment could be implemented.