Sorry Stephen, I feel like I've fallen down the rabbit hole here... your posts are usually a paragon of clarity but this one is just beyond me :(
On Sat, May 14, 2016 at 02:28:51PM +0900, Stephen J. Turnbull wrote:
Inference of str vs bytes (in particular, which component of a "sum" type in general) is not always possible, and it's not obvious how beneficial it is. Proposal: have typecheckers recognize "suspicious" unions, and complain if they are not "converted" to a component type before passing to a polymorphic function.
So what you really want is a Sum type constructor, where Sum is in the sense of category theory's sum functor. That is, not only is the result Type a (disjoint) union, but you're also guaranteed that each operation respects the component type.
Are we supposed to know what category theory's sum functor is? I'm warning you, if you start talking about Monads I'm just going hit delete on your post :-)
I'm afraid I don't understand what you mean by a Sum type constructor. Can you explain in more detail?
I also don't understand what you mean by '"suspicious" unions' (quotes in original) or what makes them suspicious, or "suspicious" as the case may be. What's suspicious about Union[bytes, str]?
Are you proposing a Sum contructor for the typing module, as an alternative to Union? What will it do?
If not, why are you talking about Sum[bytes, str]?