Skip to content

Incorrect blanket trait implementations for commutative rings #17

@grover-lc

Description

@grover-lc

Consider the following program:

use derive_more::{Add, AddAssign, Mul, MulAssign, Sub, SubAssign};
use noether::{
    AssociativeAddition, AssociativeMultiplication, CommutativeAddition, CommutativeMultiplication,
    Distributive, PrincipalIdealDomain,
};
use num_traits::{One, Zero};
use std::ops::Neg;

// create and implement the ring ZZ x ZZ

#[derive(Debug, PartialEq, Add, AddAssign, Sub, SubAssign, Mul, MulAssign)]
#[mul(forward)]
#[mul_assign(forward)]
struct ZxZ(isize, isize);

impl AssociativeAddition for ZxZ {}
impl CommutativeAddition for ZxZ {}
impl AssociativeMultiplication for ZxZ {}
impl CommutativeMultiplication for ZxZ {}
impl Distributive for ZxZ {}
impl One for ZxZ {
    fn one() -> Self {
        ZxZ(1, 1)
    }
}
impl Zero for ZxZ {
    fn zero() -> Self {
        ZxZ(0, 0)
    }
    fn is_zero(&self) -> bool {
        self == &Self::zero()
    }
}
impl Neg for ZxZ {
    type Output = Self;
    fn neg(self) -> Self::Output {
        ZxZ(-self.0, -self.1)
    }
}

// a function which only accepts an input of a type implementing PrincipalIdealDomain
fn is_pid<T: PrincipalIdealDomain>(_: T) {
    println!("My type implements PrincipalIdealDomain.")
}

// mainline shows that ZZ x ZZ implements PrincipalIdealDomain
fn main() {
    let pair = ZxZ(5, -3);
    is_pid(pair);
}

Behaviour

This program compiles and runs without error, printing My type implements PrincipalIdealDomain..

Expected behaviour

I think the code should fail to compile because the explicitly implemented traits should not cause PrincipalIdealDomain to be implemented for ZxZ.

Note

The struct ZxZ represents the commutative ring $\mathbb{Z}\times\mathbb{Z}$. Only appropriate traits for this ring were explicitly implemented in this program, but $\mathbb{Z}\times\mathbb{Z}$ is not a principal ideal domain. It is not even an integral domain.

Proposal

Remove the following blanket implementations of IntegralDomain, UniqueFactorizationDomain and PrincipalIdealDomain for all types implementing CommutativeRing:

noether/src/rings.rs

Lines 107 to 109 in 677edcb

impl<T: CommutativeRing> IntegralDomain for T {}
impl<T: IntegralDomain> UniqueFactorizationDomain for T {}
impl<T: UniqueFactorizationDomain> PrincipalIdealDomain for T {}

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions