# List Functions That Don't Depend on Length

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?

• This seems like parametric quantifiers; notably the parametric quantification on Size; instead of normal natural numbers in publications.lib.chalmers.se/records/fulltext/252073/… ; a difference would be that while in parametric quantifiers Size and naturals are distinct with different relational structure, it seems like here you would like to consider single type with 2 different relational structures depending on use; modality.
– Ilk
Jan 15 at 1:37
• The criterion of not inspecting the length of the list: What kind of problem will that solve for you? That might provide some useful inspiration.
– Ian
Apr 5 at 0:01