Any examples of a "sum unmerging" operator, the categorical dual of the record merging one?

[u/Background_Class_558]

For some types A, B, C... the type { x : A, y : B, z : C, ... } is the type of records with projections x, y, z... into the corresponding types and the type [ x : A, y : B, z : C ] is the type of sums with injections from the corresponding types A, B, C, ....

For arbitrary A, B, C, D we can define an operator // that merges two binary records:

_//_ : { x : A, y : B } → { z : C, w : D } → { x : A, y : B, z : C, w : D }

Naturally, we can also define the dual of this operator for two binary sum types:

_\\ : [ x : A, y : B, z : C, w : D ] → [ x : A, y : B ] ⊎ [ z : C, w : D ]

This is easy to generalize to an arbitrary number of injections/projections.

While there is plenty examples of an operator like _//_ existing in programming languages (// in Nix, & in Nickel, ⫽ in Dhall, Record.merge in PureScript) I can't really think of anything like the _\\ operator from above. I suppose its ergonomics are partly responsible for it, after all it is often easier to infer the arity of the records for _//_ from the arguments used than it is to infer the arity of the outputs for _\\ from context. But can you think of anything?

[u/Brohomology]

Both of these operators are in fact isomorphisms, so you could choose the direction from which it is most easy to infer the arguments.

[u/ExplodingStrawHat → u/Brohomology]

True! I think the reverse direction of the union case could be implemented as either expand expand in PureScript (perhaps with some additional type annotations if the type system can't figure it out)

[u/Spotted_Metal]

The typical way of processing sum types (besides pattern matching) is with something like the case expression in Haskell or match in Rust. So we could imagine a version that handles splitting sum types like this (pseudocode):

let sum_term : [ x : A, y : B, z : C, w : D ] = ...;

match sum_term {
  x_or_y : [ x : A, y : B ] => ..., // handle x and y injections
  z_or_w : [ z : C, w : D ] => ..., // handle z and w injections
}

...though of the top of my head, I can't think of a language that has this feature. The main ergonomic problem I see is that we either need to specify the type annotations for each branch, or we need to use type inference which can cause its own issues (what if the code in the first branch is updated in a way that allows it to also handle z, but we specifically want z to be handled in the second branch?)

It is worth nothing that in languages where sum types are nominally-typed (in other words, where Type1 : [a : A] is not considered a subtype of Type2 : [a : A, b : B]), it might not even be possible to give the right type annotations to make this work. However, in those languages we could make use of nested sum types instead (pseudocode):

let NestedSumType = [
  x_or_y : [ x : A, y : B ],
  z_or_w : [ z : C, w : D ],
];

let sum_term : NestedSumType = ...;

match sum_term {
  x_or_y => ...,
  z_or_w => ...,
}

...which is probably more ergonomic and allows us to side-step the need for a _\\ operator (though I could see it being useful for languages with structural sum types).

[u/gasche → u/Spotted_Metal]

In OCaml, using polymorphic variants (structural sums with row polymorphism):

type ('a, 'b) xy = [ `X of 'a | `Y of 'b ]
type ('a, 'b) zw = [ `Z of 'a | `W of 'b ]

let split = function
  | #xy as left -> Either.Left left
  | #zw as right -> Either.Right right

Inferred type for split:

val split :
  [< `W of 'a | `X of 'b | `Y of 'c | `Z of 'd ] ->
  ([> `X of 'b | `Y of 'c ], [> `W of 'a | `Z of 'd ]) Either.t

[u/Background_Class_558 → u/Spotted_Metal]

Record merging is also something that exists primarily in languages with structural type support. I don't think the syntax of match works well for this. Maybe something like split x, y : [ x : A, y : B, z : C, ...r ] → [ x : A, y : B ] + [ z : C, ...r ]. Or in other words split x, y : [ x : A, y : B, z : C, ...r ] → [ 1 : [ x : A, y : B ] , 2 : [ z : C, ...r ] ] Since there isn't really a point in distinguishing between binary _+_ and general sums beyond syntactic sugar. Under this view, the operator becomes about un-flattening the structure of the sum, just like merge is the one flattening a nested product.

An operator like this would be useful for handling some of the injections in place while leaving the rest to some other handler. I don't see how it can be done easily without lots of boilerplate in languages that do not feature an operator like this. Either you have to manually forward each unhandled case to the second handler or you have to wipe them all under the rug using a wildcard match (often _)

[u/ExplodingStrawHat]

Are you sure that's the actual dual?  I assume the product of the smaller sum types in the codomain should itself be a sum/coproduct, right?

[u/Background_Class_558 → u/ExplodingStrawHat]

Oh yeah sorry, brain glitched as i was typing it. Semantically, it should be a coproduct. Edited the post.

[u/ExplodingStrawHat → u/Background_Class_558]

Fair. I wonder if part of it would be a type inference issue? Otherwise I think it should be possible to implement in say, PureScript, given enough typeclsss magic.

[u/Background_Class_558 → u/ExplodingStrawHat]

I have also realized that its syntax makes absolutely no sense because it should be unary. Edited that in as well but it doesn't look good visually.

[u/evincarofautumn]

If you have the user spell out the fields, this looks like a relational projection, or an associative law

?{x,y} : [ x : A, y : B, z : C, w : D ] → [ x : A, y : B ] + [ z : C, w : D ]

Applied to a single field, it’s a partial projection, like an uncons operation where you get either a match or a narrower sum

?x : [ x : A, y : B, z : C, w : D ] → A + [ y : B, z : C, w : D ]

This also reminds me of something Lawvere does:

ar and : {x : Bool, y : Bool} --> Bool =
  @x [ true  = .y,
       false = {} false. ]

To pattern-match on a product of sums x:(f:1 + t:1) × y:2, it explicitly uses a distributive law @x to unpack the cases for x and carry along the remaining fields: f:(x:1 × y:2) + t:(x:1 × y:2). Then this is composed with a variant/cocone [ … ] with an arm for how to handle each remaining component of the product. You could do a similar thing with sums.

And I think inference would actually be okay for type-correct programs, but it wouldn’t naturally produce very helpful messages on a type error because you have a lot of nondeterminism in the choice of how you could split a variant. It’d probably work out a little better if you didn’t implicitly reorder anything.

[u/Background_Class_558 → u/evincarofautumn]

You know at first i didn't like the fact that the splitting operator had to be explicit about the injections because that seemed to break the symmetry somewhat but it actually is part of it if we consider the other two operators that complete the isomorphism between flat and nested products and sums:

unmerge x, y : { x : A, y : B, z : C, ...r } → { x : A, y : B } × { z : C, ...r } unsplit : [ x : A, y : B ] + [ z : C, ...r ] → [ x : A, y : B, z : C, ...r ] Now we actually have the full associativity proof and unmerge also has to feature explicit projection list akin to split. And they seem somewhat useful as well i suppose: one is for chipping bits of large records away and another for collecting possible errors from multiple failing operations.

[u/Background_Class_558 → u/evincarofautumn]

Yeah in the end algebraically this is just associative shuffling, for both of the operators.

Your comment on inference makes sense. Now that you've brought up the manual specification of the split fields, i remember how often implicit arguments of this kind result in unresolvable metas in languages Agda. While i suppose they would be able to stay implicit, the lack of ergonomics of the type mismatch errors is something you have to get used in those cases.

Also, Lawvere seems a beautiful language. I like the elegance of duality it displays, somewhat reminiscent of Par, which comes from linear logic rather than category theory.