<div><div dir="auto">I understand that in terms of the specified applicative operations it wouldn’t work. </div></div><div dir="auto"><br></div><div dir="auto">I guess my confusion is that I think of some and many combinators in terms of parser combinators style behavior, where some p can return any positive length list of consecutive values. </div><div dir="auto"><br></div><div dir="auto">If we were to model these algrbrsically as formal power series </div><div dir="auto"><br></div><div dir="auto">I’d think of many x = sum_k (x^k / k! ) = exp x</div><div dir="auto"><br></div><div dir="auto">And then some x = many x -1. </div><div dir="auto">—- because size zero products of x aren’t a valid element </div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto">A lot of expressive power in Haskell comes from being able to use laziness to have the same code work on values that act strict (least fixed point) and those which arent (greatest fixed point). </div><div dir="auto"><br></div><div dir="auto"> My questions are this </div><div dir="auto">1) how would this change impact expected behavior of parser combinator libraries using some and many? </div><div dir="auto">2) what is a calculation I can do today with some and many that I can’t do with this change?</div><div dir="auto">3) what’s a calculation I can do with some and many only once we have this change ? </div><div dir="auto"><br></div><div><br><div class="gmail_quote"><div dir="ltr">On Fri, Dec 14, 2018 at 12:18 PM 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">No, you can't return just a singleton list. If many (Just 3) = Just [3], then</div><div>some (Just 3) = liftA2 (:) (Just 3) (Just [3]) = Just [3,3]. But then</div><div>many (Just 3) = some (Just 3) <|> pure [] = Just [3,3], a contradiction.</div><div>If instead some (Just 3) = Just [3], then many (Just 3) = Just [3] <|> pure [] = Just [3],</div><div>which gets us back where we started.</div><div dir="ltr"><br></div><div dir="ltr">The definitions I gave for Maybe (and also the ones for [], which I haven't mentioned) are equivalent to "lazifying" the defaults in a straightforward manner.</div><div dir="ltr"><br></div><div> -- This one is the default</div><div dir="ltr"><div dir="ltr"> some v = liftA2 (:) v (many v)</div><div dir="ltr"><br></div><div> -- This one is much like the default. But note that (barring non-termination),</div><div> -- isJust (m <|> pure []) == True</div><div> -- So we push the case match under the constructor application:</div><div dir="ltr"> many v = Just $</div><div dir="ltr"> case some v <|> pure [] of</div><div dir="ltr"> Just x -> x</div><div dir="ltr"><br></div><div>These definitions give the same results as the repeat-based ones I showed before. Are these greatest fixed points? I believe so, but I don't really know enough about domain theory and such to say for sure.</div></div></div></div><br><div class="gmail_quote"><div dir="ltr">On Fri, Dec 14, 2018 at 10:11 AM Carter Schonwald <<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@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 dir="auto">I guess I’m just surprised that some can’t return just a singleton list of x. Or maybe I’m reading the notation of this discussion wrong. </div></div><div><br><div class="gmail_quote"><div dir="ltr">On Fri, Dec 14, 2018 at 9:49 AM Carter Schonwald <<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@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 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></div><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" 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"><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_1814591694555870823gmail-m_-2886692898960877646m_-4626506941825712851m_4414973243449251346gmail-m_4218940050289965188gmail_signature"></div> <br><p class="m_1814591694555870823gmail-m_-2886692898960877646m_-4626506941825712851m_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_1814591694555870823gmail-m_-2886692898960877646m_-4626506941825712851m_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_1814591694555870823gmail-m_-2886692898960877646m_-4626506941825712851m_4414973243449251346gmail-m_4218940050289965188gmail-m_-6220873419669364604gmail-m_-3317407928059190030gmail_signature">
</div>
<br>
<p class="m_1814591694555870823gmail-m_-2886692898960877646m_-4626506941825712851m_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_1814591694555870823gmail-m_-2886692898960877646m_-4626506941825712851m_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>
</blockquote></div></div>
</blockquote></div>
</blockquote></div></div>