Unordered Homogeneous N-tuples for Guaranteed Commutativity

Links
#1
5 Likes
#2

But if f returns the same value for both elements of the pair, then we have not successfully differentiated between them,

Our pair (using Haskell tuple notation) might be (5, 5), in which the elements are not differentiable by any f, but the pair is differentiable from (3, 5) or (5, 3). So your N-tuples’ values must be a set, not a multiset(?)

A function application whose arguments just happen to be equal is perfectly cromulent. I’m pretty sure I can guarantee commutativity of operations on a pair where the elements are equal (or an N-tuple where all the elements are equal), but that seems beyond this trick(?)

So I think diffBy needs to be able to report 5 possible results:

  • Both Booleans are True, but the values are different;
  • Both Booleans are True, and/because the values are the same;
  • Right (b1, b2): the Boolean is True of b1, False of b2;
  • Both Booleans are False, but the values are different;
  • Both Booleans are False, and/because the values are the same.

To extend this to N-tuples then gives us binomial explosion. (As in: the second and fourth are equal, but different to the third and fifth which are equal, none equal to the first.)

Contrast the blog post you link to which starts from Commutative functions:

prf : ∀ x y → f x y ≡ f y x

This’ll come out True if x == y.

#3

But it is a multiset! (5, 5) Is differentiable from (5, 3) by the function (== 5). For the first pair diffBy (== 5) produces Left True. For the second pair, Right (5, 3).
Also, the functions I wrote at the end of the blogpost, do work with multiples of the same value. So there’s no need to extend the possible results of diffBy.