<p>They are different things. <code>SClos</code> is a case-split function, which is a function that pattern match on its parameter. Think of it as a lambda (if you know Haskell, you can think of it as a LambdaCase <code>\case</code>, which is a sugared lambda). This is definitely a canonical value in Mini-TT.</p>
<p>The neutral value, OTOH, is an <em>application</em> on a case-split function, where the argument supplied is neutral. If an instance of a sum type is neutral, you don't know which constructor it belongs to, so you don't know which clause in the pattern matching should be selected, so this is a neutral value.</p>
<p>Summary: pattern matching itself is canonical, while application on pattern matching is not. If this application stucks, it becomes a neutral value.</p>

CC BY-SA 4.0
2021-05-21T04:00:22.280Z
Btw, I prefer the following definition of 'neutral value' (by induction):

0. A variable reference is a neutral value
1. Eliminating a neutral value gives a neutral value
ice1000
CC BY-SA 4.0
2021-05-21T04:00:08.323Z
2021-05-21T04:00:08.323Z
ice1000
<p>I am studying <a href="http://www.cse.chalmers.se/%7Ebengt/papers/GKminiTT.pdf" rel="nofollow noreferrer">A simple type-theoretic language: MiniTT</a>, which introduces a dependently typed language with The language contains data types, mutual recursive/inductive definitions and a universe of small types. The type checking proceeds by a mostly-straightforward bidirectional type-checking, coupled with normalization-by-evaluation to compute normal forms. It is here that I am confused. First, some quick syntax:</p>
<p>A sum type is created using <code>Sum(c1 A1, ..., cn An)</code>, which contains objects
of the form <code>ci E : Sum(c1 A1, ..., cn An)</code>, where <code>E: Ai</code>. For example, booleans are encoded as <code>Sum(true 1, false 1)</code> where <code>1</code> is the unit type. The type of naturals is encoded as <code>rec Nat : U = Sum (zero | succ Nat)</code>. Sum types are eliminated using case-analysis, written as <code>fun(c1 M1, ..., cn Mn)</code>, where each constructor is <code>ci</code> and the associated handler is <code>Mi</code>. For example, the elimination rule for booleans can be encoded as:</p>
<pre><code>Bool : U = Sum (true | false)
elimBool : Π C:Bool → U. C false → C true → Π b:Bool. C b
= λ C.λ h0.λ h1.fun (true → h1 | false → h0)
</code></pre>
<p>and the elimination for naturals can be written as:</p>
<pre><code>rec natrec: ΠC : Nat → U. C zero → (Πn:Nat . C n → C (succ n)) → Π n:Nat. C n
= λ C.λ a.λ g. fun (zero → a | succ n1 → g n1 (natrec C a g n1))
</code></pre>
<p>Now, I had always assumed that when implementing normalization-by-evaluation (NBE), the normal forms always consist of <em>constructors</em>, while the neutral values consist of <em>eliminators</em>, since an eliminator can get stuck if it does not know enough about its argument, while a constructor can always freely construct.</p>
<p>However, in the paper's implementation of NBE (given in the appendix), it appears that <code>Fun</code> (labelled sum eliminators) are one of the normal forms:</p>
<pre><code>data Val =
Lam Clos
 ...
| Fun SClos -- function is a normal form?!
...
| Nt Neut
deriving Show
</code></pre>
<p>Furthermore, the inductive data type of stuck/neutral values has <em>yet another</em> encoding of a stuck <code>fun</code>, called as <code>NtFun</code>:</p>
<pre><code>data Neut = Gen Int
...
| NtFun SClos Neut -- Fun as a stuck term
</code></pre>
<p>I have not seen an explanation of NBE which allows one to encode a particular syntactic category (in this case, the labelled sum eliminator <code>fun</code>), as both a normal form and a neutral/stuck term.</p>
<ol>
<li>What is going on here? Why can a <code>fun</code> be <em>both</em> a normal form and a stuck/neutral term?</li>
<li>How should I think about what my normal forms and stuck terms should be? I had previously imagined that constructors would be normal forms, and eliminators are stuck terms. What's the rule of thumb that's being followed here?</li>
</ol>

CC BY-SA 4.0
2021-05-20T21:33:02.987Z
I think your intuition for neutral terms is not quite right: it's terms which cannot create *new reductions* when substituted in an evaluation context. E.g. $$\lambda. x. x$$ creates a new evaluation when put in the context $$[\_]\ t$$.
cody
CC BY-SA 4.0
2021-05-21T11:48:08.033Z
@cody What is the definition of "context" here? It is not the same as the typing judgement context `Γ ⊢ ...` is it?
Siddharth Bhat
CC BY-SA 4.0
2021-05-21T12:59:01.220Z
No it's an *evaluation context*, i.e. a term with a hole, in which to put the "thing I am currently evaluating". See e.g. these slides by Andrew Myers: https://courses.cs.cornell.edu/cs6110/2009sp/lectures/lec08-sp09.pdf
cody
<dependent-type><normalization>
NBE for MiniTT: Why is labelled sum eliminator both a normal form and a neutral value?
Siddharth Bhat
# NBE for MiniTT: Why is labelled sum eliminator both a normal form and a neutral value?

