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?
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?
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.