Export functions on Natural in Numeric.Natural

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Export functions on Natural in Numeric.Natural

Zemyla
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Export functions on Natural in Numeric.Natural

chessai .
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 <[hidden email]> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Export functions on Natural in Numeric.Natural

Zemyla
That pretty much sums it up.

On Sun, Mar 22, 2020, 17:55 chessai . <[hidden email]> 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 <[hidden email]> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Export functions on Natural in Numeric.Natural

chessai .
Sounds reasonable to me. Perhaps others can weigh in.

Thanks

On Sun, Mar 22, 2020, 6:11 PM Zemyla <[hidden email]> wrote:
That pretty much sums it up.

On Sun, Mar 22, 2020, 17:55 chessai . <[hidden email]> 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 <[hidden email]> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries