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
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
funbe 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?