In theory, yes i would agree that they might be a different somewhere. But it's not clear (at least to me that) is this distinction maters in practice. I think

In theory, yes i would agree that they might be a different somewhere. But it's not clear (at least to me that) is this distinction maters in practice. I think the main point here would that a thunk is also a value. And most type system can already express "a computation which return Type X" by a value of type "() -> X". Adding side effect annotation, it seems to be that a pure function of type "() -> X" gives you very close to the same semantic. It's also unclear to me that one should want to allow both value and computation producing values to be used interchangeably. If the goal of CBPV is about better performance, then being able to mix and match both "kind" of value is probably not wise (at least without good compiler error messages), same as mixing type of values would break a type system.