> So in your hypothetical language with union types `X | Null -> Y` is a function that can actually return `Y | Null`?

No, but a function which returns Y | Null can be replaced with a function which returns Y without changing code on the call site.

Imagine I always used to give you a nail (Y) or nothing (Null), and you can handle both receiving a nail and receiving nothing. Then I can, at any time, change my behavior to giving you nails only. Because you can already handle nails, and the fact that I now never give you nothing doesn't bother you. You just perform a (now useless) check of whether you have received a nail or nothing.

> a function which returns Y | Null can be replaced with a function which returns Y without changing code on the call site.

Yes this falls out of injectivity.

> the function type (X -> Y|Null) can be improved by rewriting the function to (X|Null -> Y)

I agree that any value received by the former function (`X`) can be received by the latter function (`X|Null`). However you cannot rewrite the former to have the signature of the latter.

You would need to write:

prf : (X -> Y|Null) -> X|Null -> Y

You would have to be able to convert a `Null` value into a `Y`.

You could definitely use `X|Null -> Y` to implement `X -> Y|Null` but that is not what you are claiming.

> However you cannot rewrite the former to have the signature of the latter.

Of course I can. I can always change the code to anything I like. That's what "rewriting" is. The question is only whether the business logic still makes sense, and whether the old call site code still works. Just look at the example I gave above.

> You could definitely use `X|Null -> Y` to implement `X -> Y|Null` but that is not what you are claiming.

"Implementing" is a special case of rewriting, so how can you say you can implement something but not rewrite it?

> Of course I can. I can always change the code to anything I like. That's what "rewriting" is. The question is only whether the business logic still makes sense, and whether the old call site code still works. Just look at the example I gave above.

You have a function that can return a Null response and you are claiming you can rewrite it to be one that does not return a Null.

This means that in the cases where your function previously produced a `Null`, you have to produce a `Y`. You claimed you can do this if you write the function to receive `X|Null`. In other words you are claiming you can write `(X -> Y|Null) -> X|Null -> Y`. I challenge you to write this function.

> "Implementing" is a special case of rewriting, so how can you say you can implement something but not rewrite it?

I didn't say that. You claimed you can write `(X -> Y|Null) -> X|Null -> Y`. I am saying that is impossible but you could write `(X|Null -> Y) -> X -> Y|Null`. Do you see the difference?

You seem to have a strangely specific understanding of the term "rewrite". "Rewriting" here just means replacing one function with another one. If it is possible to write a function f, then any(!) function g can replaced with f simply by renaming it. That's the same as "rewriting". It's just writing a different function and giving it the same name. The question is only if your call site code will still work (from the compiler perspective, we ignore the business logic here). It generally will still work if the name of the new/rewritten function stays the same. But it also will still work if the input type is more general or the return type is more specific, or both. That is, if your language supports union types of this sort (like e.g. Typescript).