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 <
carter.schonwald at gmail.com> 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 <
> carter.schonwald at gmail.com> 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 <david.feuer at gmail.com>
>> 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 <gershomb at gmail.com> 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 (david.feuer at gmail.com)
>>>> 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 <david.feuer at gmail.com>
>>>> 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 <gershomb at gmail.com> 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 (
>>>>>> david.feuer at gmail.com) 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
>>>>>> Libraries at haskell.org
>>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>>>
>>>>>> _______________________________________________
>>>> Libraries mailing list
>>>> Libraries at haskell.org
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>
>>>> _______________________________________________
>>> Libraries mailing list
>>> Libraries at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20181214/8a6840aa/attachment.html>