<p>I think I found a solution to my problem.
But it is a bit unfair to previous answers, because they were lacking context.</p>
<p>Specifically, I knew how <code>fun</code> is implemented. For my idea to work, it is important to know that <code>fun f</code> can only call <code>f</code> a finite number of times, and that we can enumerate all the call sites.</p>
<p>In my specific case, there was just a single call <span class="math-container">$f(\mathit{pre})$</span> (where <span class="math-container">$f$</span> is the semantic function corresponding to <code>f</code>) inside the implementation of <code>fun</code> with a special <span class="math-container">$pre : D$</span> that is <em>not</em> parametric (note that the implementation of <code>fun</code> knows how <span class="math-container">$D$</span> is defined and can do all kinds of shenanigans).</p>
<p>Now I can instantiate the abstraction theorem from the Q as follows:</p>
<p><span class="math-container">$$\begin{array}{c}
  A \triangleq B := D, \qquad \mathit{inst_1} := \mathit{inst_2} := \mathit{inst}, \qquad d_1 := a, \qquad d_2 := \mathit{pre} \\
  R_{a}(d_1,d_2) := \forall g.\ d_1 = g(a) \land d_2 = g(\mathit{pre}) \implies g(a) ⊑ \mathit{apply}(\mathit{fun}(g),a)  \\
\end{array}$$</span></p>
<p>FWIW, <span class="math-container">$R_{a}$</span> can be further simplified once <span class="math-container">$\mathit{fun}$</span> is inlined; then the strange quantification over <span class="math-container">$g$</span> vanishes and I get <span class="math-container">$R_{a}(d_1,d_2) = d_1 \sqsubseteq \mathit{apply}(\mathit{abs}(d_2),a)$</span> for some <span class="math-container">$\mathit{abs}$</span> with the property <span class="math-container">$\mathit{fun}(f) = \mathit{abs}(f(\mathit{pre}))$</span>.</p>
<p>Instantiating the abstraction theorem and simplifying it a bit yields</p>
<p><span class="math-container">$$\begin{array}{l}
a ⊑ \mathit{apply}(\mathit{fun}(\mathit{id}),a) \land (\mathit{inst}, \mathit{inst}) ∈ \mathsf{Dict}(R_{a}) \implies \\
  f_D(\mathit{inst})(a) ⊑ \mathit{apply}(\mathit{fun}(f_D(\mathit{inst})),a)
\end{array}$$</span></p>
<p>And I could successfully prove the premises to show the desired property.</p>
<hr />
<p>This approach can be generalised to implementations of <code>fun</code> that call <code>f</code> more than once, simply anticipating all potential arguments <span class="math-container">$\mathit{pre}_1, ... \mathit{pre}_n$</span> and then generalising <span class="math-container">$R$</span> to type <span class="math-container">$D \times D^n$</span>.</p>
<hr />
<p>Perhaps someone has an idea to make this simpler?</p>

CC BY-SA 4.0
2024-06-26T12:01:43.563Z
That's a strange R because d2 is not used in the conclusion, and d1 can also be rid of by substitution, that's just "for all f, f a ⊑ app (fun f) a". And if you have that, you don't need parametricity since you can apply that property directly to f.
Li-yao Xia
CC BY-SA 4.0
2024-06-26T12:07:41.413Z
I think the premises are important because it enlarges R. Proof: I don't think your substitution rewrite is reversible in general. That's important because otherwise it's exactly what you say: "If you have that, you don't need parametricity".
Sebastian Graf
CC BY-SA 4.0
2024-06-26T12:09:53.350Z
The premise filters out fs that I cannot do the proof for. R says that "any f is fine, as long as it coincides with all the points I specify", because that gives me enough leverage to prove the inequality.
Sebastian Graf
CC BY-SA 4.0
2024-06-27T16:55:38.730Z
I updated a bit and used the more familiar style from Wadler to derive the free theorem. Still same $R$, but I explain a bit how it simplifies once `fun` inlines.
Sebastian Graf
CC BY-SA 4.0
2024-06-27T21:00:12.203Z
Does your solution still require some knowledge about the structure of all possible terms of type `Dict d -> d -> d`? That's what it looks like to me. In my answer, I derived the structure of all possible terms of a simpler type. Perhaps you need to generalize that technique to a more complicated type where both `fun` and `apply` from `inst` are used.
winitzki
CC BY-SA 4.0
2024-06-28T12:51:49.183Z
I'm not sure I understand your question. Of course I require "knowledge about the structure of all possible terms of type Dict d -> d -> d", that's exactly the knowledge provided by parametricity! Perhaps I should have said so, but without appealing to parametricity, I cannot prove the property `f a <= apply (fun f) a`; I can find a counter-example for `f`. Crucially, this counter-example is not parametric, that is, not definable at type `forall d. Dict d -> d -> d`!
Sebastian Graf
CC BY-SA 4.0
2024-06-26T10:17:50.017Z
2024-06-27T16:53:33.180Z
2024-06-27T16:53:33.180Z
Sebastian Graf
<blockquote>
<p><code>f(a) ⊑ inst.apply(inst.fun(f),a)</code></p>
</blockquote>
<p>Unless I'm misunderstanding something, that's not a property that holds for all functions <code>f</code> of that type.</p>
<p>Counterexample:</p>
<ul>
<li><code>f = \inst x -&gt; inst.fun (\_ -&gt; x)</code></li>
<li><code>D = Bool</code> with the discrete order (<code>x ⊑ y</code> iff <code>x == y</code>)</li>
<li><code>inst.fun = \_ -&gt; False</code></li>
<li><code>inst.apply = \_ _ -&gt; True</code>.</li>
</ul>

