<p><span class="math-container">$\newcommand{\Alg}{\mathsf{Alg}\ }$</span>
<span class="math-container">$\newcommand{\NatF}{\mathsf{NatF}\ }$</span>
<span class="math-container">$\newcommand{\Nat}{\mathsf{Nat}}$</span>
<span class="math-container">$\newcommand{\map}{\mathrm{map}\ }$</span>
<span class="math-container">$\newcommand{\Z}{\mathrm{Z}}$</span>
<span class="math-container">$\newcommand{\S}{\mathrm{S}}$</span></p>
<p>I don't think this is an actual counter-example.</p>
<p>Parametricity implies:</p>
<p><span class="math-container">$$∀(α : \Alg \NatF t) (g : r → t)(x : \NatF r). \\
α\ [r]\ g\ x = α\ [t]\ (λx.x)\ (\map g\ x)
$$</span></p>
<p>(a special case of the free theorem), where
<span class="math-container">$$\map g\ x = Λt. λz\ s. x\ [t]\ z\ (s \circ h)$$</span></p>
<p>let:</p>
<p><span class="math-container">$$h : (∀s. s → s) → t \\
h\ \_ = α\ [t]\ (λy. y)\ (Λt. λz\ s. z)$$</span></p>
<p>which is your first argument to <span class="math-container">$α$</span>. Then in your example:</p>
<p><span class="math-container">$$α\ [∀s. s→s]\ h\ x \\
= α\ [t]\ (λx.x)\ (\map h\ x) \\
= α\ [t]\ (λx.x)\ (Λt. λ\_\ s. s (α\ [t]\ (λx. x)\ (Λt. λz\ \_. z)))$$</span></p>
<p>Now observe the following from <span class="math-container">$\Z$</span> and <span class="math-container">$\S$</span></p>
<p><span class="math-container">$$
α\ [\Nat]\ (λy. y\ [t]\ α)\ (Λt. λz\ \_. z)  \\
  = α\ [t]\ (λx.x)\ (\map (λy. y\ [t]\ α) (Λt. λz\ \_. z)) \\
  = α\ [t]\ (λx.x)\ (Λt. λz\ \_. z)
$$</span></p>
<p><span class="math-container">$$
α\ [\Nat]\ (λy. y\ [t]\ α)\ (Λt. λ\_\ s. s\ n) \\
 = α\ [t]\ (λx.x)\ (map (λy. y\ [t]\ α) (Λt. λ\_\ s. s n)) \\
 = α\ [t]\ (λx.x)\ (Λt. λ\_\ s. s (n\ [t]\ α))
$$</span></p>
<p>Then, if we go back to the calculation from your example:</p>
<p><span class="math-container">$$
α\ [t]\ (λx.x)\ (Λt. λ\_ s. s (α\ [t]\ (λx.x)\ (Λt. λz\ \_. z))) \\
  = α\ [t]\ (λx.x)\ (Λt. λ\_\ s. s (\Z\ [t]\ α)) \\
  = \S\ \Z\ [t]\ α
$$</span></p>
<p>So your example is extensionally equal to <span class="math-container">$1$</span>, assuming my calculations are correct.</p>

CC BY-SA 4.0
2021-03-02T09:06:55.117Z
Thanks Dan! I just tried it and I think you are completely right, wrong behaves exactly like 1. This really shows the difficulties of lambda encodings and extensionality! I have more confidence that the Mendler encoding is adequate now, I think the (r -> t) function makes sure it's adequate, because if we take the Scott-encoding: Fix f = forall t. (forall r. f r -> t) -> t (which is just the encoding of a (weak) existential type) then you can definitely make invalid terms, because you are completely free to chose the r.
Labbekak
CC BY-SA 4.0
2021-03-02T16:14:20.557Z
I suspect you can use parametricity to prove adequacy relative to the Church encoding, because the Mendler Alg should be isomorphic to the Church Alg `f t -> t` for functors `f`. Essentially $(∃r. (r →t)×f\ r) \cong f\ t$ because of the co-Yoneda lemma.
Dan Doel
CC BY-SA 4.0
2021-03-02T03:38:17.963Z
2021-03-02T03:38:17.963Z
Dan Doel
<p>In the paper <a href="https://homepage.cs.uiowa.edu/%7Eastump/papers/stump-fu-jfp-2016.pdf" rel="noreferrer">&quot;Efficiency of Lambda-Encodings in Total Type Theory&quot;</a> it is mentioned that the Church-encoding is adequate and the Parigot encoding is not adequate. This means that any inhabitant of an encoded datatype actually represents an element of the datatype.</p>
<p>My question is if the Mendler-style encoding is adequate. I think I found a counter example (in System F):</p>
<pre><code>-- Mendler-style encoding
Alg f t = forall r. (r -&gt; t) -&gt; f r -&gt; t
Fix f = forall t. Alg f t -&gt; t

-- Natural numbers
NatF r = forall t. t -&gt; (r -&gt; t) -&gt; t
Nat = Fix Nat

-- the valid constructors for natural numbers
Z : Nat = /\t. \alg. alg [Nat] (\y. y [t] alg) (/\t. \z s. z)
S : Nat -&gt; Nat = \n. /\t. \alg. alg [Nat] (\y. y [t] alg) (/\t. \z s. s n)

