Proposal: Change Alternative law for some and many

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
10 messages Options
Reply | Threaded
Open this post in threaded view
|

Proposal: Change Alternative law for some and many

David Feuer
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
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: Change Alternative law for some and many

Gershom Bazerman
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
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: Change Alternative law for some and many

David Feuer
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
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: Change Alternative law for some and many

David Feuer
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
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: Change Alternative law for some and many

Gershom Bazerman
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
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: Change Alternative law for some and many

David Feuer
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
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: Change Alternative law for some and many

Carter Schonwald
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
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: Change Alternative law for some and many

Carter Schonwald
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.  

On Fri, Dec 14, 2018 at 9:49 AM Carter Schonwald <[hidden email]> wrote:
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
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: Change Alternative law for some and many

David Feuer
No, you can't return just a singleton list. If many (Just 3) = Just [3], then
some (Just 3) = liftA2 (:) (Just 3) (Just [3]) = Just [3,3]. But then
many (Just 3) = some (Just 3) <|> pure [] = Just [3,3], a contradiction.
If instead some (Just 3) = Just [3], then many (Just 3) = Just [3] <|> pure [] = Just [3],
which gets us back where we started.

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.

  -- This one is the default
  some v = liftA2 (:) v (many v)

  -- This one is much like the default. But note that (barring non-termination),
  -- isJust (m <|> pure []) == True
  -- So we push the case match under the constructor application:
  many v = Just $
    case some v <|> pure [] of
      Just x -> x

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.

On Fri, Dec 14, 2018 at 10:11 AM Carter Schonwald <[hidden email]> wrote:
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.  

On Fri, Dec 14, 2018 at 9:49 AM Carter Schonwald <[hidden email]> wrote:
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
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: Change Alternative law for some and many

Carter Schonwald
I understand that in terms of the specified applicative operations it wouldn’t work.  

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. 

If we were to model these algrbrsically as formal power series 

I’d think of many x = sum_k (x^k / k! ) = exp x

And then some x = many x -1. 
—- because size zero products of x aren’t a valid element 


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). 

 My questions are this 
1) how would this change impact expected behavior of parser combinator libraries using some and many? 
2) what is a calculation I can do today with some and many  that I can’t do with this change?
3) what’s a calculation I can do with some and many only once we have this change ? 


On Fri, Dec 14, 2018 at 12:18 PM David Feuer <[hidden email]> wrote:
No, you can't return just a singleton list. If many (Just 3) = Just [3], then
some (Just 3) = liftA2 (:) (Just 3) (Just [3]) = Just [3,3]. But then
many (Just 3) = some (Just 3) <|> pure [] = Just [3,3], a contradiction.
If instead some (Just 3) = Just [3], then many (Just 3) = Just [3] <|> pure [] = Just [3],
which gets us back where we started.

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.

  -- This one is the default
  some v = liftA2 (:) v (many v)

  -- This one is much like the default. But note that (barring non-termination),
  -- isJust (m <|> pure []) == True
  -- So we push the case match under the constructor application:
  many v = Just $
    case some v <|> pure [] of
      Just x -> x

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.

On Fri, Dec 14, 2018 at 10:11 AM Carter Schonwald <[hidden email]> wrote:
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.  

On Fri, Dec 14, 2018 at 9:49 AM Carter Schonwald <[hidden email]> wrote:
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