(Asked by: username_0 on 2021-05-20)

I am studying [A simple type-theoretic language: MiniTT](http://www.cse.chalmers.se/%7Ebengt/papers/GKminiTT.pdf), which introduces a dependently typed language with The language contains data types, mutual recursive/inductive definitions and a universe of small types. The type checking proceeds by a mostly-straightforward bidirectional type-checking, coupled with normalization-by-evaluation to compute normal forms. It is here that I am confused. First, some quick syntax:

A sum type is created using `Sum(c1 A1, ..., cn An)`, which contains objects
of the form `ci E : Sum(c1 A1, ..., cn An)`, where `E: Ai`. For example, booleans are encoded as `Sum(true 1, false 1)` where `1` is the unit type. The type of naturals is encoded as `rec Nat : U = Sum (zero | succ Nat)`. Sum types are eliminated using case-analysis, written as `fun(c1 M1, ..., cn Mn)`, where each constructor is `ci` and the associated handler is `Mi`. For example, the elimination rule for booleans can be encoded as:

```
Bool : U = Sum (true | false)
elimBool : Π C:Bool → U. C false → C true → Π b:Bool. C b
= λ C.λ h0.λ h1.fun (true → h1 | false → h0)

```

and the elimination for naturals can be written as:

```
rec natrec: ΠC : Nat → U. C zero → (Πn:Nat . C n → C (succ n)) → Π n:Nat. C n
= λ C.λ a.λ g. fun (zero → a | succ n1 → g n1 (natrec C a g n1))

```

Now, I had always assumed that when implementing normalization-by-evaluation (NBE), the normal forms always consist of *constructors*, while the neutral values consist of *eliminators*, since an eliminator can get stuck if it does not know enough about its argument, while a constructor can always freely construct.

However, in the paper's implementation of NBE (given in the appendix), it appears that `Fun` (labelled sum eliminators) are one of the normal forms:

```
data Val =
Lam Clos
 ...
| Fun SClos -- function is a normal form?!
...
| Nt Neut
deriving Show

```

Furthermore, the inductive data type of stuck/neutral values has *yet another* encoding of a stuck `fun`, called as `NtFun`:

```
data Neut = Gen Int
...
| NtFun SClos Neut -- Fun as a stuck term

```

I have not seen an explanation of NBE which allows one to encode a particular syntactic category (in this case, the labelled sum eliminator `fun`), as both a normal form and a neutral/stuck term.

1. What is going on here? Why can a `fun` be *both* a normal form and a stuck/neutral term?
2. How should I think about what my normal forms and stuck terms should be? I had previously imagined that constructors would be normal forms, and eliminators are stuck terms. What's the rule of thumb that's being followed here?

**Tags:** dependent-type, normalization

> **Comments:**
> **username_1**: I think your intuition for neutral terms is not quite right: it's terms which cannot create *new reductions* when substituted in an evaluation context. E.g. $$\lambda. x. x$$ creates a new evaluation when put in the context $$[\_]\ t$$.  
> **username_0**: @username_1 What is the definition of "context" here? It is not the same as the typing judgement context `Γ ⊢ ...` is it?  
> **username_1**: No it's an *evaluation context*, i.e. a term with a hole, in which to put the "thing I am currently evaluating". See e.g. these slides by Andrew Myers: https://courses.cs.cornell.edu/cs6110/2009sp/lectures/lec08-sp09.pdf  

---

## 1 answers

### Answer by username_2 on 2021-05-21. Score: 3 | Accepted answer

They are different things. `SClos` is a case-split function, which is a function that pattern match on its parameter. Think of it as a lambda (if you know Haskell, you can think of it as a LambdaCase `\case`, which is a sugared lambda). This is definitely a canonical value in Mini-TT.

The neutral value, OTOH, is an *application* on a case-split function, where the argument supplied is neutral. If an instance of a sum type is neutral, you don't know which constructor it belongs to, so you don't know which clause in the pattern matching should be selected, so this is a neutral value.

Summary: pattern matching itself is canonical, while application on pattern matching is not. If this application stucks, it becomes a neutral value.

> **Comments:**
> **username_2**: Btw, I prefer the following definition of 'neutral value' (by induction):  0. A variable reference is a neutral value 1. Eliminating a neutral value gives a neutral value  

---

