Export functions on Natural in Numeric.Natural

Zemyla

22 Mar 2020 22 Mar '20

6:40 p.m.

Functions in GHC.Natural like naturalToWordMaybe and minusNaturalMaybe are extremely useful, especially when trying to write provably total functions, and I wish they were available in a Safe module like Numeric.Natural. I also want a total function that does the following: -- This function turns an Integer n into a pair of -- (fromInteger (abs n), fromInteger (signum n)). integerToNaturalSign :: Integer -> (Natural, Int) #if 0 -- This is the reference version, except for the fact that numeric literals don't exist yet -- when GHC.Natural is being defined, and fromInteger isn't actually total. integerToNaturalSign n = case compare n 0 of LT -> (fromInteger (negate n), -1) EQ -> (0, 0) GT -> (fromInteger n, 1) #elif !defined(MIN_VERSION_integer_gmp) -- This is like the reference version, except using the newtype wrapper and MagicHash. integerToNaturalSign n = case compare n (intToInteger# 0#) of LT -> (Natural (negateInteger n), I# (-1#)) EQ -> (Natural n, I# 0#) GT -> (Natural n, I# 1#) #else -- We take advantage of the GMP functions and constructors. integerToNaturalSign (Jn# bn) = (bigNatToNatural bn, I# (-1#)) integerToNaturalSign (S# i#) = case isTrue# (i# <# 0#) of True -> (NatS# (int2Word# (negateInt# i#)), I# (-1#)) _ -> (NatS# (int2Word# i#), I# (i# ># 0#)) integerToNaturalSign (Jp# bn) = (bigNatToNatural bn, I# 1#) #endif

Attachments:

attachment.html (text/html — 1.9 KB)

Show replies by date

chessai .

22 Mar 22 Mar

10:55 p.m.

Sure, I don't see why not. I think powModNatural is also safe. Are your criteria for a function worth re-exporting from Numeric.Natural that 1. The function does not have an overloaded variant defined in base (e.g. all the monorphic version of `fromIntegral` in GHC.Natural would be excluded) and 2. The function is total? Thanks On Sun, Mar 22, 2020 at 11:40 AM Zemyla wrote:

...

Functions in GHC.Natural like naturalToWordMaybe and minusNaturalMaybe are extremely useful, especially when trying to write provably total functions, and I wish they were available in a Safe module like Numeric.Natural. I also want a total function that does the following:

-- This function turns an Integer n into a pair of -- (fromInteger (abs n), fromInteger (signum n)). integerToNaturalSign :: Integer -> (Natural, Int) #if 0 -- This is the reference version, except for the fact that numeric literals don't exist yet -- when GHC.Natural is being defined, and fromInteger isn't actually total. integerToNaturalSign n = case compare n 0 of LT -> (fromInteger (negate n), -1) EQ -> (0, 0) GT -> (fromInteger n, 1) #elif !defined(MIN_VERSION_integer_gmp) -- This is like the reference version, except using the newtype wrapper and MagicHash. integerToNaturalSign n = case compare n (intToInteger# 0#) of LT -> (Natural (negateInteger n), I# (-1#)) EQ -> (Natural n, I# 0#) GT -> (Natural n, I# 1#) #else -- We take advantage of the GMP functions and constructors. integerToNaturalSign (Jn# bn) = (bigNatToNatural bn, I# (-1#)) integerToNaturalSign (S# i#) = case isTrue# (i# <# 0#) of True -> (NatS# (int2Word# (negateInt# i#)), I# (-1#)) _ -> (NatS# (int2Word# i#), I# (i# ># 0#)) integerToNaturalSign (Jp# bn) = (bigNatToNatural bn, I# 1#) #endif _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

Zemyla

23 Mar 23 Mar

1:11 a.m.

That pretty much sums it up. On Sun, Mar 22, 2020, 17:55 chessai . wrote:

...

Sure, I don't see why not. I think powModNatural is also safe.

Are your criteria for a function worth re-exporting from Numeric.Natural that

1. The function does not have an overloaded variant defined in base (e.g. all the monorphic version of `fromIntegral` in GHC.Natural would be excluded) and 2. The function is total?

