[Haskell-cafe] A Proposed Law for Foldable?

[Mike Izbicki]

I'd like to throw another law into the ring that is simple and
satisfies the issues raised by David Feuer.  Using the following
definitions:

> class Foldable f where
>     length :: f a -> Int
>     foldMap :: (a -> b) -> f a -> b
>
> disjoint :: (Monoid (f a), Foldable f) => f a -> f a -> Bool
> disjoint f1 f2 = length f1 + length f2 == length (f1 `mappend` f2)

The law is:

> disjoint f1 f2 ==> foldMap f f1 + foldMap f f2 == foldMap f (f1 `mappend` f2)

The main advantage of the law is that it forces foldMap to consider
"every element" of the container, where "every element" is very
loosely defined.  The Foldable instance that considers only the first
element in a list breaks the law.  But David Feuer's Team/IP example
can be made to work with the law.

The inspiration for the law is to treat the Foldable class as a
generalization of the Lebesgue integral.  If you're familiar with
measure theory, foldMap over a set of numbers "should be" the same as
integrating over the set using the discrete measure.  The generalized
definition of disjoint to let us "integrate" over containers other
than sets.  (For example, every list is disjoint to every other list,
but every set is not disjoint to every other set.)

On Sat, Feb 28, 2015 at 9:59 AM, Edward Kmett <ekmett at gmail.com> wrote:
> The Foldable/Monoid constraints are unrelated in behavior, so not
> necessarily.
>
> Why?
>
> At first blush you might think you'd get there via the free theorems, but
> Monoid is only on *, so you can use the inclusion of the argument in the
> Monoid instance to incur further constraints.
>
> newtype Foo a = Foo a deriving (Monoid, Foldable)
>
> now Foo has
>
> instance Foldable Foo
> instance Monoid m => Monoid (Foo m)
>
> it lifts the Monoid to the element inside, but if you fold it you get the
> single value contained inside of it, not mempty.
>
> Now if you want to upgrade this approach all the way to Alternative, rather
> than Monoid then the free theorem arguments start getting teeth.
>
> foldMap f empty = mempty
>
> should then (almost?) hold. I say almost because you might be able to have
> empty be an infinitely large tree which never gets down to values somehow,
> in which case that law would require deciding an infinite amount of work. I
> haven't sat down to prove if the latter is impossible, so I characterize it
> as at least plausible.
>
> -Edward
>
> On Fri, Feb 27, 2015 at 6:00 PM, Daniel Díaz <diaz.carrete at gmail.com> wrote:
>>
>> Hi,
>>
>> Sorry for the slight derail, but I wanted to ask the following doubt: if a
>> Foldable type also happens to be a Monoid (say, like Set) does that
>> automatically imply that toList mempty = [] ?
>>
>> On Friday, February 27, 2015 at 8:18:05 PM UTC+1, Gershom B wrote:
>>>
>>> On February 27, 2015 at 1:39:10 AM, David Feuer (david... at gmail.com)
>>> wrote:
>>> > I am still struggling to understand why you want this to be a law for
>>> > Foldable. It seems an interesting property of some Foldable instances,
>>> > but, unlike Edward Kmett's proposed monoid morphism law, it's not
>>> > clear to me how you can use this low to prove useful properties of
>>> > programs. Could you explain?
>>>
>>> I think there are a number of purposes for laws. Some can be thought of
>>> as "suggested rewrite rules" -- and the monoid morphism law is one such, as
>>> are many related free approaches.
>>>
>>> Note that the monoid morphism law that Edward provides is _not_ a
>>> "proposed" law -- it is an "almost free theorem" -- given a monoid morphism,
>>> it follows for free for any Foldable. There is no possible foldable instance
>>> that can violate this law, assuming you have an actual monoid morphism.
>>>
>>> So Edward may have proposed adding it to the documentation (which makes
>>> sense to me) -- but it provides absolutely no guidance or constraints as to
>>> what an "allowable" instance of Foldable is or is not.
>>>
>>> But there are other reasons for laws than just to provide rewrite rules,
>>> even though it is often desirable to express laws in such terms. Consider
>>> the first Functor law for example -- fmap id === id. Now clearly we can use
>>> it to go eliminate a bunch of "fmap id" calls in our program, should we have
>>> had them. But when would that ever be the case? Instead, the law is
>>> important because it _restricts_ the range of allowable instances -- and so
>>> if you know you have a data type, and you know it has a functor instance,
>>> you then know what that functor instance must do, without looking at the
>>> source code.
>>>
>>>
>>
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>