<p>Intuitively, a polymorphic function of type <span class="math-container">$f : \forall a. [a] \to [a]$</span> cannot inspect the type of its elements. This intuition can be captured formally using either natural transformations or relational parametricity.</p>
<p>However, <span class="math-container">$f$</span> <em>can</em> inspect the length of its input list. For example <span class="math-container">$f$</span> could act as the identity on lists with even lengths and reverse lists with odd lengths.</p>
<p>Is there a mathematical condition that captures the class of functions which <em>do not</em> 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. &quot;hello&quot; <span class="math-container">$\mapsto$</span> &quot;hellohello&quot;), and the function which duplicates each element in a list (e.g. &quot;hello&quot; <span class="math-container">$\mapsto$</span> &quot;hheelllloo&quot;).</p>
<p>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 <span class="math-container">$t : a \to b$</span> lifts to a function <span class="math-container">$t^* : [a] \to [b]$</span> by element-wise application and dropping any elements where <span class="math-container">$t$</span> is undefined. However even if this works, this seems rather ad-hoc.</p>
<p>I'm not super familiar with dependent types, but it seems like a better motivated approach might be to consider a type such as <span class="math-container">$f : \forall n\ a. \text{Vec}\ n\ a \to [a]$</span>. However, even with this type the outputs of <span class="math-container">$f$</span> 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?</p>

CC BY-SA 4.0
2023-04-05T00:01:09.430Z
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.
Beth
CC BY-SA 4.0
2023-01-15T01:37:31.360Z
This seems like parametric quantifiers; notably the parametric quantification on Size; instead of normal natural numbers in  https://publications.lib.chalmers.se/records/fulltext/252073/local_252073.pdf ; 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
<type-theory><pl.programming-languages><ct.category-theory><parametricity><logical-relations>
List Functions That Don't Depend on Length
vigenary
# List Functions That Don't Depend on Length

(Asked by: username_0 on 2023-01-14)

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?

**Tags:** type-theory, pl.programming-languages, ct.category-theory, parametricity, logical-relations
> **Comments:**
> **username_2**: This seems like parametric quantifiers; notably the parametric quantification on Size; instead of normal natural numbers in  https://publications.lib.chalmers.se/records/fulltext/252073/local_252073.pdf ; 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.  
> **username_1**: 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.  

---

## 0 answers

