A type level equivalent of the `with` keyword

[Tristano8]

When interacting with a library that may not have the most ergonomic types, a useful escape hatch is to overwrite fields using with. This gets unwieldy very quickly, though, when I need to reach for a function like List/Map to apply this same transformer items in a list; you need to supply the input and output types as arguments to the function. If i'm decorating/changing an existing type, the only thing I know to do here is infer the new decorated type with the compiler, and then paste that definition as an argument to List/Map. If with had a type level equivalent, the type-level and term-level implementations would match and this would be much more ergonomic.

[JackKelly-Bellroy]

Does this also mean that we probably want a typelevel version of //?

[winitzki]

Can you give a code example that shows what the proposal would look like?

[JackKelly-Bellroy]

The primary driver of this request is that the types in https://github.com/jcouyang/dhall-aws-cloudformation/ are sometimes out of date, or AWS's own definitions are incorrect, and we need to overwrite the type of a single (possibly nested) field. This means we cannot use //\\ because Dhall will complain about a record field collision.

Given a type x = { a : A, r : { b : B, c : C }, I want to be able to construct a type { a : A, r : { b : B', c : C } without having to rewrite the entire structure by hand. One way would be to extend the with syntax, so that `x with a.b = B' works on record types.

Additionally, a type-level version of // could behave something like: { a : A, b : B } /// { b : B', c : C } = { a : A, b : B', c : C }.

[winitzki]

Makes sense to me.

[Gabriella439]

Yeah, this seems like a reasonable request

[winitzki]

The with keyword will then work in the same way for record values and for record types. This makes sense to me, but this contradicts the current design of Dhall, where record values and record types require different operations, for example /\ and //\\.

Record types are always distinct from record values, already at the level of syntax. Do we actually need separate operators like // and /// for them?

Right now Dhall has separate operators /\ and //\\ for record values and record types. Can we not collapse them into a single operator /\? What is the motivation for keeping them separate?

Should we simplify the design of Dhall and have just one set of operations that works both for record types and record values?

[JackKelly-Bellroy]

I think something with-like is useful but I don't have a strong opinion on whether it should overload the with keyword or introduce another keyword. A fresh keyword would be more in keeping with the language's current design, I agree.

[Gabriella439]

I think it would be okay to combine ∧ and ⩓, too, but still support ⩓ for backwards compatibility

[JackKelly-Bellroy]

Should the . operator then be allowed to index into record types?

Currently:

⊢ { A : Text, B : Natural }.A

Error: Not a record or a union

[Gabriella439]

I think so, and there's actually already an issue for that, too: https://github.com/dhall-lang/dhall-lang/issues/1079

[winitzki]

I'd say, we should go through the entire records / unions syntax to see if things can be simplified. I could do that given time.

[winitzki]

Right now it appears to me that the functionality of with is a superset of the functionality of //.

It seems we can always replace an expression of the form a // b by an expression of the form a with b1 with b2 with ... while getting the same result. Does that seem right?

{ x = { y = 1 }} // { x.y = True, x.z = 2 } gives { x = { y = True, z = 2 }}.

{ x = { y = 1 }} with x.y = True with x.z = 2 gives the same result, { x = { y = True, z = 2 }}.

The additional functionality of with is working with Optional values. As long as we are just working with records, with and // seem to be largely doing the same thing via different syntax.

One difference is that // accepts two records while with is a special syntax that does not accept records. So, we can write code such as a // b where a and b are variables set to some records. But we can't say a with b.

let replace
  = λ(record1 : { a : Natural, b : Bool, c : Text }) → λ(record2 : { b : Bool, c : Text }) →
      record1 // record2  -- We cannot easily rewrite this via `a with x`.