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?

  • $\begingroup$ What goes wrong if we define $\Phi(A)=\bot$ for all $A$? Then $\varphi_0$ should probably not exist... $\endgroup$
    – cody
    Jul 6, 2017 at 13:28
  • $\begingroup$ I think that works! $\endgroup$ Jul 7, 2017 at 14:40


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.