Constraints on definition of `length` should be strengthened

[Paolo Giarrusso]

TL;DR. One (implicit?) assumption in recent debates on `length` seems
to be unfounded, because current docs for Foldable are meant to be
much stronger than their actual language, unless I'm missing
something. Clarifications welcome.
If my understanding is right, I'd suggest somebody fixes the docs. One
point is not clear to me, so at present I could not volunteer to fix
them myself.

In recent debates, it was assumed or implied that `length` must be equivalent to

length = length . toList

>  we also have a kind
> system, so we can ignore the name.
> length :: f a -> Int
> We immediately know that values of the kind (* -> *) slot in to the
> value (f), with a kind checker to ensure we get it correct. Therefore,
> we can easily reason about the length of values of kind ((,) a)

I don't quite get how that argument is supposed to proceed. However
that's meant, that seems incorrect because length is a typeclass
method, so even the following strawman instance typechecks:

instance Foldable ((,,) a b) where
  length _ = 42

I assume this should violate some law, but the relevant law seems to
be forgotten.

The most constraining language I can find is the following:

> sum, product, maximum, and minimum should all be essentially equivalent to foldMap forms, such as
> sum = getSum . foldMap Sum
> but may be less defined.

but (a) `length` is not even mentioned, even if it's intended (b) I
think those should be laws (c) using "should" and "essentially" in
"should all be essentially equivalent", seems too weak. I can infer
the intention, but this seems insufficient to declare

Docs for `length` don't help either:

> Returns the size/length of a finite structure as an Int. The default implementation is optimized for structures that are similar to cons-lists, because there is no general way to do better.

I mean, these docs use the English word "length", so that actually
forbids 42, but that text is too vague to forbid 3 frankly. As I
missing something?

I also take issue with "may be less defined", and here I'm not sure of
the intention, since that declares

instance Foldable ((,,) a b) where
  length _ = undefined

as legal. I imagine the point is about taking the length of partially
undefined structures, but it's not clear to me why a custom `sum`
implementation would be less defined than `sum = getSum . foldMap
Sum`.

Even ignoring the above instances (which I would never write down), I
can't reason much about my code based on those specifications. This
situation seems unfortunate.

Cheers,
--
Paolo G. Giarrusso - Ph.D. Student, Tübingen University
http://ps.informatik.uni-tuebingen.de/team/giarrusso/