Constraints on definition of `length` should be strengthened

[Anthony Clayden]

> On Wed Apr 5 16:15:48 UTC 2017, Paolo Giarrusso wrote:
> Thanks for all the mails, but I'm still missing an answer,
> so I must have done something wrong.

:-) Thanks Paolo, you've done nothing wrong IMHO.

You've done the community a service by pointing out an
omission in the docos.

It's the same failure to communicate clearly that's given
rise to the whole FTP kerfuffle.

> I guess I didn't explain my question well.
> Or nobody thinks it's worth answering (in which case,
sorry, but I'd
> prefer to be told I'm misguided, over having the question
ignored).

I think your original question was clear.
I think it is very well worth answering.
That is: answering what are the 'Laws' for Foldable?
I've been waiting patiently for Libraries HQ to:
* explain the applicable Laws
* acknowledge they're not doco'd
* volunteer to fix that

> ... I'm really asking a different question: do length docs
actually
> give a complete specification—it still seems to me they
don't.

I agree they don't.

> ...
> But that's very confusing: can really debate on `length
(a, b) = 1`
> have continued for so long, without noticing that `length
= getSum .
> foldMap (Sum . const 1)` is a fundamental assumption and
is not
> mandated by anything written down? I assume I must be
missing
> something, which is why I asked.

The only reply I've seen [from David F, you copied below,
 apologies if I've missed others]
doesn't give any "fundamental assumption".
It only says "should be quite well-behaved"
and "pretty much everybody agrees on".
I'm not 'getting at' David, at least he answered.

I agree with your intuition that
Foldable length = length . toList

But that just pushes the question back to
what are the Laws for `toList`?
Note that `toList` has been in Foldable 'for ever'.
And instance Foldable Maybe 'for ever'.
That returns a 0-or-1 length list.

Contrast that `instance Foldable ((,) b)`
appeared in GHC 7.8 ~2014,
along with `instance Foldable Either`.

> Of all incomplete docs, this matters more
> since `length (a, b)` is so surprising.

I'd say the surprising bit is `toList (a, b)`.
`length` is just a consequence.

Cue another long thread on `toList`.

I'm inclined to agree with Edward K,
that there's only one possible definition for `toList`
-- that is, if we accept `instance Foldable ((,) b).

Cue another long thread on tuple instances,
and the Either instance.

> The unsuspecting looking at docs lacks the facts needed to
> infer this wart. Spelling out implications would IMHO be
even better,
> for the same reason people state theorems even though they
can be
> proved, but maybe some disagree. A complete spec would be
a starting
> point.

Yes. In particular, the conspicuous lack of docos
is now wildly at variance with all the tutorial/intro texts,
which explain `length` as for Lists.

I plain think that `length` should be Lists-only;
there should be some other name for Foldable's size.

>>> On 3 April 2017 at 17:59, David Feuer wrote:
>>> length should be quite well-behaved relative to foldMap:
>>>
>>> length = getSum . foldMap (Sum . const 1)

>> Thanks, that looks useful to add to docs. I was thinking
of `length =
>> length . toList`.

>>> Another law pretty much everyone agrees on is that *if*
f is an instance of
>>> Traversable, then
>>>
>>> foldMap = foldMapDefault



AntC