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