λ-cube: Why are dependent types and dependent functions on the same axis?

384 Views Asked by At

The lambda cube seems to unify the concepts of dependent types (types that depend on terms) with dependent functions (functions whose return type depends on an argument) into a single axis.

But what is the reason for that? How is the relationship between these two concepts any different than the relationship between type constructors and polymorphism?

2

There are 2 best solutions below

1
On BEST ANSWER

I believe the following is one of possibly multiple ways of interpreting the lambda cube. One way to think of this is that if $A:*$, then $A$ is a small type, and if $K:\square$, then $K$ is a large type. In particular we have $*:\square$. We describe the cube as follows.

  1. ($\lambda_\to$, or $(*,*)$) In the simply typed lambda calculus, the type of a lambda term is given $$A : *, B : *,\qquad x:A\vdash t:B\quad\implies\quad \lambda(x:A).t :\Pi(A,x.B) :*$$ At first this may seem surprising, because $B$ should not be allowed to depend on $x:A$. However, in order to have a dependent type $B$, we need a function symbol, for example, $\texttt{Id}:A\to A\to *$ which is not typable in $\lambda_\to$ because $A\to A\to * :\square$. This means that we can safely write $\Pi(A,x.B) = A\to B$ if we restrict ourselves to this system.

  2. ($\lambda P$, or $(*,\square)$) For dependent types we have $$A:*,K:\square,\qquad x:A \vdash t : K\quad\implies\quad \lambda (x:A).t : \Pi(A,x.K) :\square$$ For example, we may assign a type to the identity type for the natural numbers $$\lambda (x,y:\mathbb N). \texttt{Id_nat}(x,y) : \mathbb N\to\mathbb N\to *.$$ We can now answer your question: it is $\lambda_\to$ which allows us to write and type a dependent function, but we cannot have dependent types without $\lambda P$. For example, $$\lambda (x:\mathbb N).\texttt{refl_nat}(x) : \Pi(\mathbb N, x.\texttt{Id_nat}(x,x))$$

  3. ($\lambda 2$, or $(\square,*)$) For polymorphic types we have $$K:\square, B:*,\qquad \alpha : K \vdash t : B\quad\implies\quad \Lambda(\alpha:K).t : \Pi(K,\alpha.B) :*$$ For example, we may type the polymorphic identity function as $$\Lambda(\alpha:*).\lambda(x:\alpha).x :\Pi(*,\alpha.\alpha\to \alpha))$$

  4. ($\lambda\omega$, or $(\square,\square)$) Type constructors can be typed as follows $$K,L:\square,\qquad\alpha : K\vdash t : L\quad\implies\quad \Lambda(\alpha:K).t :\Pi(K,\alpha.L) :\square$$ for example, the type constructor for vectors is typed $$\Lambda(\alpha:*).\lambda (n:\mathbb N).\texttt{Vec}(\alpha,n) : \Pi(*,\alpha.\mathbb N\to *)$$


As an application of all three axes, we can now write: $$\Lambda (\alpha :*).\lambda (x,y:\alpha).\texttt{Id}(\alpha,x,y) : \Pi(*,\alpha.\alpha\to\alpha\to *).$$ which requires both $\lambda\omega$ and $\lambda P$, as well as its constructor $$\Lambda (\alpha : *).\lambda (x:\alpha).\texttt{refl}(\alpha,x) :\Pi(*,\alpha.\texttt{Id}(\alpha,x,x)),$$ which requires $\lambda 2$.

4
On

I find the most helpful way to think of the $\lambda$-cube as representing the 4 variations on term—type interbinding.

  • (λ→) Terms may be bound in terms (functions).
  • (λ2) Types may be bound in terms (polymorphism).
  • (λP) Terms may be bound in types (type dependency).
  • (λω) Types may be bound in types (type constructors).

If $x$ may be bound in $y$, then as a consequence $y$ may naturally depend on $x$ (for $x, y \in \{ \text{terms}, \text{types} \}$). The various assignments of $x$ and $y$ correspond to different axes of the $\lambda$-cube. However, the simply-typed $\lambda$-calculus (λ→), is always present (we could alternatively consider a $\lambda$-tesseract, where this too is given as an axis).

In this way, one may see that polymorphism, type dependency, and type constructors are orthogonal concepts.

As an aside, note that it is possible (in the general context of type theory) to talk about type dependency without allowing terms to be bound in terms (for example, the $\mathrm{Id}$-type in Martin-Löf Type Theory). It is also possible to consider types that bind terms other than $\Pi$-types (for example, $\Sigma$-types). However, the $\lambda$-cube specifically focuses on functions.