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!
1 Like
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 ?
Sorry for the late reply!
It's not quite correct to say that (+ 1) is not neutral because it's normal form has a lambda at the top. This is because whether an expression is neutral or in normal form is not a property that's invariant under substitution or computation - it's a property of a specific way of writing something rather than a property of the thing itself.
(+ 1) is not neutral because + is defined to mean some particular thing, and this thus not itself neutral. The target of the eliminator (that is, the function position in the application form (+ 1)) is thus also not neutral, so the whole application form cannot be neutral.
This is really a matter of referential transparency (in the sense that Quine uses it, not quite the way programmers use it). My name in "'David' has five letters" can't be replaced by something that has the same meaning while preserving truth - e.g., writing "'The author of this Discourse post' has five letters" is false, because it's a much longer sentence that contains 28 letters and some spaces. This is because quotations that talk about the form of a word rather than the meaning of it are referentially opaque.
In the sentence "E is a neutral term", the position E is referentially opaque. The same goes for E in the sentence "E is in normal form". In other words, even though (+ 1) means the same thing as (lambda (n) (add1 n)), the former is not in normal form, but the latter is. Similarly, in a context where f is bound by a lambda, (f 5) is neutral, but the equivalent (which-Nat 0 (f 5) (lambda (b) (f (f b)))) is not neutral.
Thus, the normal form of an expression is irrelevant when talking about whether the expression itself is a value or neutral.
Hope that's (still) useful!