Did I just write a continuation?

Question

I don't have formal knowledge of continuations, and am wondering if someone can help me verify and understand the code I wrote :).

Problem

The general problem I'm trying to solve is to convert expressions like

(2 * var) + (3 * var) == 4

into functions

\x y -> 2 * x + 3 * y == 4 -- (result)

which can be then passed into the yices-painless package.

Motivation

As a simpler example, note that var is translated into \x -> x. How can we multiply two var's (denote them \x -> x and \y -> y) into one expression \x -> \y -> x * y?

I've heard continuations described as the "rest of computation", and thought that's what I need. Following that idea, a var should take a function

f :: α -> E -- rest of computation

whose argument will be the value of the variable var created, and return what we want (code listing marked result), a new function taking a variable x and returning f x. Hence, we define,

var' = \f -> (\x -> f x)

Then, for multiplication, say of xf and yf (which could be equal to var, for example), we want to take a "rest of computation" function f :: α -> E as above, and return a new function. We know what the function should do given the values of xf and yf (denoted x and y below), and define it as so,

mult xf yf = \f -> xf (\x -> yf (\y -> f (x Prelude.* y)))

Code

const' c = \f -> f c
var' = \f -> (\x -> f x) -- add a new argument, "x", to the function
add xf yf = \f -> xf (\x -> yf (\y -> f (x Prelude.+ y)))
mult xf yf = \f -> xf (\x -> yf (\y -> f (x Prelude.* y)))

v_α = var' -- "x"
v_β = var' -- "y"
v_γ = var' -- "z"
m = mult v_α v_β -- "x * y"
a = add m v_γ -- "x * y + z"
eval_six = (m id) 2 3
eval_seven = (a id) 2 3 1

two = const' 2 -- "2"
m2 = mult two v_γ -- "2 * z"
a2 = add m m2 -- "x * y + 2 * z"
eval_two = (m2 id) 1
eval_eight = (a2 id) 2 3 1

quad_ary = (var' `mult` var') `mult` (var' `mult` var')
eval_thirty = (quad_ary id) 1 2 3 5

well, it seems to work.

Answer 1

Yes, this is written in continuation passing style (CPS).

Somebody once explained continuations to me as "callbacks everywhere", which I didn't find particularly useful but maybe you will.

As seems true with so many things, probably the best you can do is to keep working on this to develop more fluency with the style.