Constraints on definition of `length` should be strengthened

[Ben Franksen]

Am 09.04.2017 um 01:51 schrieb Nathan Bouscal:
> - You're trying to establish an analogy between these tuple instances and
> non-law-abiding instances, but that analogy really doesn't work. These are
> the only law-abiding instances that the types can possibly have. When I
> claim something is a Monad, I'm saying that if the compiler knew how to
> take a proof, I'd be able to provide one. When you claim tuples are unbiased,

I do not claim tuples *are* unbiased. I have been (espressly) talking
about intent. A programming language is a tool designed by humans, not
an artefact of nature. Whatever tuples are, factually, is not important.
The only important thing is what we *want* them to be. Of course we want
our intents to be consistent, but I don't see how ignoring the
(unavoidable) bias violates consistency.

> there is no analogous statement. You can't say that you'd be able
> to provide a proof that tuples are unbiased, because they *aren't* unbiased.

You can't prove that instances of Monad adhere to the Monad laws, in
general. But you can (informally) express your intent that instances
*should* adhere to the laws.

Yes, for a single concrete instance you can provide proof that the laws
are fulfilled. And for a single concrete program (or library, or module,
or function) that uses tuples I can prove that it does not depend on the
(existing, but not intended) bias for tuples.

> - A lot of these arguments are taking the form "let's have unbiased
> tuples", but the actual impact of just removing the instances wouldn't be
> unbiased tuples,

Again, you argue as if we were talking about a mechanical system. The
"impact" in this case depends on people's behavior and expectations. We
are talking about *designing* library infrastructure.

> it would be a crippled biased tuple. Getting rid of the
> instances wouldn't make tuples any less biased, it would just take away
> useful functionality.

And this is where we differ: IMO it would take away functionality that
is confusing and ill-termed. The desired functionality is not bad perse,
but would be much better provided by dedicated data types that clearly
express the intent of using the bias induces by currying and left to
right order of type arguments. The tuples with reduced functionality
would be more useful, not less, because one could rely on them not
acting in strange and unexpected ways. See the many examples that people
provided for refactoring code that uses tuples and where the type error
was the intended and expected behavior and the "functionality" provided
by Foldable instances was in fact dysfunctional.

Cheers
Ben