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

What is going on here? Why can a fun be both a normal form and a stuck/neutral term?
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**: @cody 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  

---

