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?

  • $\begingroup$ 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. $\endgroup$
    – Ilk
    Jan 15, 2023 at 1:37
  • $\begingroup$ 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. $\endgroup$
    – Ian
    Apr 5, 2023 at 0:01


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.