Thanks

On Sun, Mar 22, 2020 at 11:40 AM Zemyla wrote:

...
Functions in GHC.Natural like naturalToWordMaybe and minusNaturalMaybe

are extremely useful, especially when trying to write provably total functions, and I wish they were available in a Safe module like Numeric.Natural. I also want a total function that does the following:

...
-- This function turns an Integer n into a pair of -- (fromInteger (abs n), fromInteger (signum n)). integerToNaturalSign :: Integer -> (Natural, Int) #if 0 -- This is the reference version, except for the fact that numeric

literals don't exist yet

...
-- when GHC.Natural is being defined, and fromInteger isn't actually total. integerToNaturalSign n = case compare n 0 of LT -> (fromInteger (negate n), -1) EQ -> (0, 0) GT -> (fromInteger n, 1) #elif !defined(MIN_VERSION_integer_gmp) -- This is like the reference version, except using the newtype wrapper and MagicHash. integerToNaturalSign n = case compare n (intToInteger# 0#) of LT -> (Natural (negateInteger n), I# (-1#)) EQ -> (Natural n, I# 0#) GT -> (Natural n, I# 1#) #else -- We take advantage of the GMP functions and constructors. integerToNaturalSign (Jn# bn) = (bigNatToNatural bn, I# (-1#)) integerToNaturalSign (S# i#) = case isTrue# (i# <# 0#) of True -> (NatS# (int2Word# (negateInt# i#)), I# (-1#)) _ -> (NatS# (int2Word# i#), I# (i# ># 0#)) integerToNaturalSign (Jp# bn) = (bigNatToNatural bn, I# 1#) #endif _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

chessai .

1:16 a.m.

Sounds reasonable to me. Perhaps others can weigh in. Thanks On Sun, Mar 22, 2020, 6:11 PM Zemyla wrote:

...

That pretty much sums it up.

On Sun, Mar 22, 2020, 17:55 chessai . wrote:

...
Sure, I don't see why not. I think powModNatural is also safe.

Are your criteria for a function worth re-exporting from Numeric.Natural that

1. The function does not have an overloaded variant defined in base (e.g. all the monorphic version of `fromIntegral` in GHC.Natural would be excluded) and 2. The function is total?

Thanks

On Sun, Mar 22, 2020 at 11:40 AM Zemyla wrote:

...
Functions in GHC.Natural like naturalToWordMaybe and minusNaturalMaybe

are extremely useful, especially when trying to write provably total functions, and I wish they were available in a Safe module like Numeric.Natural. I also want a total function that does the following:

...
-- This function turns an Integer n into a pair of -- (fromInteger (abs n), fromInteger (signum n)). integerToNaturalSign :: Integer -> (Natural, Int) #if 0 -- This is the reference version, except for the fact that numeric

literals don't exist yet

...
-- when GHC.Natural is being defined, and fromInteger isn't actually total. integerToNaturalSign n = case compare n 0 of LT -> (fromInteger (negate n), -1) EQ -> (0, 0) GT -> (fromInteger n, 1) #elif !defined(MIN_VERSION_integer_gmp) -- This is like the reference version, except using the newtype wrapper and MagicHash. integerToNaturalSign n = case compare n (intToInteger# 0#) of LT -> (Natural (negateInteger n), I# (-1#)) EQ -> (Natural n, I# 0#) GT -> (Natural n, I# 1#) #else -- We take advantage of the GMP functions and constructors. integerToNaturalSign (Jn# bn) = (bigNatToNatural bn, I# (-1#)) integerToNaturalSign (S# i#) = case isTrue# (i# <# 0#) of True -> (NatS# (int2Word# (negateInt# i#)), I# (-1#)) _ -> (NatS# (int2Word# i#), I# (i# ># 0#)) integerToNaturalSign (Jp# bn) = (bigNatToNatural bn, I# 1#) #endif _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

1931

Age (days ago)

1932

Last active (days ago)

List overview

Download

3 comments

2 participants

participants (2)

chessai .
Zemyla