Skip to content
{{ message }}

Instantly share code, notes, and snippets.

# hdgarrood/Main.purs

Last active Apr 4, 2020
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)
to join this conversation on GitHub. Already have an account? Sign in to comment