Could Unison support untagged unions?

[pchiusano]

@alvaroc1 posted this in the Slack:

Here is a use case where i REALLY could use untagged unions: when working with actors, often i want to send a reference to an actor, but the reference should only accept a subset of the messages that the actor is capable of receiving (encapsulation, easier reasoning, etc):

unique type Message = Start | Stop | Flush | Flip

actor : ActorRef Message
actor = self

-- limit this actor reference to only receiving Start and Stop messages
limitedActor : ActorRef (Start | Stop) -- untagged union
limitedActor = actor

starterActor |> Actor.send limitedActor

Without untagged unions, if i want to remain type-safe i have to create a new type for every subset of the messages that i want to expose, along with mappings, which gets very boilerplatey fast (even more so if i want to present expose several subsets):

unique type Message = Start | Stop | Flush | Flip
unique type Message.StartOrStop = Start | Stop

Message.StartOrStop.toMessage = cases
  StartOrStop.Start -> Message.Start
  StartOrStop.Stop -> Message.Stop

actor : ActorRef Message
actor = self

-- limit this actor reference to only receiving Start and Stop messages
limitedActor : ActorRef Message.Start
limitedActor = actor |> ActorRef.contramap Message.StartOrStop.toMessage

starterActor |> Actor.send limitedActor

[pchiusano]

Here's some concerns I have about this sort of thing in Unison:

• Right now, pattern matching is compiled to multi-level switch statements that just inspect the constructor tags. This is the most efficient thing to do.
• Once you start adding untagged unions, pattern matching must instead inspect the type id as well as the constructor tag. I don't want all pattern matching to take a performance hit for this one niche use case. There's perhaps a way to compile pattern matching with untagged unions differently. But even if possible, it adds complexity.
• I'm not clear on what this even means for like Int | Nat. Those two types will have the same runtime representation (and there may be many other cases where we use the same runtime representation for types that are considered different by the type system).
• I also have some questions about types like (Text -> Int) | (Text -> List Text). There's no way to distinguish which of the two cases it is without calling the function, same goes for any generic type which is contravariant in some type parameter. This feels kind of can of worms-y.

In general, untagged unions seem like a feature that makes more sense in dynamically typed languages. I'm happy to be proven wrong though. :)

I wonder if we could do some extensible sum types implementation, similar to the extensible records proposal but for sums / unions. These would be tagged unions, but I wonder if the syntax could be made just as ergonomic.

Here's the extensible records proposal #3845

cc @dolio who might have more thoughts on this.

[alvaroc1]

In general, untagged unions seem like a feature that makes more sense in dynamically typed languages. I'm happy to be proven wrong though. :)

my only experience with untagged unions comes from typescript and scala 3 🤷🏼

I wonder if we could do some extensible sum types implementation, similar to the extensible records proposal but for sums / unions. These would be tagged unions, but I wonder if the syntax could be made just as ergonomic.

Yes! this definitely sounds to me like it could work for my use cases, without the runtime issues of untagged unions

[alvaroc1]

the original example is assuming that each constructor automatically gets its own type (which is what happens with typescript)

this is what it would look like without that assumption:

unique type Start = Start
unique type Stop = Stop
unique type Flush = Flush
unique type Flip = Flip

-- unioning the types here, not the constructors
untagged type Message = Start | Stop | Flush | Flip
...

[alvaroc1]

pattern matching must instead inspect the type id

don't change pattern matching, it should continue to just use the constructors

unions that can't be distinguished at runtime can't be distinguished by pattern-match... and that's ok

(Text -> Int) | (Text -> List Text)

unbaked thought: you can define this type, but you can't do anything with it (maybe trace it?) because you can't distinguish between them at runtime... that's ok, and i think it's sound, you would just not use that type in practice

maybe in theory calling that returns Int | List Text 🤔 ... probably too much work and not worth it

Int | Nat

trickier...

fn : (Int | Nat) -> ()
fn = cases
  0 -> printLine "got zero"
  -1 -> printLine "got negative one"
  n -> trace "can't print, since i don't know what type it is" n

a literal will match if its runtime representation matches... a bit of a stretch, but maybe this is ok?

it kinda fits in that pattern matching remains a runtime thing

given this, Nat | Int is not a very useful type in practice, but it's not necessarily disallowed

[pchiusano]

my only experience with untagged unions comes from typescript and scala 3 🤷🏼

Haha, true.

Some questions I have on tagged unnamed unions cc @dolio

1. Is A ⊕ B a subtype of B ⊕ A?
2. Is A ⊕ B a subtype of A ⊕ B ⊕ C?
3. Is List Nat ⊕ List Text allowed?

If answer to 1 is yes, then this implies we need to somehow canonicalize the order of the union, right? Though how would we do that in a polymorphic context where A and B are type variables? Maybe if 3 is disallowed somehow then the "type head" could be used as the tag, similar to Typescript.

It certainly seems simpler / more tractable to just have A ⊕ B be order dependent. A ⊕ B can still be a subtype of A ⊕ B ⊕ C. This could literally be done with a bit of syntax sugar, where ⊕ is just a right nested Either, similar to what we do for Tuple.

Alternately you could have named unions, similar to extensible records. So choice { a : Nat, b : Text, c : Blah } and then you use choice a 42 or choice b "hi" to construct or pattern match. You could compile it by literally including the field name in the runtime representation and pattern matching on that, or perhaps you could assign globally unique sequential ids to each field and then use that for pattern matching - though you'd still need the bytecode format to contain the fields, presumably.

[alvaroc1]

pattern matching must instead inspect the type id as well as the constructor tag

not convinced that this is the case

typescript doesn't support matching on type, since they are all erased... but it does support matching on "runtime" type (for those values that have a way to distinguish)

i would actually prefer it if scala didn't support matching on type either since it's flaky

[alvaroc1]

this one niche use case

The particular example is niche, but I run into this all the time in different contexts:

• A big part of this hierarchy is types carrying different subsets of the top-level messages: https://share.unison-lang.org/@alvaroc1/midi/code/main/latest/types/Message
• Only some subsets of ImageSize are supported on some methods, but I can't currently type that without another type: https://share.unison-lang.org/@alvaroc1/p/code/latest/types/public/openai/main/api/request/ImageSize
• Only some channel masks are supported depending on implementation: https://share.unison-lang.org/@alvaroc1/p/code/latest/types/@5gs3tpsfennqt8d3ipmdfpu4ir0663gim60m1t1k0cej1bv5enc50segpmn5m6aqnp0ugj6htc3shuerrrk6dln8re0jq15a3ib469g

That's just in unison... in most of my typescript projects you'll see it untagged unions used in almost every file.