<div><div dir="auto">Hello!</div><div dir="auto"><br></div><div dir="auto">Am I correct in reading the example definitions you provided as being the greatest fixed points?</div><br><div class="gmail_quote"><div dir="ltr">On Fri, Dec 14, 2018 at 12:58 AM David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div dir="ltr"><div dir="ltr">Some of it, for sure. Where Capriotti mentioned "It's a fixpoint, but not the least," this fixes it. Another potentially interesting relaxation would be</div><div dir="ltr"><br></div><div dir="ltr"><div dir="auto"> some v >= (:) <$> v <*> many v</div><div dir="auto"> many v >= some v <|> pure []</div><div dir="auto"><br></div><div>but that seems considerably more likely to limit practically useful reasoning.</div></div></div></div><br><div class="gmail_quote"><div dir="ltr">On Fri, Dec 14, 2018 at 12:47 AM Gershom B <<a href="mailto:gershomb@gmail.com" target="_blank">gershomb@gmail.com</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"><div><div style="font-family:Helvetica,Arial;font-size:13px">Some interesting prior discussion on the topic. I haven’t worked out how much of what’s discussed there would do better in this setting… <a href="https://www.reddit.com/r/haskell/comments/2j8bvl/laws_of_some_and_many/" target="_blank">https://www.reddit.com/r/haskell/comments/2j8bvl/laws_of_some_and_many/</a></div><div style="font-family:Helvetica,Arial;font-size:13px"><br></div><div style="font-family:Helvetica,Arial;font-size:13px">That said, I think this probably is a good improvement.</div><div style="font-family:Helvetica,Arial;font-size:13px"><br></div><div style="font-family:Helvetica,Arial;font-size:13px">-g</div> <br> <div class="m_4414973243449251346gmail-m_4218940050289965188gmail_signature"></div> <br><p class="m_4414973243449251346gmail-m_4218940050289965188airmail_on">On December 14, 2018 at 12:30:52 AM, David Feuer (<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>) wrote:</p> <blockquote type="cite" class="m_4414973243449251346gmail-m_4218940050289965188clean_bq"><span><div><div></div><div>
<div dir="ltr">Note: even making liftA2 and (<|>) lazy ends
up leading to some bottoms that the proposed definition avoids. I
don't honestly understand just why that is.</div>
<br>
<div class="gmail_quote">
<div dir="ltr">On Fri, Dec 14, 2018 at 12:22 AM David Feuer
<<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</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">
<div dir="ltr">With the current law and (default) definitions,
<div><br></div>
<div>some (x :*: y) = liftA2 (:) (x :*: y) (many (x :*: y))</div>
<div>many (x :*: y) = some (x :*: y) <|> pure []</div>
<div><br></div>
<div>Since liftA2 is strict in its third argument, and (<|>)
is strict in its first argument, some = many = const _|_ regardless
of the underlying functors.</div>
<div><br></div>
<div>On the other hand, with the proposed law and the proposed
definitions, the methods will behave well for products if they
behave well for the underlying functors.</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr">On Fri, Dec 14, 2018 at 12:12 AM Gershom B
<<a href="mailto:gershomb@gmail.com" target="_blank">gershomb@gmail.com</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">
<div>
<div style="font-family:Helvetica,Arial;font-size:13px">Can you
give an example of where the new definitions and current
definitions of functor products would yield different
behavior?</div>
<div style="font-family:Helvetica,Arial;font-size:13px">
<br></div>
<div style="font-family:Helvetica,Arial;font-size:13px">-g</div>
<br>
<div class="m_4414973243449251346gmail-m_4218940050289965188gmail-m_-6220873419669364604gmail-m_-3317407928059190030gmail_signature">
</div>
<br>
<p class="m_4414973243449251346gmail-m_4218940050289965188gmail-m_-6220873419669364604gmail-m_-3317407928059190030airmail_on">
On December 14, 2018 at 12:03:32 AM, David Feuer (<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>) wrote:</p>
<blockquote type="cite" class="m_4414973243449251346gmail-m_4218940050289965188gmail-m_-6220873419669364604gmail-m_-3317407928059190030clean_bq">
<div>
<div>
<div dir="ltr">
<div dir="auto"><span>Currently, we document this law:</span>
<div dir="auto"><span><br></span></div>
<div dir="auto">
<div dir="auto"><span>> If defined, some and many should be the
least solutions of the equations:</span></div>
<div dir="auto"><span>></span></div>
<div dir="auto"><span>> some v = (:) <$> v
<*> many v</span></div>
<div dir="auto"><span>> many v = some v <|>
pure []</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span>This seems a bit too strong. I believe we
should weaken "should be the least solutions of" to "should obey".
This allows non-bottoming implementations for more types. I would
be surprised if the change would meaningfully weaken the value of
the law for reasoning about real programs.</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span>For example, we currently
require</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span> some Nothing =
Nothing</span></div>
<div dir="auto"><span> some (Just x) =
_|_</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span> many Nothing = Just
[]</span></div>
<div dir="auto"><span> many (Just x) =
_|_</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span>But if we weaken the law, we could instead
use</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span> some Nothing =
Nothing</span></div>
<div dir="auto"><span> some (Just x) = Just (repeat
x)</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span> many Nothing = Just
[]</span></div>
<div dir="auto"><span> many (Just x) = Just (repeat
x)</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span>This seems strictly, albeit slightly, more
interesting.</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span>More significantly, I think, the instance for
functor products can also get much better-defined:</span></div>
<div><span><br></span></div>
<div><span> some (x :*: y) = some x :*: some
y</span></div>
<div><span> many (x :*: y) = many x :*: many
y</span></div>
<div><span><br></span></div>
<div><span>That strikes me as an improvement that may actually be
of some practical value.</span></div>
</div>
</div>
</div>
<span>_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</span></div>
</div>
</blockquote>
</div>
</blockquote>
</div>
</blockquote>
</div>
_______________________________________________<br>Libraries mailing list<br><a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br></div></div></span></blockquote></div></blockquote></div>
_______________________________________________<br>
Libraries mailing list<br>
<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>
</blockquote></div></div>