<div dir="auto"><div dir="auto">There is a homomorphism from the Naturals to any Semiring, which obeys:</div><div dir="auto"><br></div><div dir="auto">fromNatural 0 = zero</div><div dir="auto">fromNatural 1 = one</div><div dir="auto">fromNatural (m + n) = fromNatural m `plus` fromNatural n</div><div dir="auto">fromNatural (m * n) = fromNatural m `times` fromNatural n</div><div dir="auto"><br></div><div dir="auto">The simplest implementation is this, but it's nowhere near the most efficient:</div><div dir="auto"><br></div><div>fromNatural :: Semiring a => Natural -> a</div><div dir="auto">fromNatural 0 = zero</div><div dir="auto">fromNatural n = one `plus` fromNatural (n - 1)<br><br>One which takes O(log n) time instead of O(n) would go like this:<br><br>fromNatural :: Semiring a => Natural -> a</div><div dir="auto">fromNatural = go 0 zero one</div><div dir="auto"> go i s m n | i `seq` s `seq` m `seq` n `seq` False = undefined<br></div><div dir="auto"> go _ s _ 0 = s</div><div dir="auto"> go i s m n</div><div dir="auto"> | testBit n i = go (i + 1) (plus s m) (plus m m) (clearBit n i)</div><div dir="auto"> | otherwise = go (i + 1) s (plus m m) n</div><div dir="auto"><br></div><div dir="auto"><div class="gmail_quote" dir="auto"><div dir="ltr" class="gmail_attr">On Tue, Feb 4, 2020, 02:21 Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> > class Semiring a where<br>
> zero :: a<br>
> plus :: a -> a -> a<br>
> one :: a<br>
> times :: a -> a -> a<br>
> fromNatural :: Natural -> a<br>
<br>
I think `fromNatural` should not be part of the `Semiring` class, but we <br>
could have an extension (NaturalSemiring) that adds this method.<br>
<br>
In the Agda code base, we have, for lack of a standard, rolled our own <br>
semiring class,<br>
<br>
<a href="https://github.com/agda/agda/blob/master/src/full/Agda/Utils/SemiRing.hs" rel="noreferrer noreferrer" target="_blank">https://github.com/agda/agda/blob/master/src/full/Agda/Utils/SemiRing.hs</a><br>
<br>
and we use it for several finite semirings, e.g.,<br>
<br>
<br>
<a href="https://github.com/agda/agda/blob/64c0c2e813a84f91b3accd7c56efaa53712bc3f5/src/full/Agda/TypeChecking/Positivity/Occurrence.hs#L127-L155" rel="noreferrer noreferrer" target="_blank">https://github.com/agda/agda/blob/64c0c2e813a84f91b3accd7c56efaa53712bc3f5/src/full/Agda/TypeChecking/Positivity/Occurrence.hs#L127-L155</a><br>
<br>
Cheers,<br>
Andreas<br>
<br>
On 2020-02-03 22:34, Carter Schonwald wrote:<br>
> Andrew: could you explain the algebra notation you were using for short <br>
> hand? I think I followed, but for people the libraries list might be <br>
> their first exposure to advanced / graduate abstract algebra (which <br>
> winds up being simpler than most folks expect ;) )<br>
> <br>
> On Fri, Jan 31, 2020 at 4:36 PM Carter Schonwald <br>
> <<a href="mailto:carter.schonwald@gmail.com" target="_blank" rel="noreferrer">carter.schonwald@gmail.com</a> <mailto:<a href="mailto:carter.schonwald@gmail.com" target="_blank" rel="noreferrer">carter.schonwald@gmail.com</a>>> wrote:<br>
> <br>
> that actually sounds pretty sane. I think!<br>
> <br>
> On Fri, Jan 31, 2020 at 3:38 PM Andrew Lelechenko<br>
> <<a href="mailto:andrew.lelechenko@gmail.com" target="_blank" rel="noreferrer">andrew.lelechenko@gmail.com</a> <mailto:<a href="mailto:andrew.lelechenko@gmail.com" target="_blank" rel="noreferrer">andrew.lelechenko@gmail.com</a>>><br>
> wrote:<br>
> <br>
> On Tue, 28 Jan 2020, Dannyu NDos wrote:<br>
> <br>
> > Second, I suggest to move `abs` and `signum` from `Num` to<br>
> `Floating`<br>
> <br>
> I can fully relate your frustration with `abs` and `signum` (and<br>
> numeric type classes in Haskell altogether). But IMO breaking<br>
> both in `Num` and in `Floating` at once is not a promising way<br>
> to make things proper.<br>
> <br>
> I would rather follow the beaten track of Applicative Monad and<br>
> Semigroup Monoid proposals and - as a first step - introduce a<br>
> superclass (probably, borrowing the design from `semirings`<br>
> package):<br>
> <br>
> class Semiring a where<br>
> zero :: a<br>
> plus :: a -> a -> a<br>
> one :: a<br>
> times :: a -> a -> a<br>
> fromNatural :: Natural -> a<br>
> class Semiring a => Num a where ...<br>
> <br>
> Tangible benefits in `base` include:<br>
> a) instance Semiring Bool,<br>
> b) a total instance Semiring Natural (in contrast to a partial<br>
> instance Num Natural),<br>
> c) instance Num a => Semiring (Complex a) (in contrast to<br>
> instance RealFloat a => Num (Complex a)),<br>
> d) newtypes Sum and Product would require only Semiring<br>
> constraint instead of Num.<br>
> <br>
> Best regards,<br>
> Andrew<br>
> <br>
> <br>
> _______________________________________________<br>
> Libraries mailing list<br>
> <a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a> <mailto:<a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a>><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
> <br>
> <br>
> _______________________________________________<br>
> Libraries mailing list<br>
> <a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
> <br>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div></div></div>