是否可以将 HOAS 函数转换为延续传递样式?

Question

注意以下Haskell程序：

-- A HOAS term, non-polymorphic for simplicity
data Term
= Lam (Term -> Term)
| App Term Term
| Num Int
-- Doubles every constant in a term
fun0 :: Term -> Term
fun0 (Lam b)   = Lam ( x -> fun0 (b x))
fun0 (App f x) = App (fun0 f) (fun0 x)
fun0 (Num i)   = Num (i * 2)
-- Same function, using a continuation-passing style
fun1 :: Term -> (Term -> a) -> a
fun1 (Lam b)   cont = undefined
fun1 (App f x) cont = fun1 f ( f' -> fun1 x ( x' -> cont (App f' x')))
fun1 (Num i)   cont = cont (Num (i * 2))
-- Sums all nums inside a term
summ :: Term -> Int
summ (Lam b)   = summ (b (Num 0))
summ (App f x) = summ f + summ x
summ (Num i)   = i
-- Example
main :: IO ()
main = do
let term = Lam $  x -> Lam $  y -> App (App x (Num 1)) (App y (Num 2))
print (summ term)                 -- prints 3
print (summ (fun0 term))          -- prints 6
print (fun1 term $  t -> summ t) -- a.hs: Prelude.undefined 

在这里，Term是具有数字常量的(非多态(λ 项，fun0是将项内所有常量加倍的函数。是否可以以延续传递样式重写fun0？换句话说，是否有可能完成fun1函数的undefined情况，使其行为与fun0相同，并且最后print输出6？

Answer 1

如果要将此函数转换为CPS，则还需要在数据类型中转换该函数：

data Term' a
= Lam' (Term' a -> (Term' a -> a) -> a)
| App' (Term' a) (Term' a)
| Num' Int

然后，您可以相应地编写fun1：

fun1 :: Term' a -> (Term' a -> a) -> a
fun1 (Lam' b)   cont = cont (Lam' ( x cont' -> b x cont'))
fun1 (App' f x) cont = fun1 f ( f' -> fun1 x ( x' -> cont (App' f' x')))
fun1 (Num' i)   cont = cont (Num' (i * 2))

并通过适当的调整来summ：

summ' :: Term' Int -> Int
summ' (Lam' b)   = b (Num' 0) summ'
summ' (App' f x) = summ' f + summ' x
summ' (Num' i)   = i

以及 CPS 术语：

term' = Lam' $  x k -> k $ Lam' $  y k' -> k' $ App' (App' x (Num' 1)) (App' y (Num' 2))

您可以很好地运行计算：

> fun1 term' summ'
3

Answer 2

如果您试图以通常使用的方式定义 HOAS 中的术语，那么您就错了。 除了解释器之外，您不应该在构造函数上进行模式匹配。 HOAS 中的标识如下所示：

id2 :: Term
id2 = Lam (x -> x)

事实上，完全禁止模式匹配是很常见的，使用这样的接口

class HOAS t where
lam :: (t -> t) -> t
app :: t -> t -> t

另请注意，缺少var情况 -- 因为 var 始终作为参数提供给lam。

HOAS 中的诀窍是使用 Haskell 的 lambda 来实现目标语言的 lambda，因此您基本上可以用裸 lambda 演算(加上一些额外的语法(编写术语。

---

如果您必须回答您的问题，有很多方法可以做到。您的两个恒等函数都不是目标语言中lambda演算恒等函数的HOAS实现，而是作用于Term的Haskell恒等函数的实现。 您的第一个id0实际上等于

id0' :: Term -> Term
id0' = id

而你的第二个正在形成等于

id1' :: Term -> (Term -> a) -> a
id1' t cont = cont t

(我认为后一种情况的严格程度会有所不同(

请注意，这些与Term类型无关，因此您只是无缘无故地努力工作。

我不相信可以用任何其他东西来填补id1缺失的情况

id1 (Lam b) cont = cont (Lam b)

因为Term -> Term没有为a延续结果类型提供"转义机制"——a可能是Term无法表示的东西，例如IO ()。