Constraints on definition of `length` should be strengthened

[Vladislav Zavialov]

On Tue, Apr 4, 2017 at 11:33 AM, Henrik Nilsson
<Henrik.Nilsson at nottingham.ac.uk> wrote:
>
> For the sake of argument, suppose some mechanism were adopted to
> mitigate the bias implied by the (inevitable) ordering of arguments
> to to type constructors. For tuples, we might imagine some kind
> of notation inspired by operator sections as a first step, making the
> following instance declaration possible:
>
>     instance Functor (,b) where
>         ...
>
> Would tuples then still be biased in the above sense, and if
> so why?
>

No, tuples wouldn't be biased if (a,) and (,b) could behave the same,
i.e. 'f x' could be instantiated as both '(a,x)' and '(x,b)'. However,
what you propose is not possible in Haskell and the extension is not
straightforward.

(1) Writing (,b) would require type-level lambda functions, as it's
equivalent to writing '\a -> (a,b)'. Type-level lambdas are not
straightforward at all: they conflict with the matchability
(injectivity+generativity) assumption about type constructors -
currently 'f a ~ g b' implies 'f ~ g' and 'a ~ b' - which is not true
for arbitrary type-level functions. Removing this rule would wreak
havoc on type inference. The solution seems to be to have two kinds of
type-level arrows, as described in Richard Eisenberg's thesis on
Dependent Haskell.

(2) Even if type-level functions are added to the language, it's very
likely that they will be disallowed as class parameters. Notice that
classes perform pattern matching on types, and pattern matching on
functions is impossible. So even if one could write '\a -> (a,b),
writing Functor (\a -> (a,b)) would remain impossible.

(3) Assume that somehow we managed to solve those problems. What
instance do you define, Functor (a,) or Functor (,b)? Perhaps neither?
Or maybe Functor (\a -> (a,a)) to map over both arguments? Hard design
questions, many opinions will emerge! Do those instances even overlap?
- determining this requires the compiler to reason about function
equalities.

All in all, I see only two sensible ways to proceed: accept that
tuples are biased, or make them unbiased by changing their kind from
Type -> Type -> Type to something uncurried.