<div dir="ltr">ooo, thats a good point about lattices/partial orders! (we like those here too, but sometimes forget :) )<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Feb 5, 2020 at 1:34 PM 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:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Well, I see your arguments, but cannot help the feeling that you are <br>
reasoning from a specific instance family of semirings, namely numerical <br>
ones (N, Z, Q, ...).<br>
<br>
For idempotent semirings (e.g. the example I gave), repetitively adding <br>
one gets you nowhere.  (Cf. also lattices, many of which are semirings.)<br>
<br>
I'd be convinced if Natural was something like the free semiring, but <br>
this is certainly not the case.<br>
<br>
Semirings are really diverse, I don't think the Semiring class should be <br>
hijacked for a particular flavor of semirings.  We do not have any such <br>
pretext for Semigroup or Monoid either.<br>
<br>
Enjoy the diversity at <a href="https://en.wikipedia.org/wiki/Semiring" rel="noreferrer" target="_blank">https://en.wikipedia.org/wiki/Semiring</a><br>
<br>
On 2020-02-04 17:32, Zemyla wrote:<br>
> It really doesn't matter if it's not "interesting" or not surjective for <br>
> some Semirings. It should be included, because:<br>
> <br>
> (a) Even for semirings where it is "interesting", it's not surjective <br>
> (for instance, Rational or Double)<br>
> (b) It's a method with a default definition, so you don't have to expend <br>
> any mental effort on it<br>
> (c) A lot of instances have uninteresting methods: for instance, (*>) <br>
> and (<*) for Applicative ((->) e) are const id and const respectively. <br>
> Haskell adds methods to classes when they're always possible and <br>
> sometimes useful/interesting/faster, rather than when they're always <br>
> interesting.<br>
> (d) It's useful for Semiring-generic methods and instances.<br>
> (e) It can achieve an asymptotic speedup on some instances. Like, if you <br>
> have Semiring a => Semiring (f a) for some type f, then you can have <br>
> fromNatural n = pure (fromNatural n) instead of doing the whole O(log n) <br>
> song and dance with the default definition. Also, your example admits a <br>
> simple definition:<br>
>    fromNatural n = if n == 0 then S.empty else S.singleton True<br>
> (f) "zero" and "one" can be defined in terms of fromNatural, for <br>
> programmers who only need to define that:<br>
>    zero = fromNatural 0<br>
>    one = fromNatural 1<br>
> This leads to the MINIMAL pragma on Semiring being {-# MINIMAL plus, <br>
> times, (zero, one | fromNatural) #-}<br>
> (g) If it's not included in the class, but in some subclass <br>
> (NaturalSemiring, you proposed), but it's possible from the class, then <br>
> people will just define and use the O(log n) version instead of <br>
> requiring the subclass, leading to wasted effort and duplicated code.<br>
> <br>
> On Tue, Feb 4, 2020, 09:20 Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a> <br>
> <mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>>> wrote:<br>
> <br>
>       > There is a homomorphism from the Naturals to any Semiring<br>
> <br>
>     Sure, but there are many finite semirings where I would not care about<br>
>     such a homomorphism, thus, why force me to define it?<br>
> <br>
>       > fromNatural 0 = zero<br>
>       > fromNatural 1 = one<br>
>       > fromNatural (m + n) = fromNatural m `plus` fromNatural n<br>
>       > fromNatural (m * n) = fromNatural m `times` fromNatural n<br>
> <br>
>     This might not be surjective, and also not very interesting.  For<br>
>     instance consider the semiring<br>
> <br>
>         Set Bool<br>
>         zero  = Set.empty<br>
>         one   = Set.singleton True<br>
>         plus  = Set.union<br>
>         times s t = { x == y | x <- s, y <- t }<br>
> <br>
>     This semiring models variances (covariant = {True}, contravariant =<br>
>     {False}, constant = {}, dontknow = {True,False}).  times is for<br>
>     function<br>
>     composition and plus combination of information.<br>
> <br>
>     The fromNatural targets only the zero/one-fragment since plus is<br>
>     idempotent.  I conjecture there is not a single surjective semiring-hom<br>
>     from Nat to Set Bool.  Thus, a function fromNatural is totally<br>
>     uninteresting for the general case of semirings.<br>
> <br>
>     On 2020-02-04 13:42, Zemyla wrote:<br>
>      > There is a homomorphism from the Naturals to any Semiring, which<br>
>     obeys:<br>
>      ><br>
>      > fromNatural 0 = zero<br>
>      > fromNatural 1 = one<br>
>      > fromNatural (m + n) = fromNatural m `plus` fromNatural n<br>
>      > fromNatural (m * n) = fromNatural m `times` fromNatural n<br>
>      ><br>
>      > The simplest implementation is this, but it's nowhere near the most<br>
>      > efficient:<br>
>      ><br>
>      > fromNatural :: Semiring a => Natural -> a<br>
>      > fromNatural 0 = zero<br>
>      > 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<br>
>      > fromNatural = go 0 zero one<br>
>      >    go i s m n | i `seq` s `seq` m `seq` n `seq` False = undefined<br>
>      >    go _ s _ 0 =  s<br>
>      >    go i s m n<br>
>      >      | testBit n i = go (i + 1) (plus s m) (plus m m) (clearBit n i)<br>
>      >      | otherwise = go (i + 1) s (plus m m) n<br>
>      ><br>
>      > On Tue, Feb 4, 2020, 02:21 Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
>     <mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>><br>
>      > <mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
>     <mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>>>> wrote:<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>
>      ><br>
>      >     I think `fromNatural` should not be part of the `Semiring` class,<br>
>      >     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,<br>
>     rolled our own<br>
>      >     semiring class,<br>
>      ><br>
>      ><br>
>     <a href="https://github.com/agda/agda/blob/master/src/full/Agda/Utils/SemiRing.hs" rel="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>
>      ><br>
>     <a href="https://github.com/agda/agda/blob/64c0c2e813a84f91b3accd7c56efaa53712bc3f5/src/full/Agda/TypeChecking/Positivity/Occurrence.hs#L127-L155" rel="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<br>
>     using for<br>
>      >     short<br>
>      >      > hand?  I think I followed, but for people the libraries list<br>
>      >     might be<br>
>      >      > their first exposure to advanced / graduate abstract<br>
>     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">carter.schonwald@gmail.com</a><br>
>     <mailto:<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>><br>
>     <mailto:<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a> <mailto:<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>>><br>
>      >     <mailto:<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a><br>
>     <mailto:<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>><br>
>      >     <mailto:<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a><br>
>     <mailto:<a href="mailto:carter.schonwald@gmail.com" target="_blank">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">andrew.lelechenko@gmail.com</a><br>
>     <mailto:<a href="mailto:andrew.lelechenko@gmail.com" target="_blank">andrew.lelechenko@gmail.com</a>><br>
>      >     <mailto:<a href="mailto:andrew.lelechenko@gmail.com" target="_blank">andrew.lelechenko@gmail.com</a><br>
>     <mailto:<a href="mailto:andrew.lelechenko@gmail.com" target="_blank">andrew.lelechenko@gmail.com</a>>><br>
>      >     <mailto:<a href="mailto:andrew.lelechenko@gmail.com" target="_blank">andrew.lelechenko@gmail.com</a><br>
>     <mailto:<a href="mailto:andrew.lelechenko@gmail.com" target="_blank">andrew.lelechenko@gmail.com</a>><br>
>      >     <mailto:<a href="mailto:andrew.lelechenko@gmail.com" target="_blank">andrew.lelechenko@gmail.com</a><br>
>     <mailto:<a href="mailto:andrew.lelechenko@gmail.com" target="_blank">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`<br>
>     from `Num` to<br>
>      >      >         `Floating`<br>
>      >      ><br>
>      >      >         I can fully relate your frustration with `abs` and<br>
>      >     `signum` (and<br>
>      >      >         numeric type classes in Haskell altogether). But<br>
>     IMO breaking<br>
>      >      >         both in `Num` and in `Floating` at once is not a<br>
>      >     promising way<br>
>      >      >         to make things proper.<br>
>      >      ><br>
>      >      >         I would rather follow the beaten track of Applicative<br>
>      >     Monad and<br>
>      >      >         Semigroup Monoid proposals and - as a first step -<br>
>      >     introduce a<br>
>      >      >         superclass (probably, borrowing the design from<br>
>     `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<br>
>      >     partial<br>
>      >      >         instance Num Natural),<br>
>      >      >         c) instance Num a => Semiring (Complex a) (in<br>
>     contrast to<br>
>      >      >         instance RealFloat a => Num (Complex a)),<br>
>      >      >         d) newtypes Sum and Product would require only<br>
>     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">Libraries@haskell.org</a> <mailto:<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a>><br>
>     <mailto:<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a> <mailto:<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a>>><br>
>      >     <mailto:<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a> <mailto:<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a>><br>
>     <mailto:<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a> <mailto:<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a>>>><br>
>      >      > <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="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">Libraries@haskell.org</a> <mailto:<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a>><br>
>     <mailto:<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a> <mailto:<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a>>><br>
>      >      > <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="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">Libraries@haskell.org</a> <mailto:<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a>><br>
>     <mailto:<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a> <mailto:<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a>>><br>
>      > <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
>      ><br>
> <br>
</blockquote></div>