When a type is a value?

Question

In functional programming and in the theoretical setting of the $\lambda$-calculus it is standard to consider a lambda abstraction $\lambda x.M$ as a value. In my understanding, the intuitive reason is that a function $\lambda x.M$ is an finished piece of data, sharing with other values like $3$ or $\mathtt{true}$ the following ontological status: something that one can handle independently of a notion of execution. (Indeed, you cannot execute $\lambda x.M$ until you apply it to something. Of course you may reduce a $\beta$-redex in $M$, but then intuitively you are not reducing the whole piece of code $\lambda x.M$.)

Now, when it comes to dependent type theories, or more generally any type system having some vertex of Barendregt's cube as its core, all levels of the syntax - objects, types, kinds and possibly all the infinite higher kinds - have the status of terms. So it makes sense to ask when one of them is a value. Let us ask the question for types, but of course the same applies to all possible superior kinds.

Obviously a functional type $\lambda x: T. T' : \Pi x: T.A $ (for $A: \mathtt{Kind}$ and $T:\mathtt{Type}$) is a value. (Notice that in basic dependent type theory, the one without the higher-dimensional kinds $\omega$, the kind $\Pi x: T.A$ is actually $T\to A$).

Now, what about the universal type $\Pi x: T.T'$ (where $T,T': \mathtt{Types}$) ? From a mathematical perspective it is a family, hence a function. It corresponds to my definition of ontology of a value above: something that one can handle independently of a notion of execution. But on the other side $\Pi x: T.T'$ has a relevant difference from $\lambda x: T. T' $: the latter has a destruction operator (the application), whereas the former does not. In light of this, would you consider $\Pi x: T.T'$ as a value?

In a way, I am asking the following (philosophical?) question. Which intuition do you prefer:

1. a value is something that one can handle independently of a notion of execution
2. a value is something that one can handle independently of a notion of execution and when it is not ground can be decomposed via an appropriate operator.

In case 2 the "dependent arrow" type $\Pi x: T.T'$ is not a value, only the functional type $\lambda x: T. T'$ and the polymorphic universal type $\forall X.T$ are.

I am personally inclined towards option 2, but I would like to hear from more experienced researchers.

Answer 1

I will offer a semantic perspective. The relationship between values and general computations may be expressed in terms of an adjunction between two categories: \begin{align*} F &: \mathcal{V} \to \mathcal{C} \\ U &: \mathcal{C} \to \mathcal{V} \\ F &\vdash U \end{align*} Here $\mathcal{V}$ is a category of values, $\mathcal{C}$ is a category of computations. The prototypical example comes from domain theory:

• $\mathcal{V}$ is the category of predomains, i.e., $\omega$-chain complete posets which may not have a list element,
• $\mathcal{C}$ is the category of domains, i.e., $\omega$-chain complete posets with a least element,
• $F$ is the lifting functor
• $U$ is the forgetful functor

This view is closely related to Paul Levy's call-by-push-value (CBPV).

The semantic picture suggests that we should not only distinguish values and computations, but also value types and computations types. Thus, instead of saying that there are terms of type $A$, some of which are values and others are computations, we say instead that there are two kinds of types: the elements of value types are always values, while the elements of computation types are always computations.

In CBPV languages the distinction is explicit. For instance $\mathtt{nat}$ is a value type and $42 : \mathtt{nat}$ while $F \mathtt{nat}$ is a computation type inhabited by computations such as $\mathtt{return}\;42$ and $(\lambda n . n \cdot n + 6) \; 6$.

From a theoretical point of view such a typing discipline is desirable, because the value/computation distinction becomes a proper mathematical concept, rather than a syntactic device that drives normalization algorithms. (I warned you that I will offer the semantic perspective.)

We may think about the distinction between values and computations for dependent types and other corners of Barndregt's cube. The semantic picture suggests that we should again distinguish value types from computation types. Thus, we really should replace the judgement $\Gamma \vdash A \ \mathrm{type}$ ($A$ is a type in context $\Gamma$) with two judgements:

• $\Gamma \vdash A \ \mathrm{vtype}$
• $\Gamma \vdash C \ \mathrm{ctype}$

Of course, the next step requires us to figure out precisely how to extend the above picture to the rather more complicated situation that arises through dependencies. This is a topic of current research, and a great deal of past research.

Now, as to whether something like $(\lambda T . \mathrm{return}\,T) (\prod_{x : A} B(x))$ itself is a value or a computation can be phrased in terms of universes. There ought to be a universe of value types $\mathcal{U}_V$ and a universe of computations $\mathcal{U}_C$, each reflecting the two kinds of judgements above. We also have to decide whether $\mathcal{U}_V$ and $\mathcal{U}_C$ themselves are value or computation types (probably value types, with corresponding computation types $F \mathcal{U}_V$ and $F \mathcal{U}_C$). The typing rules would place $(\lambda T . T) (\prod_{x : A} B(x))$ into one or the other universe (presumably in this case the universe of computations).

I do not really want to give a definitive answer here, I just want to place the question into a proper mathematical context that allows us to consider the mathematical possibilities rather than look for an answer based on experience with normalizing algorithms.

Answer 2

My impression is that most researchers in dependent type theory speak of normal forms instead of values to avoid ambiguity. There are many ways to precisely define evaluation: beta normal form, eta-long normal form, weak head normal form...

When working with dependent types it is important to be exact about how we mean terms to be equal. Since in practice we need to decide equality over types which may contain terms (see the conversion rule). In non-dependent type theories it is fine to talk about values and not bother too much with these details, since the types cannot contain terms and equality checking is straightforward.

There are many active areas of research in dependent type theory that hinge on the equality of terms (HOTT, cubical type theory, intentional/extensional, congruence closure).

Answer 3

In rewriting theory, there are a number of useful definitions of what counts as a value. Here is one which seems quite useful:

A term $t$ in normal form is a value if it is not neutral.

A term $t$ is neutral if for every context $E[\_]$, $E[t]\rightarrow^* u$ iff there is a context $E'[\_]$ and a term $t'$ such that $u = E'[t']$. Edit: And $E[\_]\rightarrow^*E'[\_]$ and $t\rightarrow^*t'$.

I've extended the notion of terms and reductions to contexts and reductions in the obvious way (a context is a term with some "hole").

This allows for a general method to talk about normalization, where one has to take special care to distinguish neutral terms and non-neutral terms in the usual proofs.

This would indeed make $\Pi x:A.B$ a neutral term, and therefore not a value, though one could imagine a setting where a legitimate type constructor, say $I$, could also be a value, if we had, say, the rules

$i : I$

and

$F(I) \rightarrow^* \mathrm{Bool}$

for some defined symbol $F:\mathrm{Type}\rightarrow\mathrm{Type}$. It would take great care for such a system to enjoy consistency, or even subject reduction!

This really nice article by Colin Riba explains some of the technical aspects of termination: Toward a General Rewriting-Based Framework for Reducibility

And work by Frederic Blanqui takes place in these kinds of lax type systems with strange computational type constructors, see. e.g. Definitions by Rewriting in the Calculus of Constructions.