# Proposal: Change Alternative law for some and many

10 messages
Open this post in threaded view
|

## Proposal: Change Alternative law for some and many

 Currently, we document this law:> If defined, some and many should be the least solutions of the equations:>>   some v = (:) <\$> v <*> many v>   many v = some v <|> pure []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.For example, we currently require    some Nothing = Nothing    some (Just x) = _|_    many Nothing = Just []    many (Just x) = _|_But if we weaken the law, we could instead use    some Nothing = Nothing    some (Just x) = Just (repeat x)    many Nothing = Just []    many (Just x) = Just (repeat x)This seems strictly, albeit slightly, more interesting.More significantly, I think, the instance for functor products can also get much better-defined:    some (x :*: y) = some x :*: some y    many (x :*: y) = many x :*: many yThat strikes me as an improvement that may actually be of some practical value. _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Open this post in threaded view
|

## Re: Proposal: Change Alternative law for some and many

 Can you give an example of where the new definitions and current definitions of functor products would yield different behavior?-g On December 14, 2018 at 12:03:32 AM, David Feuer ([hidden email]) wrote: Currently, we document this law: > If defined, some and many should be the least solutions of the equations: > >   some v = (:) <\$> v <*> many v >   many v = some v <|> pure [] 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. For example, we currently require     some Nothing = Nothing     some (Just x) = _|_     many Nothing = Just []     many (Just x) = _|_ But if we weaken the law, we could instead use     some Nothing = Nothing     some (Just x) = Just (repeat x)     many Nothing = Just []     many (Just x) = Just (repeat x) This seems strictly, albeit slightly, more interesting. More significantly, I think, the instance for functor products can also get much better-defined:     some (x :*: y) = some x :*: some y     many (x :*: y) = many x :*: many y That strikes me as an improvement that may actually be of some practical value. _______________________________________________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
Open this post in threaded view
|

## Re: Proposal: Change Alternative law for some and many

 With the current law and (default) definitions,some (x :*: y) = liftA2 (:) (x :*: y) (many (x :*: y))many (x :*: y) = some (x :*: y) <|> pure []Since liftA2 is strict in its third argument, and (<|>) is strict in its first argument, some = many = const _|_ regardless of the underlying functors.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.On Fri, Dec 14, 2018 at 12:12 AM Gershom B <[hidden email]> wrote:Can you give an example of where the new definitions and current definitions of functor products would yield different behavior?-g On December 14, 2018 at 12:03:32 AM, David Feuer ([hidden email]) wrote: Currently, we document this law: > If defined, some and many should be the least solutions of the equations: > >   some v = (:) <\$> v <*> many v >   many v = some v <|> pure [] 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. For example, we currently require     some Nothing = Nothing     some (Just x) = _|_     many Nothing = Just []     many (Just x) = _|_ But if we weaken the law, we could instead use     some Nothing = Nothing     some (Just x) = Just (repeat x)     many Nothing = Just []     many (Just x) = Just (repeat x) This seems strictly, albeit slightly, more interesting. More significantly, I think, the instance for functor products can also get much better-defined:     some (x :*: y) = some x :*: some y     many (x :*: y) = many x :*: many y That strikes me as an improvement that may actually be of some practical value. _______________________________________________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
Open this post in threaded view
|

## Re: Proposal: Change Alternative law for some and many

 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.On Fri, Dec 14, 2018 at 12:22 AM David Feuer <[hidden email]> wrote:With the current law and (default) definitions,some (x :*: y) = liftA2 (:) (x :*: y) (many (x :*: y))many (x :*: y) = some (x :*: y) <|> pure []Since liftA2 is strict in its third argument, and (<|>) is strict in its first argument, some = many = const _|_ regardless of the underlying functors.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.On Fri, Dec 14, 2018 at 12:12 AM Gershom B <[hidden email]> wrote:Can you give an example of where the new definitions and current definitions of functor products would yield different behavior?-g On December 14, 2018 at 12:03:32 AM, David Feuer ([hidden email]) wrote: Currently, we document this law: > If defined, some and many should be the least solutions of the equations: > >   some v = (:) <\$> v <*> many v >   many v = some v <|> pure [] 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. For example, we currently require     some Nothing = Nothing     some (Just x) = _|_     many Nothing = Just []     many (Just x) = _|_ But if we weaken the law, we could instead use     some Nothing = Nothing     some (Just x) = Just (repeat x)     many Nothing = Just []     many (Just x) = Just (repeat x) This seems strictly, albeit slightly, more interesting. More significantly, I think, the instance for functor products can also get much better-defined:     some (x :*: y) = some x :*: some y     many (x :*: y) = many x :*: many y That strikes me as an improvement that may actually be of some practical value. _______________________________________________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
Open this post in threaded view
|

