Allow combining record types

[dhall-lang]

Allow combining record types

[Gabriella439]

Yeah, I think it's probably fine to generalize // and /\ to work on types. I'd have to implement it to say for sure but if it works then I will put up a proposed change to the semantics

[Gabriella439]

Okay, so looking into this more closely I think this would work better if there were a new operator for this purpose. The reason why you don't want to overload the operator is that it complicates the semantics. For example, naively overloading the operator to work on both record values and record types behaves weirdly if you have a record value whose field is a record type, such as:

{ foo = { bar : Bool } } ∧ { foo = { baz : Text } }

If you define the semantics of ∧ to trivially recurse over the fields you run the risk of accidentally merging the wrong kind of values:

{ foo = { bar : Bool } } ∧ { foo = { baz : Text } }

-- Oops!  It started by combining record values and not it's combinine record fields
= { foo = { bar : Bool } ∧ { baz : Text } }

= { foo = { bar : Bool, baz : Text } }

It's less confusing if it's a new operator name. The only non-trivial part is deciding what it should be named.

My suggestion is to name it //\\ (ASCII) / ⩓ (UTF8 U+2A53) and have it behave like the type-level analog of ∧. I don't think we need a type-level analog of //

[Gabriella439]

Alright, I have a prototype of this in a branch here:

https://github.com/dhall-lang/dhall-haskell/compare/gabriel/combine_types

I will open up a proposal to update the standard soon to match that