haskell - 我是不是写了续篇？

Question

我没有关于延续的正式知识，并且想知道是否有人可以帮助我验证和理解我编写的代码:)。

问题

我要解决的一般问题是将表达式转换为

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

进入函数

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

然后可以将其传递到 yices-painless包裹。

动机

作为一个更简单的示例，请注意 var翻译成 \x -> x .我们如何将两个 var 相乘的(表示它们 \x -> x 和 \y -> y )到一个表达式 \x -> \y -> x * y ?

我听说延续被描述为“计算的其余部分”，并认为这就是我所需要的。遵循这个想法，一个 var应该有一个功能

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

其参数将是变量 var 的值创建并返回我们想要的(标记为 result 的代码 list )，一个采用变量 x 的新函数并返回 f x .因此，我们定义，

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

然后，对于乘法，比如说 xf和 yf (例如，它可能等于 var)，我们想要使用“剩余计算”函数 f :: α -> E如上，并返回一个新函数。给定 xf 的值，我们知道函数应该做什么。和 yf (表示为 x 和 y 下面)，并将其定义为，

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

代码

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

好吧，它似乎工作。

Answer 1

是的，这是用延续传递风格 (CPS) 编写的。

有人曾经向我解释过 continuations 是“无处不在的回调”，我觉得这并不是特别有用，但也许你会。

就像很多事情一样，你能做的最好的事情可能就是继续努力，以提高风格的流畅度。