<p>I will offer a semantic perspective. The relationship between values and general computations may be expressed in terms of an adjunction between two categories:
<span class="math-container">\begin{align*}
F &amp;: \mathcal{V} \to \mathcal{C} \\
U &amp;: \mathcal{C} \to \mathcal{V} \\
F &amp;\vdash U
\end{align*}</span>
Here <span class="math-container">$\mathcal{V}$</span> is a category of values, <span class="math-container">$\mathcal{C}$</span> is a category of computations. The prototypical example comes from domain theory:</p>

<ul>
<li><span class="math-container">$\mathcal{V}$</span> is the category of <em>predomains</em>, i.e., <span class="math-container">$\omega$</span>-chain complete posets which may not have a list element,</li>
<li><span class="math-container">$\mathcal{C}$</span> is the category of <em>domains</em>, i.e., <span class="math-container">$\omega$</span>-chain complete posets with a least element,</li>
<li><span class="math-container">$F$</span> is the lifting functor</li>
<li><span class="math-container">$U$</span> is the forgetful functor</li>
</ul>

<p>This view is closely related to Paul Levy's <a href="http://www.cs.bham.ac.uk/~pbl/papers/thesisqmwphd.pdf" rel="nofollow noreferrer">call-by-push-value</a> (CBPV).</p>

<p>The semantic picture suggests that we should not only distinguish values and computations, but also <em>value types</em> and <em>computations types</em>. Thus, instead of saying that there are terms of type <span class="math-container">$A$</span>, some of which are values and others are computations, we say instead that there are two kinds of types: the elements of <em>value</em> types are always values, while the elements of <em>computation</em> types are always computations.</p>

<p>In CBPV languages the distinction is explicit. For instance <span class="math-container">$\mathtt{nat}$</span> is a value type and <span class="math-container">$42 : \mathtt{nat}$</span> while <span class="math-container">$F \mathtt{nat}$</span> is a computation type inhabited by computations such as <span class="math-container">$\mathtt{return}\;42$</span> and <span class="math-container">$(\lambda n . n \cdot n + 6) \; 6$</span>.</p>

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

<p>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 <span class="math-container">$\Gamma \vdash A \ \mathrm{type}$</span> (<span class="math-container">$A$</span> is a type in context <span class="math-container">$\Gamma$</span>) with <em>two</em> judgements:</p>

<ul>
<li><span class="math-container">$\Gamma \vdash A \ \mathrm{vtype}$</span></li>
<li><span class="math-container">$\Gamma \vdash C \ \mathrm{ctype}$</span></li>
</ul>

<p>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. </p>

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

<p>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 <em>mathematical possibilities</em> rather than look for an answer based on experience with normalizing algorithms.</p>

CC BY-SA 4.0
2019-01-16T22:44:40.927Z
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.
Blaisorblade
CC BY-SA 4.0
2019-01-17T08:00:30.097Z
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.
Andrej Bauer
CC BY-SA 4.0
2019-01-17T15:29:08.343Z
This may be the best example of adjunctions I have seen.  Thanks!
user833970
CC BY-SA 4.0
2019-01-16T16:50:06.977Z
2019-01-17T10:44:39.147Z
2019-01-17T10:44:39.147Z
Andrej Bauer
<p>In rewriting theory, there are a number of useful definitions of what counts as a value. Here is one which seems quite useful:</p>
<blockquote>
<p>A term <span class="math-container">$t$</span> in normal form is a <em>value</em> if it is not <em>neutral</em>.</p>
<p>A term <span class="math-container">$t$</span> is <em>neutral</em> if for every context <span class="math-container">$E[\_]$</span>, <span class="math-container">$E[t]\rightarrow^* u$</span> iff there is a context <span class="math-container">$E'[\_]$</span> and a term <span class="math-container">$t'$</span> such that <span class="math-container">$u = E'[t']$</span>. <strong>Edit: And <span class="math-container">$E[\_]\rightarrow^*E'[\_]$</span> and <span class="math-container">$t\rightarrow^*t'$</span>.</strong></p>
</blockquote>
<p>I've extended the notion of terms and reductions to contexts and reductions in the obvious way (a context is a term with some &quot;hole&quot;).</p>
<p>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.</p>
<p>This would indeed make <span class="math-container">$\Pi x:A.B$</span> a neutral term, and therefore not a value, though one could imagine a setting where a legitimate type constructor, say <span class="math-container">$I$</span>, could also be a value, if we had, say, the rules</p>
<p><span class="math-container">$i : I$</span></p>
<p>and</p>
<p><span class="math-container">$F(I) \rightarrow^* \mathrm{Bool}$</span></p>
<p>for some defined symbol <span class="math-container">$F:\mathrm{Type}\rightarrow\mathrm{Type}$</span>. It would take great care for such a system to enjoy consistency, or even subject reduction!</p>
<p>This really nice article by Colin Riba explains some of the technical aspects of termination: <a href="http://perso.ens-lyon.fr/colin.riba/papers/redfull.pdf" rel="nofollow noreferrer">Toward a General Rewriting-Based Framework
for Reducibility</a></p>
<p>And work by Frederic Blanqui takes place in these kinds of lax type systems with strange computational type constructors, see. e.g. <a href="http://rewriting.gforge.inria.fr/papers/lics01.pdf" rel="nofollow noreferrer">Definitions by Rewriting
in the Calculus of Constructions</a>.</p>

