I think we're discussing slightly different things. I'd like to eventually get this line of reasoning closer to where you are, but right now my interest in desc

I think we're discussing slightly different things. I'd like to eventually get this line of reasoning closer to where you are, but right now my interest in describing ADTs has less to do with representation of useful things and more to do with "these types form a basis for thinking about computation". Effectively, products are the quintessential "grouping" notion, sums the quintessential "choice" notion, and implications the quintessential "hypothetical" notion. So those are pretty important for describing any computation. All that said, I really like relational types and wish they were more commonly used. I do think it takes some effort to model them in ADTs and that a system which provided them more directly would be fun.