@since WIP

@since WIP

The addition operation.

Laws

1. x #+ y = y #+ x (commutativity of #+)
2. x #+ (y #+ z) = (x #+ y) #+ z (associativity of #+)

If you define a custom pscalePositive, ensure the following also hold:

3. pscalePositive # x # pone = x
4. (pscalePositive # x # n) #+ (pscalePositive # x # m) = pscalePositive # x # (n #+ m)
5. pscalePositive # (pscalePositive # x # n) # m = pscalePositive # x # (n #* m)

The default implementation ensures these laws are satisfied.

@since WIP

The notion of zero, as well as a (kind of) reversal of pscalePositive, similar to floor division by positive integers.

Laws

1. pzero #+ x = x (pzero is the identity of #+)
2. pscalePositive # pzero # n = pzero (pzero does not scale up)

@since WIP

The notion of additive inverses, and the subtraction operation.

Laws

If you define pnegate, the following laws must hold:

1. (pnegate # x) #+ x = pzero (pnegate is an additive inverse)
2. pnegate #$ pnegate # x = x (pnegate is self-inverting)

If you define #-, the following law must hold:

3. x #- x = pzero

Additionally, the following 'consistency laws' must hold. Default implementations of both pnegate and #- uphold these.

4. pnegate # x = pzero #- x
5. x #- y = x #+ (pnegate # y)

Lastly, if you define a custom pscaleInteger, the following laws must hold:

6. pscaleInteger # x # pzero = pzero
7. pscaleInteger # x #$ pnegate y = pnegate #$ pscaleInteger # x # y

@since WIP

The multiplication operation.

Laws

1. x #* (y #* z) = (x #* y) #* z (associativity of #*)

If you define a custom ppowPositive, ensure the following also hold:

3. ppowPositive # x # pone = x
4. (ppowPositive # x # n) #* (ppowPositive # x # m) = pscalePositive # x # (n #+ m)
5. ppowPositive # (ppowPositive # x # n) # m = pscalePositive # x # (n #* m)

The default implementation ensures these laws are satisfied.

Note

Unlike PAdditiveSemigroup, the multiplication operation doesn't need to be commutative. Currently, all Plutarch-provided instances are, but this need not be true for other instances.

@since WIP

The notion of one (multiplicative identity).

Laws

1. pone #* x = x (pone is the left identity of #*)
2. x #* pone = x (pone is the right identity of #*)

@since WIP

Laws

1. pfromInteger 0 = pzero
2. pfromInteger 1 = pone
3. pfromInteger (x + y) = pfromInteger x #+ pfromInteger y
4. pfromInteger (x * y) = pfromInteger x #* pfromInteger y

Additionally, the following 'interaction laws' must hold between the instances of PAdditiveGroup and PMultiplicativeMonoid for a:

5. x #* (y #+ z) = (x #* y) #+ (x #* z) (#* left-distributes over #+)
6. (y #+ z) #* x = (y #* x) #+ (z #* x) (#* right-distributes over #+)

@since WIP

Laws

Pedantry note

Technically, the requirements here are too strong: we demand an ordered ring, which integral domains don't necessarily have to be. However, in our case, our hand is forced by expected semantics: in abstract algebra, both the absolute value and the signum are real numbers (which are always totally ordered) but in our case, both must be elements of the integral domain itself. Thus, in order for the laws to make any sense, we have to ensure a total order on the integral domain. Since all of our integral domains are 'at least as big' as the integers, this doesn't pose a huge problem.

@since WIP

Partial version of PPositive. Errors if argument is zero.

@since WIP

Build a PPositive from a PInteger. Yields PNothing if argument is zero.

A default implementation of exponentiation-by-squaring with a strictly-positive exponent.

Important note

This implementation assumes that the operation argument is associative.

@since WIP

@since WIP

@since WIP

@since WIP

@since WIP