Intuitively, a polymorphic function of type $f : \forall a. [a] \to [a]$ cannot inspect the type of its elements. This intuition can be captured formally using either natural transformations or relational parametricity.
However, $f$ can inspect the length of its input list. For example $f$ could act as the identity on lists with even lengths and reverse lists with odd lengths.
Is there a mathematical condition that captures the class of functions which do not inspect the lengths of their inputs? I would expect this class to include the identity function, the reverse function, the function which concatenates a list to itself (e.g. "hello" $\mapsto$ "hellohello"), and the function which duplicates each element in a list (e.g. "hello" $\mapsto$ "hheelllloo").
The issue with the usual naturality/parametricity conditions are that they only relate lists of the same length. I thought maybe we could consider partial functions instead of total functions, where a partial function $t : a \to b$ lifts to a function $t^* : [a] \to [b]$ by element-wise application and dropping any elements where $t$ is undefined. However even if this works, this seems rather ad-hoc.
I'm not super familiar with dependent types, but it seems like a better motivated approach might be to consider a type such as $f : \forall n\ a. \text{Vec}\ n\ a \to [a]$. However, even with this type the outputs of $f$ are only related if they have the same length, so I don't think this quite works. I have two questions: 1) is there a polymorphic type involving vectors which captures the class of functions which don't inspect the lengths? 2) does the parametricity/naturality condition arising from this type relate to the partial function approach in any way?
