Proposal: Allow combining union types

[aleator]

Would it be possible to have an analogue of // for union types? As in, <a:T1 | b:T2 | c:T3> \/ <a:T2 | d:T4 | e:T5> = <a:T2 | b:T2 | c:T3 | d:T4 | e:T5>

The use case I have is something like this

let myLayouts = ... union ...
in let myHandlers = ... handlers for the above ...
in let layouts = constructors (./basicLayouts \/ myLayouts)
in let handlers = ./basicHandlers // myHandlers
in (render handlers) [layouts.foo 1 "x",layouts.bar "x" "x"] 

[Gabriella439]

@aleator: Yeah, this seems reasonable to me. My only suggestion is to use \\// / ⩔ for the symbol for duality with ⩓

[brendanzab]

What happens on a conflict between two variants with differing types?

EDIT: oh, I see - the second on is chosen - it's shown in the initial example as a:T1->a:T2.

[aleator]

One thing that bothers me about using ⩔ is that it wouldn't behave exactly like ⩓, and more like //. I don't see how recursively updating unions would make sense. I might be wrong at this though.

Regarding the name, there isn't a type level // yet, is there? Should there be? If yes, perhaps there is some symmetry of names that could be considered here. For example /// for records and \\\ for unions.

If you'd like, I could take a stab at implementing this.

[aleator]