CC BY-SA 4.0
2019-01-16T15:22:56.373Z
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.
Domenico Ruoppolo
CC BY-SA 4.0
2019-01-16T20:33:42.863Z
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'$.
Martin Berger
CC BY-SA 4.0
2019-01-16T20:35:19.173Z
Also, if my rendering of *neutral* is right, then $letrec\ f x = f x$ is not a value, because neutral. That would be counter to most working programmers' understanding of value.
Martin Berger
CC BY-SA 4.0
2019-01-17T15:12:12.053Z
@cody I may be misunderstanding your use of contexts, but this would make 3 neutral in a language with nats? (since t = t' = u = 3) So 3 would not be a value?
user833970
CC BY-SA 4.0
2019-01-19T23:52:25.803Z
@MartinBerger of course you are right, I'll amend it.
cody
CC BY-SA 4.0
2019-01-20T00:00:45.240Z
@MartinBerger I don't think it's correct that `letrec f x = f x` is neutral under this (updated) definition: in the context $E=\_ 3$, for example, the context is activated and the resulting context would have to be $\_$.
cody
CC BY-SA 4.0
2019-01-20T00:02:53.633Z
@user833970, with the edited definition, 3 is not neutral, since the context `if _ = 3 then 0 else 1` activates that term, and reduces to a value which is provoked by the interaction of the context and the term.
cody
CC BY-SA 4.0
2019-01-20T14:29:04.413Z
@cody
Let's abbreviate `letrec f x = f x` to $\omega$.

If the context is $E[\cdot] = [\cdot]3$, then $E[\omega ]$ is $\omega 3$, so $E[\omega ] \rightarrow E[\omega ]$, but at the same time $E[\cdot] \rightarrow^* E[\cdot]$ and $\omega  \rightarrow^* \omega$. Hence $\omega$ is neutral, and cannot be a value. The problem is that *syntactially* $\omega$ does consume its argument, but immediately restores itself and its argument.  OTOH *semantically*, $\omega$ has no observable effect -- unless you can observe timing (which the languages relevant in type-theory can't).
Martin Berger
CC BY-SA 4.0
2019-01-20T14:45:25.697Z
@cody You can see a similar phenomenon at play in concurrency: for example the replicated process $!x(v).\overline{x}v$ in the (asynchronous) $\pi$-calculus has no semantic effect, although do exchange messages syntactially: $!x(v).\overline{x}v \ |\ \overline{x}3 \rightarrow !x(v).\overline{x}v \ |\ \overline{x}3 $. The general phenomenon is discussed  in Barendregt's book on untyped $\lambda$-calculus in one of the chapters on equational theory, but I don't have the book to hand at the moment, hence can't tell you where exactly.
Martin Berger
CC BY-SA 4.0
2019-01-22T20:04:26.047Z
@cody: In lambda calculus, usually neutral terms are given by `R ::= x | R M` where `M` are normal form terms (e.g. `R` in http://twelf.org/wiki/Proving_metatheorems:Full_LF). But those terms seem to be not neutral according to your definition! Am I missing something?
Blaisorblade
CC BY-SA 4.0
2019-01-22T22:05:11.320Z
@MartinBerger: ok, I get the counter example! This is an interesting point. In Riba's paper, he only considers single step reductions though. Is this enough to dispel the `letrec` counter-example?
cody
CC BY-SA 4.0
2019-01-22T22:08:12.097Z
@Blaisorblade: I think `R` defined in that way *would* be neutral by this definition! If `x M` is placed in some context, it can't "provoke" any additional reductions, since it is not headed by a $\lambda$ which would create a new redex. This definition is more general, though, and allows `M`s not in normal form (there is some ambiguity in the literature).
cody
CC BY-SA 4.0
2019-01-23T01:02:23.527Z
@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 (!?).
Blaisorblade
CC BY-SA 4.0
2019-01-23T01:04:20.687Z
Also note Riba says (ambiguously) "We now give our formulation of the notion of neutral term, which is more general than the usual ones [GLT89, Gal89]." Clearly, his neutral terms for lambda calculus don't match neither Girard's nor Twelf's (the ones I'm used to).
Blaisorblade
CC BY-SA 4.0
2019-01-23T01:58:54.090Z
@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.
cody
CC BY-SA 4.0
2019-01-23T10:18:54.833Z
@cody Regarding "*only considers single step reductions*", it depends, since we have 3 reductions in the definition: $E[t] \rightarrow^* u$, $E[.]  \rightarrow^* E'[.]$ and $t  \rightarrow^* t'$.  I think you can replace the first of those by a single step $E[t] \rightarrow u$ without changing the terms that are neutral, but the others must remain $\rightarrow^*$ otherwise it becomes a strange definition.
Martin Berger
CC BY-SA 4.0
2019-01-23T10:19:14.363Z
@cody Regarding "only considers single step reductions", it depends, since we have 3 reductions in the definition: $E[t] \rightarrow^* u$, $E[.]  \rightarrow^* E'[.]$ and $t  \rightarrow^* t'$.  I think you can replace the first of those by a single step $E[t] \rightarrow u$ without changing the terms that are neutral, but the others must remain $\rightarrow^*$ otherwise it becomes a strange definition.
Martin Berger
CC BY-SA 4.0
2019-01-23T10:23:22.733Z
@cody The idea that neutrality seeks to define is roughly: computes *as if* not interacting with any context. That's a *semantic* notion. In contrast, the definition we have been discussing here is *syntactic* and simple, hence decidable on terms. I don't expect there to be a simply syntactic definition of this semantic concept, for otherwise one could reduce the halting problem to this syntactic concept. Why? Because a terminated computation is also not interacting with any context.
Martin Berger
CC BY-SA 4.0
2019-01-23T10:37:41.343Z
@cody The reason that the syntactic definition might be OK in type theory is that there all terms terminate. I conjecture that any program that is semantically but not syntactically neutral, must contain subterms that can quine.
Martin Berger
CC BY-SA 4.0
2019-01-24T11:36:00.230Z
@cody you're right on that pretty bad misreading, sorry!! It still seems Riba is *not* using arbitrary contexts as you define them, but just a subset, whose definition changes what counts as neutral?
Blaisorblade
CC BY-SA 4.0
2019-01-31T16:07:00.083Z
@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.
cody
CC BY-SA 4.0
2019-01-31T17:21:40.173Z
@cody Thanks and no worries! My own mistakes will stay up here as well :-)
Blaisorblade
CC BY-SA 4.0
2019-01-15T22:21:00.957Z
2019-01-19T23:53:57.667Z
2020-06-17T09:38:08.363Z
cody
<p>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...</p>

<p>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 <a href="https://ncatlab.org/nlab/show/pure+type+system" rel="nofollow noreferrer">conversion rule</a>).  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.</p>

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

