Occasionally situations arise where a type of unordered pairs would be very handy.
Perhaps the most important example is for representing edges in undirected graphs.
I came across another example that is instructional in a paper by C.J. Date entitled "The Primacy of Primary Keys: An Investigation". He wonders how to define a relation to store information about marriages, under the definition that a marriage is between two people. He gives a definition like:
MARRIAGE ( HUSBAND, WIFE, DATE_OF_MARRIAGE ) CANDIDATE KEY ( HUSBAND, DATE_OF_MARRIAGE ) CANDIDATE KEY ( WIFE, DATE_OF_MARRIAGE )
and raises the issue that there is no reason to prefer designating one key or the other as primary. If you amend the example so that there are not distinguished roles like "husband" or "wife" that could provide sensible labels for two separate attributes each storing a single person identifier, then this seems to be a natural spot for an unordered pair type. (Please refrain from discussing the politics of this definition, there are plenty of places on the internet for that.)
I set about thinking of how to make such a type and what its interface could be. I ended up with nearly the exact same interface I had for general sets. I am working on a language for expressing database queries, so I want to strictly control non-determinacy. (Adopting Haskell concrete syntax for purposes of communication...) I have a
Overall I'm reasonably happy with this. But I got to wondering whether it would be better to have a more general facility and view unordered pairs as a special case of it. You can look at them as the quotient of pairs with respect to an equivalence relation that permutes the ordering, and then you get unordered triples and ... too, if you can think of anything to use them for. Or you can look at them as a refinement type of sets with cardinality 2.
Those definitions of course differ on whether
The quotient type approach struggles with one of my goals, because presumably the pattern matching function that applies on ordered pairs would still apply to the quotient unordered pairs without flagging the result as non-deterministic.
If you take the ad hoc approach (neither quotients nor refinement types) it is difficult to think of names for the unordered pairs with and without allowing the degenerate pairs relating a value to itself, so that is another challenge.
I wasn't able to dig up too many examples through search engines, does anyone have thoughts on the best approach to modeling these?
A very interesting project developed by Zachary DeVito et al at Stanford University:
Seems as if the target use case is high-performance computing. The team has also released a related paper, titled Terra: A Multi-Stage Language for High-Performance Computing:
Active forum topics
New forum topics