7
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ There’s something I can’t follow. Do you suggest that if $(\lambda x: *. x) \Pi_{x: A} B(x)$ were a value type, then it’d be a value? Since the question asks if $\Pi_{x: A} B(x)$ is a value (not a type of values), one could maybe try to infer its kind and check if that is a value or computation kind... tho I’ve never seen any CBPV-like system that allows such questions. $\endgroup$ – Blaisorblade Jan 16 at 22:44
  • 1
    $\begingroup$ Ah yes, I managed to confuse myself. I was going to mention universes, which is my main point, but somehow got side-tracked. I fixed the answer. $\endgroup$ – Andrej Bauer Jan 17 at 8:00
  • $\begingroup$ This may be the best example of adjunctions I have seen. Thanks! $\endgroup$ – user833970 Jan 17 at 15:29
3
$\begingroup$

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).

$\endgroup$
  • $\begingroup$ Sure, I myself coming from the study of the untyped $\lambda$-calculus, I was never convinced by the vague idea of "value", and always been more interested in notions of normal forms. Normal forms are well-established ideas from an ontological perspective: you choose how much of stable part of the term you are happy to get, where stable has the clear meaning of not changed by further reductions. For instance for an head normal form you are considering $\lambda x_1 \dots \lambda x_n. x $ as the stable amount of information deserving to be considered as output or observable. $\endgroup$ – Domenico Ruoppolo Jan 16 at 11:56
  • $\begingroup$ But people more into functional programming use the notion of value differently from the one of observable, and now I was wondering on how a call-by-value dependent type theory would look like. $\endgroup$ – Domenico Ruoppolo Jan 16 at 11:59
  • $\begingroup$ On CBV dependent types: arxiv.org/abs/1202.2923. Beware that formally, “value” does mean “normal form”, just in a lambda calculus without certain congruence rules. But which term is used depends on heuristics. $\endgroup$ – Blaisorblade Jan 16 at 22:37
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks, this is interesting. Anyhow, he existence of different possible definitions of value coming from the generality of rewriting theory seems to prove the implicit point behind my question (which for scientific honesty I was trying to hide): the idea of value is maybe more volatile and ultimately less significant than many think. $\endgroup$ – Domenico Ruoppolo Jan 16 at 15:22
  • 2
    $\begingroup$ I think your definition of neutral is wrong, at least if you want neutral to mean no interaction between term and context. I think $t$ is neutral if $E[t] \rightarrow^* u$ implies there exist $E'[.]$ and $t'$ such that $u = E'[t']$, $E[.] \rightarrow^* E'[.]$ and $t \rightarrow^* t'$. $\endgroup$ – Martin Berger Jan 16 at 20:33
  • 1
    $\begingroup$ @cody Found the problem. You talk about contexts, but Riba talks about elimination contexts. For general contexts, $E$ can be $(\lambda x. []) N$, so $E[x\; M]$ is $(\lambda x.\, X\; M)\; N$. This reduces to $N\; M$, which can't be decomposed. Instead, even $\lambda x. []$ is not an elimination context for Riba for lambda calculus (4.1.2). Yet, he doesn't list $x\; M$ as neutral, only $x$. Instead, "Proofs and types" lists general applications $t \; u$ as neutral (!?). $\endgroup$ – Blaisorblade Jan 23 at 1:02
  • 1
    $\begingroup$ @Blaisorblade I think you're misreading the text after Definition 4.1.3: the set of neutral terms includes the terms $E[x]$ and $E[(\lambda x.t)u)]$ for every context $E[]$ which is actually exactly the applications. $\endgroup$ – cody Jan 23 at 1:58
  • 1
    $\begingroup$ @Blaisorblade you are correct that the elimination contexts are not general contexts, which makes my post incorrect yet again. I'll leave it as is to carry my shame for posterity. Also, sorry for the very late answer. $\endgroup$ – cody Jan 31 at 16:07

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.