Skip to content

Instantly share code, notes, and snippets.

@kenoss
Last active June 8, 2022 15:22
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save kenoss/ccc4e19e8f9054a77b2345352a19f1ab to your computer and use it in GitHub Desktop.
Save kenoss/ccc4e19e8f9054a77b2345352a19f1ab to your computer and use it in GitHub Desktop.
from typing import Protocol
class Ring(Protocol):
@staticmethod
def zero() -> "Ring":
...
@staticmethod
def identity() -> "Ring":
...
def add(self, other: "Ring") -> "Ring":
...
def mul(self, other: "Ring") -> "Ring":
...
def inverse_add(self) -> "Ring":
...
# Assume T is Ring.
class RequirementForRing(SomeUnitTestFramework):
def zero_is_additive_unit():
x = for_any_element(T)
assert x == T.zero().add(x) and x == x.add(T.zero())
...
class NonZeroIsMultipricativeGroup(Protocol):
@staticmethod
def zero() -> "Ring":
...
@staticmethod
def identity() -> "MultipricativeGroup":
...
def mul(self, other: "MultipricativeGroup") -> "MultipricativeGroup":
...
def inverse_mul(self) -> "MultipricativeGroup":
...
# Assume T is NonZeroIsMultipricativeGroup.
class RequirementForNonZeroIsMultipricativeGroup(SomeUnitTestFramework):
def any_non_zero_has_unique_multiplicative_inverse():
x = for_any_element(T)
if x == T.zero():
should_raise(x.inverse_mul())
else:
assert T.identity() == x.inverse_mul().mul(x) and T.identity() == x.mul(x.inverse_mul())
...
class Field(Protocol, Ring, NonZeroIsMultipricativeGroup):
pass
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment