Oh, and this probably also needs a test exercising the new with feature

I added a section for with expressions in both the normalization and type checking docs. I can add a couple tests soon.

Before that, I did notice a big flaw with the current changes: the type checking judgements don't enforce that the ? path component is applied to an Optional, so { x = 0 } with ? = 1 is legal and results in { x = 0, `?` = 1 }, for example. Would it be reasonable to add k ≠ ? to the existing record-related with judgements? I'm not sure if there's precedent for something like that elsewhere in the standard.

Edit: Actually, I think that would break the quoted label `?`, so I'm not sure what to do instead.

I think the correct way to fix this is to distinguish at the AST level the reserved ? component and an escaped field named ?

In other words, currently the With constructor is defined as:

    | With Expression (NonEmpty Text) Expression

… and you would need to define a new WithComponent type like this:

data WithComponent = Label Text | Optional

… so that the With constructor could use it like this:

    | With Expression (NonEmpty WithComponent) Expression

Once you resolve that ambiguity at the level of the syntax tree then it's easier to fix the other ambiguities. For example, this expression:

{ x = 0 } with { ? = 1 }

… would correspond to this Haskell syntax tree:

With (RecordLiteral [("x", NaturalLiteral 0)]) (Optional :| []) (NaturalLiteral 1)

… which would be a type error. Also, it would be distinct from this expression:

{ x = 0 } with { `?` = 1 }

… which would correspond to this Haskell syntax tree:

With (RecordLiteral [("x", NaturalLiteral 0)]) (Label "?" :| []) (NaturalLiteral 1)

… which would evaluate to:

{ x = 0, `?` = 1 }

Makes sense! I chose PathComponent with the idea that this will be reused for Field in the future. The Optional constructor name overlapped with the one for Builtin, so I had to pick a different one. I went with DescendOptional (maybe that would be better if we actually used the "descend" terminology in the spec somewhere). Let me know if you have different preferred names.

This approach also revealed a similar oversight in binary encoding/decoding. Currently,

{ x = 0 } with ? = 1

and

{ x = 0 } with `?` = 1

have the same binary representation. I'm thinking maybe there could be a tag like 0 for Label and 1 for DescendOptional? What do you think?

I think it should be possible to extend the encoding for path components to include the reserved ? component without breaking backwards compatibility. CBOR is weakly typed, so you can encode an int for reserved path components instead of a string and it wouldn't require introducing an extra tag.

Got it! I'm having some trouble working inductively on the path. I initially wanted to write something like

encode(ks₀…) = [ ks₁… ]
─────────────────────────────
encode(?.ks₀…) = [ 0, ks₁… ]


encode(ks₀…) = [ ks₁… ]
───────────────────────────── ; k ≠ ?
encode(k.ks₀…) = [ k, ks₁… ]


encode(e₀) = e₁   encode(k₀.ks₀…) = [ k₁, ks₁… ]   encode(v₀) = v₁
──────────────────────────────────────────────────────────────────
encode(e₀ with k₀.ks₀… = v₀) = [ 29, e₁, [ k₁, ks₁… ], v₁ ]

but encode is defined on Expressions which NonEmpty PathComponent is not. Would it be reasonable to add a separate rule just for encoding the path?

Yeah, introducing a new judgment is one way to do it, but you can also do something like this:

encode(e₀ with k₀.ks₀… = v₀) = [ 29, e₁, [ k₁, ks₁… ], v₁ ]
───────────────────────────────────────────────────────
encode(e₀ with ?.k₀.ks… = v₀) = [ 29, e₁, [ 0, k₁, ks₁… ], v₁ ]

encode(e₀) = e₁   encode(v₀) = v₁
───────────────────────────────────────────────────────
encode(e₀ with ? = v₀) = [ 29, e₁, [ 0 ], v₁ ]

… and change the existing encoding judgment for with to:

encode(e₀ with k₀.ks₀… = v₀) = [ 29, e₁, [ k₁, ks₁… ], v₁ ]
───────────────────────────────────────────────────────  ; k ≠ ?
encode(e₀ with k.k₀.ks₀… = v₀) = [ 29, e₁, [ k, k₁, ks₁… ], v₁ ]

