Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Int64 EuclideanRing #8

Open
jamesdbrock opened this issue Dec 15, 2022 · 1 comment
Open

Int64 EuclideanRing #8

jamesdbrock opened this issue Dec 15, 2022 · 1 comment

Comments

@jamesdbrock
Copy link
Member

Int64 is not a EuclideanRing. It can’t pass the checkEuclideanRingGen test because mod is only lawful if the divisor is in the 32-bit Int range.

Maybe we should remove the EuclideanRing instance, since it’s a lie? Then Int64 would not have the div and mod EuclideanRing methods, and instead would have only the truncating division functions quot and rem.

https://pursuit.purescript.org/packages/purescript-prelude/6.0.1/docs/Data.EuclideanRing

https://pursuit.purescript.org/packages/purescript-integers/6.0.0/docs/Data.Int#v:quot

https://en.m.wikipedia.org/wiki/Modulo_operation

@jamesdbrock
Copy link
Member Author

-- `mod` is only lawful if the divisor is in 32-bit Int range.
checkEuclideanRingGen $ chooseInt64 (Int64.fromInt bottom) (Int64.fromInt top)

-- `mod` is only lawful if the divisor is in 32-bit Int range.
checkEuclideanRingGen $ chooseUInt64 zero (UInt64.unsafeFromInt top)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

No branches or pull requests

1 participant