It seems to me that Fine-grain call-by-value already subsumes CBV and CBN, using lambdas as thunks. What does CBPV improve upon FG-CBV or in what way is it "better"?
1 Answer 1
Fine-grained CBV does not subsume call-by-name.
In Fine-grained CBV, the computations $\Gamma \vdash M: A \rightharpoonup B$ do not satisfy unrestricted $\eta$ equality $$ M \equiv \lambda x. M x$$ because $M$ is interpreted as a computation that performs effects and returns a thunk, so if $M$ is a printing or diverging computation the above equality is violated. Instead we have the call-by-value $\eta$ only, which says that this equality is true if we know $M$ to be a value.
This means for instance we cannot build up the type of two argument functions compositionally and have it satisfy $$A \rightharpoonup A' \rightharpoonup B \cong A \times A' \rightharpoonup B$$
However, there is some confusion about the terminology "call-by-name". Some treatments allow for observation of termination at function type (such as reduction to weak head normal form), but this is poorly behaved semantically as it admits neither the function $\eta$ nor the boolean/sum/tuple $\eta$. Levy distinguishes between these by calling the latter "lazy", and he shows in the CBPV monograph that lazy semantics is subsumed by (fine-grained) CBV. The lazy semantics is roughly what Haskell corresponds to because of seq so this does cause some confusion.