5
$\begingroup$

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))
$\endgroup$
4
$\begingroup$

$\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.

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Labbekak
    Mar 2 at 9:06
  • $\begingroup$ 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. $\endgroup$
    – Dan Doel
    Mar 2 at 16:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.