CC BY-SA 4.0
2019-01-16T11:56:51.783Z
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_.
Domenico Ruoppolo
CC BY-SA 4.0
2019-01-16T11:59:11.353Z
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.
Domenico Ruoppolo
CC BY-SA 4.0
2019-01-16T22:37:59.147Z
On CBV dependent types: https://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.
Blaisorblade
CC BY-SA 4.0
2019-01-15T19:29:56.757Z
2019-01-15T19:29:56.757Z
user833970
<p>In functional programming and in the theoretical setting of the <span class="math-container">$\lambda$</span>-calculus it is standard to consider a lambda abstraction <span class="math-container">$\lambda x.M$</span> as a <em>value</em>. In my understanding, the intuitive reason is that a <em>function</em> <span class="math-container">$\lambda x.M$</span> is an finished piece of data, sharing with other values like <span class="math-container">$3$</span> or <span class="math-container">$\mathtt{true}$</span> the following ontological status:  <em>something that one can handle independently of a notion of execution</em>. (Indeed, you cannot execute <span class="math-container">$\lambda x.M$</span> until you apply it to something. Of course you may reduce a <span class="math-container">$\beta$</span>-redex in <span class="math-container">$M$</span>, but then intuitively you are not reducing the whole piece of code <span class="math-container">$\lambda x.M$</span>.)</p>

