with expressions regressed

[maxime-didier]

With dhall 1.41.2, it used to be possible to do the following:

(Some { x = 1 }) with ?.x = 2
=> Some { x = 2 }

(Some { x = 1 }) with ?.x = "hello"
=> Some { x = "hello" }

With dhall 1.42.1, a restriction was added forbidding a with expression from changing the type of an optional (it is a breaking change that was not announced in the changelog). This restriction is buggy and both the above expressions fail to evaluate with:

Error: ❰with❱ cannot change the type of an ❰Optional❱ value

[winitzki]

Interesting. Let me check my Scala implementation, as it passes all standard tests and implements the latest Dhall standard fully as documented.

[winitzki]

Yes, my Scala implementation fails both expressions. The error appears to be already in the Dhall standard in the typing judgments for this expression. Let me get the details.
https://github.com/dhall-lang/dhall-lang/blob/master/standard/type-inference.md#with-expressions

An `Optional` update using the `with` keyword must preserve the type of the "inner" value.


    Γ ⊢ e : Optional T
    Γ ⊢ v : T
    ──────────────────────────────────
    Γ ⊢ e with ?.ks… = v : Optional T

This means: (Some x) with ?.a = b is well-typed only if b has the same type as x (that is, the type T).

This appears to be wrong. At least, this does not in any way take into account the record access ?.a.

If this typechecking rule is implemented exactly as written in the standard, both of the examples will be not well-typed:

(Some { x = 1 }) with ?.x = 2  -- Typechecking will set `T = { x : Natural}` and `v = 2`, but `2` is not of type `T`.
(Some { x = 1 }) with ?.x = "hello" -- Typechecking will set `T = { x : Natural}` and `v = "hello"`, but `"hello"` is not of type `T`.

My Scala implementation reports these errors directly as:

Inferred type Natural differs from the expected type { x : Natural }, expression under type inference: 2

The error is that ?.x = 2 should have been interpreted as replacing Some { x = 1 } by Some { x = 2 }. Instead, it is being interpreted as replacing Some { x = 1 } by Some 2.

[maxime-didier]

Interesting. Why the restriction ? Why wasn't a rule like the following adopted ?

Γ ⊢ e : Optional T₀
Γ, x : T₀ ⊢ x with ks… = v : T₁
────────────────────────────────── x ∉ FV(v)
Γ ⊢ e with ?.ks… = v : Optional T₁

Edit: x should not appear in v, not e.

[winitzki]

The intent was to prevent changing the types of values inside Optional.

I don't really know the motivation; why is it allowed to do { x = { y = 1 } } with x.y = "abc" but not allowed to do a similar replacement under Optional.

But that was the change. A with expression should not change the type, it may only change a value.

Some { x = { y = 1 }} with ?.x.y = 2   -- Evaluates to Some { x = { y = 2 } }
Some { x = { y = 1 }} with ?.x = 0   -- Type error, it is not allowed to replace { y : Natural} with another type

That's how I understand the intent behind this change.

If this understanding is correct, then the current rule is wrong. It should have been something like this:

Γ ⊢ e : Optional T₀
Γ, x : T₀ ⊢ x with ks… = v : T₁
T₀ ≡ T₁
────────────────────────────────── x ∉ FV(e)
Γ ⊢ e with ?.ks… = v : Optional T₀

[kukimik]

I'm just linking the PR that introduced this for reference: dhall-lang/dhall-lang#1254.

[winitzki]

I have looked through the discussions in there, and I don't see any real motivation for prohibiting the type change. The use case was that you need access to record fields under Some. So, it seems to me that we should allow (Some { x = 1 }) with ?.x = "hello", that will change the type from Optional { x : Natural } to Optional { x : Text }.

The usual with operation with records already can change the type.

Is there a reason to allow (Some { x = 1 }) with ?.x = 2 (evaluating to Some { x = 2 }) but not allowing (Some { x = 1 }) with ?.x = "hello" (evaluating to Some { x = "hello" }?

I would suggest that we revise the standard and fix the implementations so that users are allowed to change the type of values under Some via with ?.x.y.z expressions. This would make the with feature consistent across record types and optional types, especially considering that they can be freely mixed as ?.x.?.y.z and so on.

[MonoidMusician]

what type T would you pass to None T during evaluation when it is not Some v? figuring out the right type would require typechecking during evaluation.

[winitzki]

what type T would you pass to None T during evaluation when it is not Some v? figuring out the right type would require typechecking during evaluation.

Good point. Maybe that was the motivation for prohibiting the type change that would be happening for (None Natural) with ? = "abc" . To evaluate that, we would need to know at evaluation time that "abc" has type Text. Only then we will be able to produce the result None Text.

There are quite a few restrictions that come from the assumption that evaluation may not use any type information. This restriction is an example.

Another example is that we cannot simplify { x = r.x, y = r.y } to just r when r is a record with just two fields x and y because we do not know, at evaluation time, the type of r. We also cannot simplify r with x = r.x to just r.

[Gabriella439]

Yeah, the reason the type is not supposed to change is so that evaluation doesn't need to infer the type. However, it is still weird that (Some { x = 1 }) with ?.x = 2 doesn't work. That seems like a specification bug, probably. In fact, the original PR that added support for this specifically cited that as one of the examples they were trying to support as valid Dhall code:

⊢ (Some { x = 1 }) with ?.x = 2

Some { x = 2 }

[winitzki]

@Gabriella439 Yes, I believe it is a specification bug that will produce the wrong behavior if implemented literally according to specification. I described that in a previous comment in this PR. I already fixed this in my Scala implementation. I can try to fix it when I have time (but this won't be soon, I am moving to a new apartment).