CC BY-SA 4.0
2024-06-26T09:30:20.320Z
Right, I said "fixed, but arbitrary set D with the partial order (⊑)⊆D×D,", and that's actually wrong. $D$, the ordering and the dictionary is fixed, but not arbitrary.
The property of interest definitely holds (I can prove it without parametricity). It seems I just need to state it properly.
Sebastian Graf
CC BY-SA 4.0
2024-06-26T09:34:07.453Z
I updated the question. I don't really want to detail how $D$ and $⊑$ is defined; but parametricity should not need that either.
Sebastian Graf
CC BY-SA 4.0
2024-06-26T08:19:55.873Z
2024-06-26T08:19:55.873Z
Li-yao Xia
<p>Let me reformulate your question via code.</p>
<p>You want to obtain some parametricity property for functions of this type:   <span class="math-container">$$   \forall d.~ (\textrm{Dict}~ d) \to d \to d $$</span></p>
<p>Since you are only interested in using the <code>fun</code> property of <code>Dict</code>, let me drop other properties of <code>Dict</code> and define a simpler type <span class="math-container">$U$</span> as:</p>
<p><span class="math-container">$$ U = \forall d.~ ((d \to d) \to d) \to  d \to d  $$</span></p>
<p>Note a similar question posted here: <a href="https://cstheory.stackexchange.com/questions/53855">Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?</a> where the type was <span class="math-container">$$T = \forall a.~((a\to a)\to a)\to a$$</span> The type <span class="math-container">$U$</span> differs slightly from the type <span class="math-container">$T$</span> in that question. My answer to that question can be suitably modified to show that <span class="math-container">$U$</span> is equivalent to the following type:</p>
<p><span class="math-container">$$ U \cong \forall r. \mu b. \mathbb1 + r + (r \to b) $$</span></p>
<p>and to derive an explicit form of type <span class="math-container">$U$</span>:</p>
<p><span class="math-container">$$ U \cong  (\mathbb1 + \mathbb1) + (\mathbb1 + \mathbb2) + (\mathbb1 + \mathbb3) + ...$$</span></p>
<p>Values of this type are pairs of integers <span class="math-container">$m, n$</span> where <span class="math-container">$m \geq n + 1$</span> and <span class="math-container">$n \geq 0$</span>.</p>
<p>I omit the details of the derivation. Please look through the detailed proof shown in my answer to the question linked above.</p>
<p>A term corresponding to each alternative of this union type can be written explicitly. The general form of terms of type <span class="math-container">$U = \forall d. ~((d\to d)\to d)\to d \to d$</span> can be written as one of <span class="math-container">$u_{m,n}$</span> (with <span class="math-container">$m\geq n\geq 1$</span>) or <span class="math-container">$u_m$</span> (with <span class="math-container">$m\geq 1$</span>) or <span class="math-container">$u_0$</span>:</p>
<p><span class="math-container">$$ u_{m,n} = \lambda p^{~: (d\to d)\to d}.\,\lambda q^ {~: d}.~  p(\lambda r_1.\,p(\lambda r_2.\,...\,p(\lambda r_m.\,r_n)...) $$</span></p>
<p><span class="math-container">$$ u_m = \lambda p^{~: (d\to d)\to d}.\,\lambda q^{ ~: d}.~  p(\lambda r_1.\,p(\lambda r_2.\,...\,p(\lambda r_m.\,q)...) $$</span></p>
<p><span class="math-container">$$ u_0 = \lambda p^{~: (d\to d)\to d}.\,\lambda q^{ ~: d}.~  q $$</span></p>
<p>Parametricity assures that there are no other terms of type <span class="math-container">$U$</span>.</p>

CC BY-SA 4.0
2024-06-26T09:36:19.380Z
But I'm also using $\mathit{apply} : d \to d \to d$, so it's more like $U=∀d. ((d→d)→d)→(d→d→d)→d→d$, a very different type. Plus, other operations in $d$ really use methods like $\mathit{stuff}$, so I want to know how to prove them correct as well
Sebastian Graf
CC BY-SA 4.0
2024-06-26T11:29:34.233Z
@SebastianGraf Indeed that would be a very different type, much more complicated. In any case, I was just trying to translate your question into a language that is close to programming. The way you formulate your question, I can't make any sense of it. Where does your notation come from, what book or paper? For example, I have no idea what  ⟦ ⊦  ⟧$~_$( $$;$$) means, as I have never seen such notation before.
winitzki
CC BY-SA 4.0
2024-06-26T12:00:12.647Z
Oh, I thought that notation would be standard, apologies. It's from https://www.sciencedirect.com/science/article/pii/S157106611500078X?ref=pdf_download&fr=RR-2&rr=899d0885af262c10.
Sebastian Graf
CC BY-SA 4.0
2024-06-27T16:42:34.610Z
FWIW, I rewrote the Q so that it uses the more familiar and scrutible, but slightly informal notation from Wadler.
Sebastian Graf
CC BY-SA 4.0
2024-06-26T09:01:14.663Z
2024-06-26T09:01:14.663Z
winitzki
<p>Say I have the following dictionary of abstract operations, written in Haskell for relatively concise notation:</p>
<pre><code>data Dict d = MkDict
  { fun   :: (d -&gt; d) -&gt; d
  , apply :: d -&gt; d -&gt; d
  , stuff :: (d -&gt; d -&gt; d) -&gt; d -&gt; d }
</code></pre>
<p>Now I want to exploit parametricity at a Haskell function <code>f :: forall d. Dict d -&gt; d -&gt; d</code>. In the semi-formal style of Wadler, the abstraction theorem gives me:</p>
<p><span class="math-container">$$
  (f, f) ∈ \forall \mathcal{X}.\ \mathsf{Dict(\mathcal{X})} \to \mathcal{X} \to \mathcal{X}
$$</span></p>
<p>(where the type formers here are interpreted relationally.)
The relational interpretation of this fact amounts to</p>
<p><span class="math-container">\begin{align*}
  &amp;\forall A, B.\
  \forall R ⊆ A \times B.\
  \forall (\mathit{inst_1}, \mathit{inst_2}) ∈ \mathsf{Dict(R)}.\
  \forall (d_1,d_2) ∈ R.\\
  &amp;(f_A(\mathit{inst_1})(d_1), f_B(\mathit{inst_2})(d_2)) ∈ R
\end{align*}</span></p>
<p>My goal is to instantiate this theorem so that I can prove a property about a concrete, fixed implementation of <span class="math-container">$\mathit{inst} : \mathsf{Dict}(D)$</span> for some fixed <span class="math-container">$D$</span>, on which I also define a partial order <span class="math-container">$(\sqsubseteq) \subseteq D \times D$</span>.
The property in question is</p>
<p><span class="math-container">$$
  \forall (f:\forall X.\ \mathsf{Dict(\mathit{X})} \to X \to X)\ (a:D)\ldotp f_D(\mathit{inst})(a) \sqsubseteq \mathit{inst.\!apply}(\mathit{inst.\!fun}(f_D(\mathit{inst}))(a)
$$</span></p>
<p>How do I formulate for this property of functions <span class="math-container">$D \to D$</span> a matching relation <span class="math-container">$R \subseteq D \times D$</span>, so that it instantiates the abstraction theorem to show the property?</p>

<type-theory><functional-programming><parametricity>
Can parametricity be applied to show a property of function values?
Sebastian Graf
# Can parametricity be applied to show a property of function values?

(Asked by: username_0 on 2024-06-25)

Say I have the following dictionary of abstract operations, written in Haskell for relatively concise notation:
data Dict d = MkDict
  { fun   :: (d -> d) -> d
  , apply :: d -> d -> d
  , stuff :: (d -> d -> d) -> d -> d }

Now I want to exploit parametricity at a Haskell function f :: forall d. Dict d -> d -> d. In the semi-formal style of Wadler, the abstraction theorem gives me:
$$
  (f, f) ∈ \forall \mathcal{X}.\ \mathsf{Dict(\mathcal{X})} \to \mathcal{X} \to \mathcal{X}
$$
(where the type formers here are interpreted relationally.)
The relational interpretation of this fact amounts to
\begin{align*}
  &\forall A, B.\
  \forall R ⊆ A \times B.\
  \forall (\mathit{inst_1}, \mathit{inst_2}) ∈ \mathsf{Dict(R)}.\
  \forall (d_1,d_2) ∈ R.\\
  &(f_A(\mathit{inst_1})(d_1), f_B(\mathit{inst_2})(d_2)) ∈ R
\end{align*}
My goal is to instantiate this theorem so that I can prove a property about a concrete, fixed implementation of $\mathit{inst} : \mathsf{Dict}(D)$ for some fixed $D$, on which I also define a partial order $(\sqsubseteq) \subseteq D \times D$.
The property in question is
$$
  \forall (f:\forall X.\ \mathsf{Dict(\mathit{X})} \to X \to X)\ (a:D)\ldotp f_D(\mathit{inst})(a) \sqsubseteq \mathit{inst.\!apply}(\mathit{inst.\!fun}(f_D(\mathit{inst}))(a)
$$
How do I formulate for this property of functions $D \to D$ a matching relation $R \subseteq D \times D$, so that it instantiates the abstraction theorem to show the property?

**Tags:** type-theory, functional-programming, parametricity

---

## 3 answers

### Answer by username_0 on 2024-06-26. Score: 0 | Accepted answer

I think I found a solution to my problem.
But it is a bit unfair to previous answers, because they were lacking context.

Specifically, I knew how `fun` is implemented. For my idea to work, it is important to know that `fun f` can only call `f` a finite number of times, and that we can enumerate all the call sites.

In my specific case, there was just a single call $f(\mathit{pre})$ (where $f$ is the semantic function corresponding to `f`) inside the implementation of `fun` with a special $pre : D$ that is *not* parametric (note that the implementation of `fun` knows how $D$ is defined and can do all kinds of shenanigans).

Now I can instantiate the abstraction theorem from the Q as follows:

$$\begin{array}{c}
A \triangleq B := D, \qquad \mathit{inst\_1} := \mathit{inst\_2} := \mathit{inst}, \qquad d\_1 := a, \qquad d\_2 := \mathit{pre} \\
R\_{a}(d\_1,d\_2) := \forall g.\ d\_1 = g(a) \land d\_2 = g(\mathit{pre}) \implies g(a) ⊑ \mathit{apply}(\mathit{fun}(g),a) \\
\end{array}$$

FWIW, $R\_{a}$ can be further simplified once $\mathit{fun}$ is inlined; then the strange quantification over $g$ vanishes and I get $R\_{a}(d\_1,d\_2) = d\_1 \sqsubseteq \mathit{apply}(\mathit{abs}(d\_2),a)$ for some $\mathit{abs}$ with the property $\mathit{fun}(f) = \mathit{abs}(f(\mathit{pre}))$.

Instantiating the abstraction theorem and simplifying it a bit yields

$$\begin{array}{l}
a ⊑ \mathit{apply}(\mathit{fun}(\mathit{id}),a) \land (\mathit{inst}, \mathit{inst}) ∈ \mathsf{Dict}(R\_{a}) \implies \\
f\_D(\mathit{inst})(a) ⊑ \mathit{apply}(\mathit{fun}(f\_D(\mathit{inst})),a)
\end{array}$$

And I could successfully prove the premises to show the desired property.

---

This approach can be generalised to implementations of `fun` that call `f` more than once, simply anticipating all potential arguments $\mathit{pre}\_1, ... \mathit{pre}\_n$ and then generalising $R$ to type $D \times D^n$.

---

Perhaps someone has an idea to make this simpler?

> **Comments:**
> **username_1**: That's a strange R because d2 is not used in the conclusion, and d1 can also be rid of by substitution, that's just "for all f, f a ⊑ app (fun f) a". And if you have that, you don't need parametricity since you can apply that property directly to f.  
> **username_0**: I think the premises are important because it enlarges R. Proof: I don't think your substitution rewrite is reversible in general. That's important because otherwise it's exactly what you say: "If you have that, you don't need parametricity".  
> **username_0**: The premise filters out fs that I cannot do the proof for. R says that "any f is fine, as long as it coincides with all the points I specify", because that gives me enough leverage to prove the inequality.  
> **username_0**: I updated a bit and used the more familiar style from Wadler to derive the free theorem. Still same $R$, but I explain a bit how it simplifies once `fun` inlines.  
> **username_2**: Does your solution still require some knowledge about the structure of all possible terms of type `Dict d -> d -> d`? That's what it looks like to me. In my answer, I derived the structure of all possible terms of a simpler type. Perhaps you need to generalize that technique to a more complicated type where both `fun` and `apply` from `inst` are used.  
> **username_0**: I'm not sure I understand your question. Of course I require "knowledge about the structure of all possible terms of type Dict d -> d -> d", that's exactly the knowledge provided by parametricity! Perhaps I should have said so, but without appealing to parametricity, I cannot prove the property `f a <= apply (fun f) a`; I can find a counter-example for `f`. Crucially, this counter-example is not parametric, that is, not definable at type `forall d. Dict d -> d -> d`!  

---

### Answer by username_1 on 2024-06-26. Score: 2

> `f(a) ⊑ inst.apply(inst.fun(f),a)`

Unless I'm misunderstanding something, that's not a property that holds for all functions `f` of that type.

Counterexample:

* `f = \inst x -> inst.fun (\_ -> x)`
* `D = Bool` with the discrete order (`x ⊑ y` iff `x == y`)
* `inst.fun = \_ -> False`
* `inst.apply = \_ _ -> True`.

> **Comments:**
> **username_0**: Right, I said "fixed, but arbitrary set D with the partial order (⊑)⊆D×D,", and that's actually wrong. $D$, the ordering and the dictionary is fixed, but not arbitrary. The property of interest definitely holds (I can prove it without parametricity). It seems I just need to state it properly.  
> **username_0**: I updated the question. I don't really want to detail how $D$ and $⊑$ is defined; but parametricity should not need that either.  

---

### Answer by username_2 on 2024-06-26. Score: 0

Let me reformulate your question via code.

You want to obtain some parametricity property for functions of this type: $$ \forall d.~ (\textrm{Dict}~ d) \to d \to d $$

Since you are only interested in using the `fun` property of `Dict`, let me drop other properties of `Dict` and define a simpler type $U$ as:

$$ U = \forall d.~ ((d \to d) \to d) \to d \to d $$

Note a similar question posted here: [Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?](https://cstheory.stackexchange.com/questions/53855) where the type was $$T = \forall a.~((a\to a)\to a)\to a$$ The type $U$ differs slightly from the type $T$ in that question. My answer to that question can be suitably modified to show that $U$ is equivalent to the following type:

$$ U \cong \forall r. \mu b. \mathbb1 + r + (r \to b) $$

and to derive an explicit form of type $U$:

$$ U \cong (\mathbb1 + \mathbb1) + (\mathbb1 + \mathbb2) + (\mathbb1 + \mathbb3) + ...$$

Values of this type are pairs of integers $m, n$ where $m \geq n + 1$ and $n \geq 0$.

I omit the details of the derivation. Please look through the detailed proof shown in my answer to the question linked above.

A term corresponding to each alternative of this union type can be written explicitly. The general form of terms of type $U = \forall d. ~((d\to d)\to d)\to d \to d$ can be written as one of $u\_{m,n}$ (with $m\geq n\geq 1$) or $u\_m$ (with $m\geq 1$) or $u\_0$:

$$ u\_{m,n} = \lambda p^{~: (d\to d)\to d}.\,\lambda q^ {~: d}.~ p(\lambda r\_1.\,p(\lambda r\_2.\,...\,p(\lambda r\_m.\,r\_n)...) $$

$$ u\_m = \lambda p^{~: (d\to d)\to d}.\,\lambda q^{ ~: d}.~ p(\lambda r\_1.\,p(\lambda r\_2.\,...\,p(\lambda r\_m.\,q)...) $$

$$ u\_0 = \lambda p^{~: (d\to d)\to d}.\,\lambda q^{ ~: d}.~ q $$

Parametricity assures that there are no other terms of type $U$.

> **Comments:**
> **username_0**: But I'm also using $\mathit{apply} : d \to d \to d$, so it's more like $U=∀d. ((d→d)→d)→(d→d→d)→d→d$, a very different type. Plus, other operations in $d$ really use methods like $\mathit{stuff}$, so I want to know how to prove them correct as well  
> **username_2**: @SebastianGraf Indeed that would be a very different type, much more complicated. In any case, I was just trying to translate your question into a language that is close to programming. The way you formulate your question, I can't make any sense of it. Where does your notation come from, what book or paper? For example, I have no idea what  ⟦ ⊦  ⟧$~_$( $$;$$) means, as I have never seen such notation before.  
> **username_0**: Oh, I thought that notation would be standard, apologies. It's from https://www.sciencedirect.com/science/article/pii/S157106611500078X?ref=pdf_download&fr=RR-2&rr=899d0885af262c10.  
> **username_0**: FWIW, I rewrote the Q so that it uses the more familiar and scrutible, but slightly informal notation from Wadler.  

---

