Skip to content

Instantly share code, notes, and snippets.

@hdgarrood

hdgarrood/Main.purs

Last active Apr 4, 2020
Embed
What would you like to do?
Ring laws are too weak
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment