<p>Let $\Phi$ be a type functor definable in polymorphic lambda calculus:
$$ \alpha : * \vdash \Phi(\alpha) : * $$
$$ f : A \to B \vdash \mathsf{Map}^{A,B}_\Phi(f) : \Phi(A) \to \Phi(B)$$
Suppose further that $\Phi$-types form a filter:
$$ \vdash \cap^{A,B}_\Phi(x,y) : \Phi(A) \to \Phi(B) \to \Phi(A \land B) $$</p>

<p>Does there exist a type $\mu \Phi$ with the following properties:</p>

<ol>
<li>$\qquad \vdash a : \Phi(A)\quad \Longrightarrow \quad \vdash \varphi_{A,a} : \mu \Phi \to A$</li>
<li>$\qquad \vdash \varphi_0 : \Phi(\mu \Phi)$</li>
</ol>

<p>(Intuitively, the denotation of $\mu\Phi$ should be $\bigcap \{ [\![A]\!] \mid \Phi(A) \}$.)</p>

<p>If we put $\mu\Phi := \forall \alpha. (\Phi(\alpha) \to \alpha)$, then the first condition obtains via $\varphi_{A,a} = \lambda m. m A a$.  </p>

<p>Is it always possible to satisfy the second condition too?  Or is there a counterexample?</p>

CC BY-SA 3.0
2017-07-06T13:28:18.873Z
What goes wrong if we define $\Phi(A)=\bot$ for all $A$? Then $\varphi_0$ should probably not exist...
cody
CC BY-SA 3.0
2017-07-07T14:40:21.983Z
I think that works!
Andrew Polonsky
<lo.logic><lambda-calculus><type-systems><polymorphism>
Finite intersection property of polymorphic type families
Andrew Polonsky
# Finite intersection property of polymorphic type families

(Asked by: username_0 on 2017-07-05)

Let $\Phi$ be a type functor definable in polymorphic lambda calculus:
$$ \alpha : \* \vdash \Phi(\alpha) : \* $$
$$ f : A \to B \vdash \mathsf{Map}^{A,B}\_\Phi(f) : \Phi(A) \to \Phi(B)$$
Suppose further that $\Phi$-types form a filter:
$$ \vdash \cap^{A,B}\_\Phi(x,y) : \Phi(A) \to \Phi(B) \to \Phi(A \land B) $$

Does there exist a type $\mu \Phi$ with the following properties:

1. $\qquad \vdash a : \Phi(A)\quad \Longrightarrow \quad \vdash \varphi\_{A,a} : \mu \Phi \to A$
2. $\qquad \vdash \varphi\_0 : \Phi(\mu \Phi)$

(Intuitively, the denotation of $\mu\Phi$ should be $\bigcap \{ [\![A]\!] \mid \Phi(A) \}$.)

If we put $\mu\Phi := \forall \alpha. (\Phi(\alpha) \to \alpha)$, then the first condition obtains via $\varphi\_{A,a} = \lambda m. m A a$.

Is it always possible to satisfy the second condition too? Or is there a counterexample?

**Tags:** lo.logic, lambda-calculus, type-systems, polymorphism

> **Comments:**
> **username_1**: What goes wrong if we define $\Phi(A)=\bot$ for all $A$? Then $\varphi_0$ should probably not exist...  
> **username_0**: I think that works!  

---

## 0 answers

