Ring laws are too weak

Main.purs

module Main where

import Prelude

import Control.Monad.Eff (Eff)
import Data.Foldable (fold)
import TryPureScript (DOM, h1, p, text, render)

main :: Eff (dom :: DOM) Unit
main =
    render $ fold
      [ h1 (text "Ring law example")
      , p (text ("Inverses 1: a - a = zero: " <> show (map law1 enumerateZ3)))
      , p (text ("Inverses 2: (zero - a) + a = zero: " <> show (map law2 enumerateZ3)))
      , p (text ("Compatibility: a - b == a + (zero - b): " <> show (compatLaw <$> enumerateZ3 <*> enumerateZ3)))
      ]
      
-- Integers modulo 3
data Z3 = Zero | One | Two

derive instance eqZ3 :: Eq Z3

-- The Semiring instance is all above board
instance semiringZ3 :: Semiring Z3 where
  zero = Zero

  add Zero x = x
  add x Zero = x
  add One One = Two
  add One Two = Zero
  add Two One = Zero
  add Two Two = One

  one = One

  mul Zero _ = Zero
  mul _ Zero = Zero
  mul One x = x
  mul x One = x
  mul Two Two = One

instance ringZ3 :: Ring Z3 where
  -- zero minus anything gives you the additive inverse
  sub Zero Zero = Zero
  sub Zero One = Two
  sub Zero Two = One

  -- anything minus itself is zero
  sub One One = Zero
  sub Two Two = Zero

  -- now, the laws do not constrain the remaining 4 cases at all!
  -- we are free to define any nonsense operation here
  sub _ _ = Zero

enumerateZ3 :: Array Z3
enumerateZ3 = [Zero, One, Two]
  
law1 :: Z3 -> Boolean
law1 a = a - a == zero

law2 :: Z3 -> Boolean
law2 a = (zero - a) + a == zero

compatLaw :: Z3 -> Z3 -> Boolean
compatLaw a b = a - b == a + (zero - b)