-- An inhabitant of Nat that is not a valid natural number
wrong : Nat =
  /\t. \alg.
    alg [forall t. t -&gt; t]
    (\x. alg [t] (\y. y) (/\t. \z s. z))
    (/\t. \z s. s (/\t. \x. x))
</code></pre>

<type-systems><typed-lambda-calculus><encoding>
Is the Mendler-encoding in System-F adequate?
Labbekak
# Is the Mendler-encoding in System-F adequate?

(Asked by: username_0 on 2021-03-01)

In the paper "Efficiency of Lambda-Encodings in Total Type Theory" it is mentioned that the Church-encoding is adequate and the Parigot encoding is not adequate. This means that any inhabitant of an encoded datatype actually represents an element of the datatype.
My question is if the Mendler-style encoding is adequate. I think I found a counter example (in System F):
-- Mendler-style encoding
Alg f t = forall r. (r -> t) -> f r -> t
Fix f = forall t. Alg f t -> t

-- Natural numbers
NatF r = forall t. t -> (r -> t) -> t
Nat = Fix Nat

-- the valid constructors for natural numbers
Z : Nat = /\t. \alg. alg [Nat] (\y. y [t] alg) (/\t. \z s. z)
S : Nat -> Nat = \n. /\t. \alg. alg [Nat] (\y. y [t] alg) (/\t. \z s. s n)

-- An inhabitant of Nat that is not a valid natural number
wrong : Nat =
  /\t. \alg.
    alg [forall t. t -> t]
    (\x. alg [t] (\y. y) (/\t. \z s. z))
    (/\t. \z s. s (/\t. \x. x))

**Tags:** type-systems, typed-lambda-calculus, encoding


---

## 1 answers

### Answer by username_1 on 2021-03-02. Score: 4 | Accepted answer

$\newcommand{\Alg}{\mathsf{Alg}\ }$
$\newcommand{\NatF}{\mathsf{NatF}\ }$
$\newcommand{\Nat}{\mathsf{Nat}}$
$\newcommand{\map}{\mathrm{map}\ }$
$\newcommand{\Z}{\mathrm{Z}}$
$\newcommand{\S}{\mathrm{S}}$

I don't think this is an actual counter-example.

Parametricity implies:

$$∀(α : \Alg \NatF t) (g : r → t)(x : \NatF r). \\
α\ [r]\ g\ x = α\ [t]\ (λx.x)\ (\map g\ x)
$$

(a special case of the free theorem), where
$$\map g\ x = Λt. λz\ s. x\ [t]\ z\ (s \circ h)$$

let:

$$h : (∀s. s → s) → t \\
h\ \\_ = α\ [t]\ (λy. y)\ (Λt. λz\ s. z)$$

which is your first argument to $α$. Then in your example:

$$α\ [∀s. s→s]\ h\ x \\
= α\ [t]\ (λx.x)\ (\map h\ x) \\
= α\ [t]\ (λx.x)\ (Λt. λ\\_\ s. s (α\ [t]\ (λx. x)\ (Λt. λz\ \\_. z)))$$

Now observe the following from $\Z$ and $\S$

$$
α\ [\Nat]\ (λy. y\ [t]\ α)\ (Λt. λz\ \\_. z) \\
= α\ [t]\ (λx.x)\ (\map (λy. y\ [t]\ α) (Λt. λz\ \\_. z)) \\
= α\ [t]\ (λx.x)\ (Λt. λz\ \\_. z)
$$

$$
α\ [\Nat]\ (λy. y\ [t]\ α)\ (Λt. λ\\_\ s. s\ n) \\
= α\ [t]\ (λx.x)\ (map (λy. y\ [t]\ α) (Λt. λ\\_\ s. s n)) \\
= α\ [t]\ (λx.x)\ (Λt. λ\\_\ s. s (n\ [t]\ α))
$$

Then, if we go back to the calculation from your example:

$$
α\ [t]\ (λx.x)\ (Λt. λ\\_ s. s (α\ [t]\ (λx.x)\ (Λt. λz\ \\_. z))) \\
= α\ [t]\ (λx.x)\ (Λt. λ\\_\ s. s (\Z\ [t]\ α)) \\
= \S\ \Z\ [t]\ α
$$

So your example is extensionally equal to $1$, assuming my calculations are correct.

> **Comments:**
> **username_0**: Thanks Dan! I just tried it and I think you are completely right, wrong behaves exactly like 1. This really shows the difficulties of lambda encodings and extensionality! I have more confidence that the Mendler encoding is adequate now, I think the (r -> t) function makes sure it's adequate, because if we take the Scott-encoding: Fix f = forall t. (forall r. f r -> t) -> t (which is just the encoding of a (weak) existential type) then you can definitely make invalid terms, because you are completely free to chose the r.  
> **username_1**: I suspect you can use parametricity to prove adequacy relative to the Church encoding, because the Mendler Alg should be isomorphic to the Church Alg `f t -> t` for functors `f`. Essentially $(∃r. (r →t)×f\ r) \cong f\ t$ because of the co-Yoneda lemma.  

---

