Call-by-push-value vs fine-grained

[atennapel]

Why choose call-by-push-value as opposed to a fine-grained calculus (like Eff does)? In what sense is a lambda abstraction a computation?

[cmcl]

Albert,

It's a matter of philosophy.

A computation reduces, handles, and produces: I am Frank's Means of Doing.

A value is inert, suspended, and immutable: I am Frank's Means of Being [1].

FG-CBV = Fine-Grained Call-By-Value CPBV = Call-By-Push-Value

In FG-CBV, functions are considered values. In CPBV, functions are considered computations; as you observed, lambda abstractions in CPBV are computations. The same is true in Frank. Frank uses pattern matching clauses to represent them. In Frank, we represent the lambda abstraction \x.M as the single clause x -> M.

In FG-CBV, CPBV, and Frank, we may only bind variables to values. To bind a variable f to a function we would write:

   f = \x.M         in FG-CBV
   f = thunk (\x.M) in CBPV
   f = {x -> M}     in Frank

injecting our computation into a value using the respective thunking constructs.

To apply a function we have:

U V in FG-CBV, V and U both values
V`M in CBPV where V a value, M a computation
m n in Frank where m and n are terms (of distinct kind; see [2])

Assume a value V and term n for which we may apply f above:

f V         in FG-CBV
V`(force f) in CBPV
f n         in Frank <--- syntactic sugar for: f! n

where the ! can be understood as Frank's analogue to "force" in CBPV.

Frank treats functions as special cases of a more general notion of computation. By doing so, Frank is able to generalise the notion of function application to encompass effect handling as well. In contrast, Eff has a restricted form of function application: U V, where U cannot be a handler and V cannot be a computation. Therefore Eff must have a separate with-handle construct for effect handling.

[1] - https://youtu.be/kPPgFa0MfEU [2] - https://arxiv.org/abs/1611.09259

[atennapel]

Thanks so much! That cleared some things up.

I just cannot wrap my head around a lambda abstraction being a computation. To me \x. e does not do anything, it is immutable, a value, inert, there is no computation done. The computation is the application of a function that's when things are done. It seems to me that Frank could also work if functions are values, do you agree?

[frank-dspeed]

@atennapel i think Frank works always :) with values and functions but you should test it your self