<p>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 <em>terms</em>. So it makes sense to ask when one of them is a <em>value</em>. Let us ask the question for types, but of course the same applies to all possible superior kinds.</p>

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

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

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

<ol>
<li>a value is <em>something that one can handle independently of a notion of execution</em></li>
<li>a value is <em>something that one can handle independently of a notion of execution</em> and <em>when it is not ground can be decomposed via an appropriate operator</em>. </li>
</ol>

<p>In case 2  the "dependent arrow" type <span class="math-container">$\Pi x: T.T'$</span> is not a value, only the functional type <span class="math-container">$\lambda x: T. T'$</span> and the polymorphic universal type <span class="math-container">$\forall X.T$</span> are.</p>

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

<lo.logic><type-theory><lambda-calculus><functional-programming><dependent-type>
When a type is a value?
Domenico Ruoppolo
# When a type is a value?

(Asked by: username_0 on 2019-01-15)

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.

**Tags:** lo.logic, type-theory, lambda-calculus, functional-programming, dependent-type

---

## 3 answers

### Answer by username_1 on 2019-01-16. Score: 6

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](http://www.cs.bham.ac.uk/~pbl/papers/thesisqmwphd.pdf) (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.

> **Comments:**
> **username_2**: 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.  
> **username_1**: 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.  
> **username_3**: This may be the best example of adjunctions I have seen.  Thanks!  

---

### Answer by username_4 on 2019-01-15. Score: 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](http://perso.ens-lyon.fr/colin.riba/papers/redfull.pdf)

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](http://rewriting.gforge.inria.fr/papers/lics01.pdf).

> **Comments:**
> **username_0**: 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.  
> **username_5**: 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'$.  
> **username_5**: Also, if my rendering of *neutral* is right, then $letrec\ f x = f x$ is not a value, because neutral. That would be counter to most working programmers' understanding of value.  
> **username_3**: @cody I may be misunderstanding your use of contexts, but this would make 3 neutral in a language with nats? (since t = t' = u = 3) So 3 would not be a value?  
> **username_4**: @MartinBerger of course you are right, I'll amend it.  
> **username_4**: @MartinBerger I don't think it's correct that `letrec f x = f x` is neutral under this (updated) definition: in the context $E=\_ 3$, for example, the context is activated and the resulting context would have to be $\_$.  
> **username_4**: @user833970, with the edited definition, 3 is not neutral, since the context `if _ = 3 then 0 else 1` activates that term, and reduces to a value which is provoked by the interaction of the context and the term.  
> **username_5**: @cody Let's abbreviate `letrec f x = f x` to $\omega$.  If the context is $E[\cdot] = [\cdot]3$, then $E[\omega ]$ is $\omega 3$, so $E[\omega ] \rightarrow E[\omega ]$, but at the same time $E[\cdot] \rightarrow^* E[\cdot]$ and $\omega  \rightarrow^* \omega$. Hence $\omega$ is neutral, and cannot be a value. The problem is that *syntactially* $\omega$ does consume its argument, but immediately restores itself and its argument.  OTOH *semantically*, $\omega$ has no observable effect -- unless you can observe timing (which the languages relevant in type-theory can't).  
> **username_5**: @cody You can see a similar phenomenon at play in concurrency: for example the replicated process $!x(v).\overline{x}v$ in the (asynchronous) $\pi$-calculus has no semantic effect, although do exchange messages syntactially: $!x(v).\overline{x}v \ |\ \overline{x}3 \rightarrow !x(v).\overline{x}v \ |\ \overline{x}3 $. The general phenomenon is discussed  in Barendregt's book on untyped $\lambda$-calculus in one of the chapters on equational theory, but I don't have the book to hand at the moment, hence can't tell you where exactly.  
> **username_2**: @cody: In lambda calculus, usually neutral terms are given by `R ::= x | R M` where `M` are normal form terms (e.g. `R` in http://twelf.org/wiki/Proving_metatheorems:Full_LF). But those terms seem to be not neutral according to your definition! Am I missing something?  
> **username_4**: @MartinBerger: ok, I get the counter example! This is an interesting point. In Riba's paper, he only considers single step reductions though. Is this enough to dispel the `letrec` counter-example?  
> **username_4**: @Blaisorblade: I think `R` defined in that way *would* be neutral by this definition! If `x M` is placed in some context, it can't "provoke" any additional reductions, since it is not headed by a $\lambda$ which would create a new redex. This definition is more general, though, and allows `M`s not in normal form (there is some ambiguity in the literature).  
> **username_2**: @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 (!?).  
> **username_2**: Also note Riba says (ambiguously) "We now give our formulation of the notion of neutral term, which is more general than the usual ones [GLT89, Gal89]." Clearly, his neutral terms for lambda calculus don't match neither Girard's nor Twelf's (the ones I'm used to).  
> **username_4**: @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.  
> **username_5**: @cody Regarding "*only considers single step reductions*", it depends, since we have 3 reductions in the definition: $E[t] \rightarrow^* u$, $E[.]  \rightarrow^* E'[.]$ and $t  \rightarrow^* t'$.  I think you can replace the first of those by a single step $E[t] \rightarrow u$ without changing the terms that are neutral, but the others must remain $\rightarrow^*$ otherwise it becomes a strange definition.  
> **username_5**: @cody Regarding "only considers single step reductions", it depends, since we have 3 reductions in the definition: $E[t] \rightarrow^* u$, $E[.]  \rightarrow^* E'[.]$ and $t  \rightarrow^* t'$.  I think you can replace the first of those by a single step $E[t] \rightarrow u$ without changing the terms that are neutral, but the others must remain $\rightarrow^*$ otherwise it becomes a strange definition.  
> **username_5**: @cody The idea that neutrality seeks to define is roughly: computes *as if* not interacting with any context. That's a *semantic* notion. In contrast, the definition we have been discussing here is *syntactic* and simple, hence decidable on terms. I don't expect there to be a simply syntactic definition of this semantic concept, for otherwise one could reduce the halting problem to this syntactic concept. Why? Because a terminated computation is also not interacting with any context.  
> **username_5**: @cody The reason that the syntactic definition might be OK in type theory is that there all terms terminate. I conjecture that any program that is semantically but not syntactically neutral, must contain subterms that can quine.  
> **username_2**: @cody you're right on that pretty bad misreading, sorry!! It still seems Riba is *not* using arbitrary contexts as you define them, but just a subset, whose definition changes what counts as neutral?  
> **username_4**: @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.  
> **username_2**: @cody Thanks and no worries! My own mistakes will stay up here as well :-)  

---

### Answer by username_3 on 2019-01-15. Score: 3

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](https://ncatlab.org/nlab/show/pure+type+system)). 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).

> **Comments:**
> **username_0**: 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_.  
> **username_0**: 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.  
> **username_2**: On CBV dependent types: https://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.  

---

