`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: https://github.com/dhall-lang/dhall-lang/pull/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.