First a thanks for this great site and for your kind attention!
I don't understand the conclusion of the syllogism on page 182 of the Fifth Printing of The Little Typer. It states:
Variables that are not defined are neutral. If the target of an eliminator expression is neutral, then the eliminator expression is neutral. Thus, values are not neutral.
Ok, I understand the two premises, and I understand that an eliminator expression with a neutral target is not a value, because a value has a constructor at top, not an eliminator. That means we have an expression that is both not-a-value and neutral, namely a neutrally targeted eliminator expression.
How do these premises imply that all values are not neutral, or, in other words, that if something is neutral, then it's not a value? Why is something like (add1 n), a value with a constructor, add1, at top, over a neutral variable, itself not neutral?
Or is it the case that the only neutrals are variables and neutrally targeted eliminator expressions, covered by the premises? Are there no other kinds of neutral expressions?
You're right: the only neutral expressions are variables or eliminators whose targets are themselves neutral.
Why do we have the concept of neutral expressions? When type checking, it is sometimes necessary to compare a type that's expected for an expression with the type that was actually found for it. This comparison uses the form of judgment "___ and ___ are the same type". This form of judgment, along with "___ is the same ___ as ___", is implemented by finding the normal forms of both expressions and then checking them for alpha-equivalence (that is, syntactic identity modulo consistent renaming of bound variables). Because finding normal forms involves computing inside of lambda, a normal form might end up being just a variable - we need neutral expressions to be able to talk about these "stuck" expressions, and contrast them with values or with reducible expressions (redexes) that contain opportunities to compute.
The reason (add1 n) is not neutral is just a matter of definition. The term "neutral" is defined as it is because neutral expressions play a certain role in the functioning of the language, and values like(add1 n) don't play that same role. You've understood it correctly, and its purpose should become more clear once equality is introduced later on in the book.
3 Likes
I've had a lot of fun analyzing Chapter 8, which introduces equality, picking Ch. 8 apart and putting it back together several times 
I think i've got it by now. And not just for fun. I'm watching for mistakes in the type systems in some new compilers. Thanks again for helping!
Perhaps it's also valid to say that (add1 n) is not neutral because its normal form (reported by Pie):
;; (+ 1) ; input to REPL
; (the (→ Nat ; response from REPL
; Nat)
; (λ (j)
; (add1 j)))
is not neutral because it has a lambda constructor up top ?