chessai/semirings

Instance for []

Closed this issue · 5 comments

I tried to use semirings in one of my projects, but stumbled over Semiring instance for []. My initial expectation was that plus = (++), but then I realised that such definition would violate the commutativity law. Nevertheless, the existing instance looks quite artificial to me. Does it have any nice applications?

The thing is that AFAIU there are many possible definitions of Semiring over []. Basically, we can apply any fixed permutation to both input lists, pass results through existing plus or times and apply an inversed permutation. E. g.,

instance Semiring a => Semiring [a] where
  zero = []
  one  = [one]
  plus xs ys = reverse (listAdd (reverse xs) (reverse ys))
  times xs ys = reverse (listTimes (reverse xs) (reverse ys))

Is any of these instances more canonical (or more useful) than another?

I wonder whether it is reasonable to sacrifice an additive commutativity for lists and vectors for the sake of practical applications.

listTimes was implemented incorrectly, for some reason it was using point-wise multiplication, which is actually unlawful. I made a typo in the test suite, so i didn't catch this. It has been fixed in dc069b7. Here on out, when I say 'current implementation', I am referring to this fixed implementation.

The current implementation of plus and times for [] and Vector can be interpreted as polynomials in one variable - this is why the laws are still followed under arbitrary permutations of the arguments to plus and times. The goal would be to have these implemented as newtypes (and additional newtypes constrained to Ring coefficients, which support a more efficient polynomial multiplication).

As for providing something that allowed for an unlawful listAdd, specifically (++), it breaks more laws than just additive commutativity. it also prevents multiplication from distributing over addition. What follows is a datatype with semiring instance, and some examples illustrating this.

newtype Unlawful a = Unlawful [a]
instance Semiring a => Semiring (Unlawful a) where
  zero = Unlawful zero
  one = Unlawful one
  plus (Unlawful x) (Unlawful y) = Unlawful (x ++ y)
  times (Unlawful x) (Unlawful y) = Unlawful (x `times` y)

examples, as per QuickCheck:

-----------------
-- Unlawful [] --
-----------------
Semiring: Additive Commutativity *** Failed! Falsifiable (after 2 tests and 1 shrink):
  Description: a + b = b + a
  a = Unlawful [1]
  b = Unlawful [0]
  a + b = Unlawful [1,0]
  b + a = Unlawful [0,1]
Semiring: Additive Left Identity +++ OK, passed 100 tests.
Semiring: Additive Right Identity +++ OK, passed 100 tests.
Semiring: Multiplicative Associativity +++ OK, passed 100 tests.
Semiring: Multiplicative Left Identity +++ OK, passed 100 tests.
Semiring: Multiplicative Right Identity +++ OK, passed 100 tests.
Semiring: Multiplication Left Distributes Over Addition *** Failed! Falsifiable (after 6 tests and 11 shrinks):
  Description: a * (b + c) = (a * b) + (a * c)
  a = Unlawful [0,0]
  b = Unlawful [0]
  c = Unlawful [0]
  a * (b + c) = Unlawful [0,0,0]
  (a * b) + (a * c) = Unlawful [0,0,0,0]
Semiring: Multiplication Right Distributes Over Addition *** Failed! Falsifiable (after 3 tests and 7 shrinks):
  Description: (a + b) * c = (a * c) + (b * c)
  a = Unlawful [0]
  b = Unlawful [0]
  c = Unlawful [0,0]
  (a + b) * c = Unlawful [0,0,0]
  (a * c) + (b * c) = Unlawful [0,0,0,0]
Semiring: Multiplicative Left Annihilation +++ OK, passed 100 tests.
Semiring: Multiplicative Right Annihilation +++ OK, passed 100 tests.

Cool, after dc069b7 it started to make more sense for me. Thanks for explanations. Is it now semantically equivalent to the following definition?

toMap :: [a] -> Map (Sum Int) a
toMap = Map.fromList . zip (map Sum [0..])

instance Semiring a => Semiring [a] where
  zero      = Map.elems (zero :: Map (Sum Int) a)
  one       = Map.elems (one  :: Map (Sum Int) a)
  plus  x y = Map.elems (toMap x `plus`  toMap y)
  times x y = Map.elems (toMap x `times` toMap y)

it breaks more laws than just additive commutativity. it also prevents multiplication from distributing over addition.

Sure, because additive commutativity follows from left and right distributive laws. On one side we have (a + b)(c + d) = (a + b)c + (a + b)d = ac + bc + ad + bd, but on the other
(a + b)(c + d) = a(c + d) + b (c + d) = ac + ad + bc + bd, which means that bc + ad = ad + bc. However, it is possible to have only left or only right distributivity, when addition is non-commutative.

The unlawful instance I had in mind was plus = (++) and times = liftA2 times. If we ignore ordering, it is similar to the Semiring instance for Set. AFAIU it satisfies all laws except additive commutativity and one of distributivity laws.

Is it now semantically equivalent to the following definition?

Yes.

Sure, because additive commutativity follows from left and right distributive laws. On one side we have (a + b)(c + d) = (a + b)c + (a + b)d = ac + bc + ad + bd, but on the other
(a + b)(c + d) = a(c + d) + b (c + d) = ac + ad + bc + bd, which means that bc + ad = ad + bc. However, it is possible to have only left or only right distributivity, when addition is non-commutative.

I knew this, but was only trying to be explicit in what laws it broke.

The unlawful instance I had in mind was plus = (++) and times = liftA2 times. If we ignore ordering, it is similar to the Semiring instance for Set. AFAIU it satisfies all laws except additive commutativity and one of distributivity laws.

That's funny; I meant to ask which instance you were thinking of, this was the one I thought you might go for. But, this instance actually fails both distributivity laws.

Left Distribute Law:

a = [0,1]
b = [1]
c = [0]

-- a * (b + c) = [0,0,1,0]
-- (a * b) + (a * c) = [0,1,0,0]

Right Distribute Law:

a = [1]
b = [0]
c = [0,1]

-- (a + b) * c = [0, 0, 1, 0]
-- (a * c) + (b * c) = [0, 1, 0, 0]

I see. You convinced me, thanks for details. It may make sense to reflect the choice of instance in haddocks, just to prevent possible user's confusion.