## Re: Proposal: Change Alternative law for some and many

 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… https://www.reddit.com/r/haskell/comments/2j8bvl/laws_of_some_and_many/That said, I think this probably is a good improvement.-g On December 14, 2018 at 12:30:52 AM, David Feuer ([hidden email]) wrote: 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. On Fri, Dec 14, 2018 at 12:22 AM David Feuer <[hidden email]> wrote: With the current law and (default) definitions, some (x :*: y) = liftA2 (:) (x :*: y) (many (x :*: y)) many (x :*: y) = some (x :*: y) <|> pure [] Since liftA2 is strict in its third argument, and (<|>) is strict in its first argument, some = many = const _|_ regardless of the underlying functors. 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. On Fri, Dec 14, 2018 at 12:12 AM Gershom B <[hidden email]> wrote: Can you give an example of where the new definitions and current definitions of functor products would yield different behavior? -g On December 14, 2018 at 12:03:32 AM, David Feuer ([hidden email]) wrote: Currently, we document this law: > If defined, some and many should be the least solutions of the equations: > >   some v = (:) <\$> v <*> many v >   many v = some v <|> pure [] 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. For example, we currently require     some Nothing = Nothing     some (Just x) = _|_     many Nothing = Just []     many (Just x) = _|_ But if we weaken the law, we could instead use     some Nothing = Nothing     some (Just x) = Just (repeat x)     many Nothing = Just []     many (Just x) = Just (repeat x) This seems strictly, albeit slightly, more interesting. More significantly, I think, the instance for functor products can also get much better-defined:     some (x :*: y) = some x :*: some y     many (x :*: y) = many x :*: many y That strikes me as an improvement that may actually be of some practical value. _______________________________________________ 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_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Open this post in threaded view
|

## Re: Proposal: Change Alternative law for some and many

 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   some v >= (:) <\$> v <*> many v   many v >= some v <|> pure []but that seems considerably more likely to limit practically useful reasoning.On Fri, Dec 14, 2018 at 12:47 AM Gershom B <[hidden email]> wrote: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… https://www.reddit.com/r/haskell/comments/2j8bvl/laws_of_some_and_many/That said, I think this probably is a good improvement.-g On December 14, 2018 at 12:30:52 AM, David Feuer ([hidden email]) wrote: 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. On Fri, Dec 14, 2018 at 12:22 AM David Feuer <[hidden email]> wrote: With the current law and (default) definitions, some (x :*: y) = liftA2 (:) (x :*: y) (many (x :*: y)) many (x :*: y) = some (x :*: y) <|> pure [] Since liftA2 is strict in its third argument, and (<|>) is strict in its first argument, some = many = const _|_ regardless of the underlying functors. 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. On Fri, Dec 14, 2018 at 12:12 AM Gershom B <[hidden email]> wrote: Can you give an example of where the new definitions and current definitions of functor products would yield different behavior? -g On December 14, 2018 at 12:03:32 AM, David Feuer ([hidden email]) wrote: Currently, we document this law: > If defined, some and many should be the least solutions of the equations: > >   some v = (:) <\$> v <*> many v >   many v = some v <|> pure [] 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. For example, we currently require     some Nothing = Nothing     some (Just x) = _|_     many Nothing = Just []     many (Just x) = _|_ But if we weaken the law, we could instead use     some Nothing = Nothing     some (Just x) = Just (repeat x)     many Nothing = Just []     many (Just x) = Just (repeat x) This seems strictly, albeit slightly, more interesting. More significantly, I think, the instance for functor products can also get much better-defined:     some (x :*: y) = some x :*: some y     many (x :*: y) = many x :*: many y That strikes me as an improvement that may actually be of some practical value. _______________________________________________ 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 _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Open this post in threaded view
|

## Re: Proposal: Change Alternative law for some and many

 Hello!Am I correct in reading the example definitions you provided as being the greatest fixed points?On Fri, Dec 14, 2018 at 12:58 AM David Feuer <[hidden email]> wrote: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   some v >= (:) <\$> v <*> many v   many v >= some v <|> pure []but that seems considerably more likely to limit practically useful reasoning.On Fri, Dec 14, 2018 at 12:47 AM Gershom B <[hidden email]> wrote: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… https://www.reddit.com/r/haskell/comments/2j8bvl/laws_of_some_and_many/That said, I think this probably is a good improvement.-g On December 14, 2018 at 12:30:52 AM, David Feuer ([hidden email]) wrote: 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. On Fri, Dec 14, 2018 at 12:22 AM David Feuer <[hidden email]> wrote: With the current law and (default) definitions, some (x :*: y) = liftA2 (:) (x :*: y) (many (x :*: y)) many (x :*: y) = some (x :*: y) <|> pure [] Since liftA2 is strict in its third argument, and (<|>) is strict in its first argument, some = many = const _|_ regardless of the underlying functors. 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. On Fri, Dec 14, 2018 at 12:12 AM Gershom B <[hidden email]> wrote: Can you give an example of where the new definitions and current definitions of functor products would yield different behavior? -g On December 14, 2018 at 12:03:32 AM, David Feuer ([hidden email]) wrote: Currently, we document this law: > If defined, some and many should be the least solutions of the equations: > >   some v = (:) <\$> v <*> many v >   many v = some v <|> pure [] 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. For example, we currently require     some Nothing = Nothing     some (Just x) = _|_     many Nothing = Just []     many (Just x) = _|_ But if we weaken the law, we could instead use     some Nothing = Nothing     some (Just x) = Just (repeat x)     many Nothing = Just []     many (Just x) = Just (repeat x) This seems strictly, albeit slightly, more interesting. More significantly, I think, the instance for functor products can also get much better-defined:     some (x :*: y) = some x :*: some y     many (x :*: y) = many x :*: many y That strikes me as an improvement that may actually be of some practical value. _______________________________________________ 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 _______________________________________________ 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
Open this post in threaded view
|