encode(e₀) = e₁   encode(v₀) = v₁
───────────────────────────────────────────────────────  ; k ≠ ?
encode(e₀ with k = v₀) = [ 29, e₁, [ k ], v₁ ]

That might not be obvious, but then the corresponding Haskell code will clarify what that means

Ah, that makes perfect sense.

encode (With e₀ (DescendOptional :| k₀ : ks₀) v₀)
    | TList [ TInt 29, e₁, TList (k₁ : ks₁), v₁ ] <- encode (With e₀ (k₀ :| ks₀) v₀)
    , let b = TList [ TInt 29, e₁, TList (TInt 0 : k₁ : ks₁), v₁ ] =
        b

encode (With e₀ (DescendOptional :| []) v₀) = TList [ TInt 29, e₁, TList [ TInt 0 ], v₁ ]
  where
    e₁ = encode e₀
    v₁ = encode v₀

encode (With e₀ ((Label k) :| k₀ : ks₀) v₀)
    | TList [ TInt 29, e₁, TList (k₁ : ks₁), v₁ ] <- encode (With e₀ (k₀ :| ks₀) v₀)
    , let b = TList [ TInt 29, e₁, TList (TString k : k₁ : ks₁), v₁ ] =
        b

encode (With e₀ ((Label k) :| []) v₀) = TList [ TInt 29, e₁, TList [ TString k ], v₁ ]
  where
    e₁ = encode e₀
    v₁ = encode v₀

Binary.lhs:201:1: error: [-Wincomplete-patterns, -Werror=incomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘encode’:
        Patterns not matched:
            With (Variable _ _) (DescendOptional :| [(Label _)]) (Variable _ _)
            With (Variable _ _) (DescendOptional :| [(Label _)]) (Lambda _ _ _)
            With (Variable _ _) (DescendOptional :| [(Label _)]) (Forall _ _ _)
            With (Variable _ _) (DescendOptional :| [(Label _)]) (Let _ _ _ _)
            ...

That said, as you pointed out, it might be better to deviate from a direct translation to make the actual behavior more obvious.

I've also added some tests!

There's just one test failure to fix and then this is ready to merge:

https://hydra.dhall-lang.org/log/c7fiq7f20h8cah9x0p7qdswal54ady50-test-files-lint.drv

Fixed!

🎉 @Gabriel439 thank you very much for all your help with this!

With this done, I'm wondering if other language features could be extended to use the ? path component. I think the most obvious one would be field selection (e.g., (Some { x = 0 }).?.x). What do you think? I'd be happy to try to standardize this as well.

Are you expecting (Some { x = 0 }).?.x to evaluate to Some 0? It looks nice, but it isn’t compositional: there’s no meaning you can give to ? such that ((Some { x = 0 }).?).x has that behavior. (Also you might run into issues with type changing None again.) You could try parsing paths as their own thing, but then you’re basically headed down the road to optics and I’m not sure those are a good fit for language primitives.

there’s no meaning you can give to ? such that ((Some { x = 0 }).?).x has that behavior

Ah, that's true! We diverged from the original idea of something like x?.y to make ? its own path component so it could work more nicely with with, but I didn't realize how it was limited in this other way. Probably others have thought about it already haha

The main issue is that there's not a good way to type-check using ? as a field accessor since you don't necessarily know at type-checking time if the value is a Some or not unless you normalize the argument.

It would work better if Dhall had something like polymorphic variant such as in Grace, because then the type of \x -> x.? could be something like:

forall (a : Type) . < Some : a > -> a

… and the type of the Some constructor would be something like:

Some : forall (a : Type) (b : Alternatives) . a -> < Some : a | b >

… so it would only work if the compiler could infer that only the Some alternative was present and the None alternative was not possible.

I see. With all that said, what do you see for the future of #1141 (perhaps the discussion can continue there)?

Oh, I misunderstood what you were asking! That would work if the result type were Optional

So in other words, you could standardize something that says that (Some { x = 0 }).?.x evaluates to Some 0

@darichey: Now that this is completed you can collect the $300 reward. If you submit an expense here then I'll approve it: https://opencollective.com/dhall/expenses/new