[Haskell-cafe] A Proposed Law for Foldable?

Thu Feb 12 21:31:45 UTC 2015

What I kind of like about this proposal is that it makes it illegal
for potentially-infinite snoc-lists to be Foldable, since toList will
produce _|_ on an infinite snoc-list. On the other hand, this is
reason enough to make a lot of people hate it. The GADT problem Edward
Kmett points out seems like a more serious issue. The solution is to
make  Functor f => Foldable f, which will probably eliminate another
four fifths of the supporters of your idea.

On Thu, Feb 12, 2015 at 3:49 PM, Gershom B <gershomb at gmail.com> wrote:
> I agree the third issue raised is a pretty tricky one. GADTs can effectively
> pack in a "secret a" that is nonetheless accessible, or a "secret a -> a"
> for that matter...
>
> A quick and dirty repair is to just say that the law only applies to data
> types that do not quantify over dictionaries (and passes no judgement on
> data types which do). In such a case I think it is still useful, but
> unfortunately specialized.
>
> I absolutely think a more general law could be possible, but it could be
> rather tricky to state... Perhaps it could be stated by, instead of
> quantifying over _all_ a, quantifying over a specific "generic a" which
> promises it has no dictionaries with a positive occurrence of `a`. This
> maintains the spirit properly, but makes the statement more complex.
>
> With regards to Atze's question, the fact that such a law could rule out
> giving an arbitrary type an instance where "foldMap = mempty" is exactly the
> sort of thing we would like to see.
>
> --gershom
>
>
> On Thu, Feb 12, 2015 at 3:36 PM, Edward Kmett <ekmett at gmail.com> wrote:
>>
>> There are 3 cases ruled out by this law. Two of them I'd have no trouble
>> seeing go, the third one I think damages it beyond repair.
>>
>> First,
>>
>> `foldMap = mempty`
>>
>> is currently an admissable definition of foldMap for anything that is not
>> Traversable.
>>
>> The law effectively talks backwards and ensures that you have to give back
>> info on every 'a' in the container, so this is ruled out for any container
>> that actually 'contains' an a.
>>
>> I'm pretty much okay with that case being ruled out.
>>
>> Second,
>>
>> There are instances such as the Foldable instance for `Machine` in the
>> machines package. Here it starves the machine for input and takes the output
>> and folds over it.
>>
>> However, these are not 'all of the 'a's it is possible to generate with
>> such a machine, as you can construct a function (Machine ((->) b) a -> Maybe
>> a) that feeds the machine a 'b' and then gets out an 'a' that would not
>> occur in toList.
>>
>> One could argue that this Foldable violates the spirit of Foldable.
>>
>> I'm somewhat less okay with that case being ruled out as folks have found
>> it useful, but I could accept it.
>>
>> Third,
>>
>> In the presence of GADTs, the fact that Foldable only accepts 'f' in
>> negative position means that 'f' might be a GADT, telling us more about `a`,
>> despite your function being parametric.
>>
>> e.g. it could carry around a Num constraint on its argument. Extracting
>> this dictionary from the GADT would enable sum :: Num a => f a -> a to be
>> used in your function (forall a. f a -> Maybe a), preventing parametricity
>> from providing the insurance you seek.
>>
>> This means that your law would rule out any `Foldable` that exploits
>> GADT-like properties.
>>
>> A version of `Set` where the data type carries around the `Ord` instance
>> internally, could for instance instantiate `elem` in log time. That example
>> becomes only marginally safe under your law because of `min` and `max` being
>> in Ord and producing "new" a's, but it also rules out similar O(1)
>> optimizations for sum or product in other potential containers, which could
>> carry Num.
>>
>> These I'm much more reluctant to let go.
>>
>> You might be able to repair your law by also quantifying over `f` with a
>> Foldable constraint or some such, but that re-admits the former 2 laws and
>> seems to make it vacuous.
>>
>> -Edward
>>
>>
>> On Thu, Feb 12, 2015 at 2:59 PM, Atze van der Ploeg <atzeus at gmail.com>
>> wrote:
>>>
>>> Hi Gershom!
>>>
>>> Do you have an example where this law allows us to conclude something
>>> interesting we otherwise would not have been able to conclude?
>>>
>>> Cheers,
>>>
>>> Atze
>>>
>>> On Feb 12, 2015 8:47 PM, "Gershom B" <gershomb at gmail.com> wrote:
>>>>
>>>> For a long time, many people, including me, have said that "Foldable has
>>>> no laws" (or Foldable only has free laws) -- this is true, as it stands,
>>>> with the exception that Foldable has a non-free law in interaction with
>>>> Traversable (namely that it act as a proper specialization of Traversable
>>>> methods). However, I believe that there is a good law we can give for
>>>> Foldable.
>>>>
>>>> I earlier explored this in a paper presented at IFL 2014 but
>>>> (rightfully) rejected from the IFL post-proceedings.
>>>> (http://gbaz.github.io/slides/buildable2014.pdf). That paper got part of the
>>>> way there, but I believe now have a better approach on the question of a
>>>> Foldable law -- as sketched below.
>>>>
>>>> I think I now (unlike in the paper) can state a succinct law for
>>>> Foldable that has desired properties: 1) It is not "free" -- it can be
>>>> violated, and thus stating it adds semantic content. 2) We typically expect
>>>> it to be true. 3) There are no places where I can see an argument for
>>>> violating it.
>>>>
>>>> If it pans out, I intend to pursue this and write it up more formally,
>>>> but given the current FTP discussion I thought it was worth documenting this
>>>> earlier rather than later. For simplicity, I will state this property in
>>>> terms of `toList` although that does not properly capture the infinite
>>>> cases. Apologies for what may be nonstandard notation.
>>>>
>>>> Here is the law I think we should discuss requiring:
>>>>
>>>> * * *
>>>> Given Foldable f, then
>>>> forall (g :: forall a. f a -> Maybe a), (x :: f a). case g x of Just a
>>>> --> a `elem` toList x
>>>> * * *
>>>>
>>>> Since we do not require `a` to be of type `Eq`, note that the `elem`
>>>> function given here is not internal to Haskell, but in the metalogic.
>>>>
>>>> Furthermore, note that the use of parametricity here lets us make an
>>>> "end run" around the usual problem of giving laws to Foldable -- rather than
>>>> providing an interaction with another class, we provide a claim about _all_
>>>> functions of a particular type.
>>>>
>>>> Also note that the functions `g` we intend to quantify over are
>>>> functions that _can be written_ -- so we can respect the property of data
>>>> structures to abstract over information. Consider
>>>>
>>>> data Funny a = Funny {hidden :: a, public :: [a]}
>>>>
>>>> instance Foldable Funny where
>>>>     foldMap f x = foldMap f (public x)
>>>>
>>>> Now, if it is truly impossible to ever "see" hidden (i.e. it is not
>>>> exported, or only exported through a semantics-breaking "Internal" module),
>>>> then the Foldable instance is legitimate. Otherwise, the Foldable instance
>>>> is illegitimate by the law given above.
>>>>
>>>> I would suggest the law given is "morally" the right thing for Foldable
>>>> -- a Foldable instance for `f` should suggest that it gives us "all the as
>>>> in any `f a`", and so it is, in some particular restricted sense, initial
>>>> among functions that extract as.
>>>>
>>>> I do not suggest we add this law right away. However, I would like to
>>>> suggest considering it, and I believe it (or a cleaned-up variant) would
>>>> help us to see Foldable as a more legitimately lawful class that not only
>>>> provides conveniences but can be used to aid reasoning.
>>>>
>>>> Relating this to adjointness, as I do in the IFL preprint, remains
>>>> future work.
>>>>
>>>> Cheers,
>>>> Gershom
>>>>
>>>> _______________________________________________
>>>> Haskell-Cafe mailing list
>>>> Haskell-Cafe at haskell.org
>>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>>
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>