Just for sake of procrastination, here is a stab at getting the semantics done (confessing that I actually haven't read the dhall semantics before doing this). Since naming is hard, I used the 'plus-in-a-circle' as a stand in.

l ⇥ e
───────────
l ⊕ <> ⇥ e


r ⇥ e
────────────
<> ⊕ r ⇥ e


ls₀ ⇥ < x : l₁ | ls₁… >
rs₀ ⇥ < x : r₁ | rs₁… >
< ls₁… > ⊕ < rs₁… > ⇥ < ts… >
───────────────────────────────
ls₀ ⊕ rs₀ ⇥ < x : r₁ | ts… >


ls₀ ⇥ < x : l₁ | ls₁… >   < ls₁… > ⊕ rs ⇥ < ls₂… >
────────────────────────────────────────────────────  ; x ∉ rs
ls₀ ⊕ rs ⇥ < x : l₁ | ls₂… >


l₀ ⇥ l₁   r₀ ⇥ r₁
─────────────────────   ; If no other rule matches
l₀ ⊕ r₀ ⇥ l₁ ⊕ r₁


and typing

Γ ⊢ l :⇥ Type
l ⇥ < ls… >
Γ ⊢ r :⇥ Type
r ⇥ <>
────────────────
Γ ⊢ l ⊕ r : Type

Γ ⊢ l :⇥ Type
l ⇥ < ls… >
Γ ⊢ r :⇥ Type
r ⇥ < a : A | rs… >
Γ ⊢ { ls… } ⊕ { rs… } : T₁
─────────────────────────────
Γ ⊢ l ⊕ r : Type

Γ ⊢ l :⇥ Kind
l ⇥ < ls… >
Γ ⊢ r :⇥ Kind
r ⇥ < a : A >
────────────────
Γ ⊢ l ⊕ r : Kind

Γ ⊢ l :⇥ Kind
l ⇥ < ls… >
Γ ⊢ r :⇥ Kind
r ⇥ < a : A | rs… >
Γ ⊢ < ls… > ⊕ { rs… } : T
───────────────────────────── 
Γ ⊢ l ⊕ r : Kind

[Gabriella439]

@aleator: Yeah, I like the idea of a type-level analog for // named /// and a dual \\\ for union types

[haitlahcen]

Would definitely be cool to have this feature available !

[jvanbruegge]

Just hit this limitation again with dhall-kubernetes. I want to use cert-manager which defines custom resources. I can normally define dhall types for them and use them, but in order to tie everything together I have one file per service that is a list of the big kubernetes union. The problem: I can't add the cert-manager types to that union without copy+pasting the file from dhall-kubernetes to my own repository. With a union operator, I could simply change my top level union import file from:

let union =
      https://raw.githubusercontent.com/dhall-lang/dhall-kubernetes/master/typesUnion.dhall sha256:8e8db456b218b93f8241d497e54d07214b132523fe84263e6c03496c141a8b18

in  union

to

let union =
      https://raw.githubusercontent.com/dhall-lang/dhall-kubernetes/master/typesUnion.dhall sha256:8e8db456b218b93f8241d497e54d07214b132523fe84263e6c03496c141a8b18

let cert-union = ./cert-manager/union.dhall

in  union \\// cert-union

[sjakobi]

@jvanbruegge I think this proposal mostly needs a volunteer to standardize it.

Would you be interested in being that volunteer?

[jvanbruegge]

Sadly not at the moment, as my spare time is quite limited right now. Most likely not before April

[Gabriella439]

I think we should narrow down this proposal to just standardizing support for \\// / ⩔ for now since I think that will satisfy most use cases.

This came up recently again in: https://discourse.dhall-lang.org/t/sum-type-subsets/219

[Nadrieril]

Didn't we say \\\ ? I would expect \\// to be recursive so we'd want to start with the simpler non-recursive one

[Gabriella439]

@Nadrieril: There are two reasons I think it would be simpler to standardize \\// first:

• We've gotten away without /// for a while, so I suspect we can do without \\\ for a while, too, so standardizing one operator instead of two is less work
• If we standardize \\\, we'd also need to standardize /// for symmetry (and still need to standardize \\// for symmetry, too). Standardizing only \\// leaves fewer symmetric gaps

[Nadrieril]

@Gabriel439 So we'd standardize only \\//, which recursively merges union types, is that right ?
Is there any sensible \/ that would go with it ? Maybe it would take a union literal and a union type and cast that literal to the merged type ? Pretty sure we can omit that for now.

[Gabriella439]

@Nadrieril: I think the natural "dual" behavior for \/ would be to merge two functions that consume unions. In other words, something like this pseudo-type:

(\/) : (a → r) → (b → r) → (a \\// b → r)

[Nadrieril]

Ah right, what I mentioned looks more like a dual to record projection I guess.
I feel like your operator can almost always be replaced by a merge and // in practise. To really make the operator redundant we'd need an inverse to merge, that converts a <...> -> r to a record rec such that merge rec is the original function.

[Gabriella439]

@Nadrieril: Yes, any operator for unions can be implemented in terms of its dual operation on records. Also, to be pedantic, you would implement \/ in terms of /\, not //.

In fact, the converse is also true: you can implement any operator on records in terms of its dual operation on unions. This means that you could implement the behavior of /\ in terms of \/.

This redundancy is a natural consequence of the fact that unions can be encoded in terms of functions on records:

-- Edit: Fixed the type as @Nadrieril noted
< A₀ : T₀ | A₁ : T₁ | … > ≅ forall (r : Type) → { A₀ : T₀ → r, A₁ : T₁ → r, … } → r

... and, dually, you can implement records in terms of functions on unions:

-- Edit: Fixed the type
{ A₀ : T₀, A₁ : T₁, … } ≅ forall (r : Type) → < A₀ : T₀ → r, A₁ : T₁ → r, … } → r

... so any time you add keyword or operator on unions or records you make its dual keyword or operator redundant.

In fact, this duality implies that there is a missing keyword that is the dual of merge which would apply a "union of handlers" to a record to project out a single field. Back when I was prototyping Dhall I considered adding this dual keyword for symmetry, but chose not to at the time because it didn't add a fundamentally new capability to the language and I couldn't figure out a compelling use case for it and it was less ergonomic than using ordinary record field access.

[Nadrieril]

@Gabriel439 Oh neat, I never realized you could go both ways between records and unions. That makes (\/) : (a → r) → (b → r) → (a \\// b → r) feel more justified to me now. I even feel like that interacts well with recursive merging.

Note: you have an extra -> r in your isomorphisms; they should be

< A₀ : T₀ | A₁ : T₁ | … > ≅ forall (r : Type) → { A₀ : T₀ → r, A₁ : T₁ → r, … } → r

and

{ A₀ : T₀, A₁ : T₁, … } ≅ forall (r : Type) → < A₀ : T₀ → r, A₁ : T₁ → r, … > → r

Also, to be pedantic, you would implement / in terms of /, not //.

I thought about it, but then since the records being merged are records of functions, /\ wouldn't work for merging conflicting fields

[damdo]

I think this could be really really useful.

A potential usecase for this, that I'm currently facing, is related to dhall-kubernetes.

I'm tying to output custom resource types (defined for example by CRDs) into Kubernetes Lists, together with standard Kubernetes Types and to do that I need to have all of them into a single Union.

The only way I can think of for achieving it, is to create a superset of the Kubernetes TypesUnion that extends it with the desired custom types, by copy/pasting the two Types groups into a new Union or to use a modified version of @TristanCacqueray's mini-generate to achieve the same in a more automated way (if you have better ideas here, suggestions are more than welcome).

I think having \\// / ⩔ could vastly improve the ergonomics of dhall-kubernetes in primis but would also be very valuable for many similar usecases.
Any chance this will be taken in consideration in the next priorities of the language? :) Thanks.

[samuela]

@jvanbruegge and @damdo I just created dhall-lang/dhall-kubernetes#187 for exactly this issue (before seeing your comment here)

Did either of you come up with a solution for this when using dhall-kubernetes?