Sets, types and type checking

Just to point that this part is very literally true. They compose perfectly well, but they don't compose on the same way that tagged unions do. Tagged unions compose by function abstraction, untagged ones compose by function dispatching.

Maybe one can argue that untagged unions compose in less useful ways. But I've never seen this argument made.

Your last sentence put the whole argument even better in place in my head, it depending on the runtime is both a blessing and a curse and is what let's us change function signatures in a backwards compatible way, while also what hinders our ability to reason/encode stuff in it statically.

[1] I think part of the misunderstanding here between the "two camps" is that some people work on systems that are a closed world. You know and control everything, so an all-encompassing type system that can evolve with the universe itself makes the most sense. Hickey on the other hand worked/works mostly in an area where big systems developed by completely different entities have to communicate with each other with little to no coordination. You can't willy nilly refactor your code and just trust the compiler to do its job, this is the open sea. Also, I think this area is a bit neglected by more modern/hyped languages, e.g. the dynamicism that the JVM has is not really reproduced anywhere anymore?

You can do this:

    const user = await fetchUserDTO(123);
    // user is Result<UserDTO, Error>
    if(!isOk(user)) { something(user.err); return; }
    user.name; // user is narrowed to UserDTO

    export const FailSym: unique symbol = (globalThis as any).____FailSym ?? Symbol('FailSym');
    (globalThis as any).____FailSym = FailSym;
    export type Result<T, E> = T | {
        [FailSym]: true,
        err: E
    }
    
    export function Ok<T>(val: T): Result<T, never> { return val; }
    export function Fail<E>(err: E): Result<never, E> { return {[FailSym]: true, err}; }
    
    export function isOk<T, E>(val: Result<T, E>): val is T { return !(typeof val == 'object' && val != null && FailSym in val); }
    export function isFail<T, E>(val: Result<T, E>): val is Result<never, E> { return typeof val == 'object' && val != null && FailSym in val; }
    
    export function resultify<T, E>(promise: Promise<T>): Promise<Result<T, E>> {
        return promise.then(Ok, err => Fail(err as any));
    }

Could you give an example of this? The only case I can imagine is a union null <=: T, T | null. This would cause unexpected behaviour, i.e. a if T = (U | null), the function orElse : T | null → T → T would always return the second argument if the first is null, but this is perfectly consistent with the fact that T itself is a union type. The idea that it should do anything different is presuming that the null assigned to T is different from the null assigned to T | null (that union types are disjoint). But this is an invalid assumption. It's still a validly typed program that obeys a consistent set of rules. It's just that there is no tagging in the union type (you don't know if a member comes from the left or right side). This is only an issue if you write code expecting the union to work like a tagged union.

You don’t even know how to query it to find anything out about it.

But you could pass it to someone else.

When someone asks you for a completely unconstrained object, the type is “any”.

It’s technically the same type from two perspectives.

(Not saying this extreme version of the concepts are how they are implemented. Never had a chance to use such types before.)

Scala3 is the only programming language to implement both AFAIK.

C# has a proposal to add both unions and disjoint unions: https://github.com/dotnet/csharplang/blob/main/proposals/Typ...

OCaml has polymorphic variants which are open disjoint unions.

Kotlin is looking to add union types for errors: https://youtrack.jetbrains.com/issue/KT-68296/Union-Types-fo...

I believe Java's checked exceptions behave somewhat like union types.

Do you mean implemented with enums? Enums themselves are not a type. They are a mechanism for value generation, providing automatic numbering (hence enumeration) for constants. Indeed, they, like all values, are ultimately represented by a type, but that type can range from something like a simple integer or something more complex like a tagged union (typically with the generated value being the tag) with different ecosystems favouring different type approaches.