I’ve been working on a Java implementation, and in general it’s been pretty straightforward to write directly from the spec, but I’ve run into something I don’t understand.
From the spec:
β-normalization does not simplify partially applied built-in functions
…and the reduction rules later on that page for the individual folds only apply in the fully-saturated case.
The Haskell implementation does simplify if any arguments are provided, though:
$ dhall normalize <<< "Natural/fold 0" λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) → zero
I can just follow the Haskell implementation here, but I’m wondering whether the spec or my reading is wrong.