是否可以将 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 的情况丢失了——因为变量总是作为lam 的参数提供。

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

---

如果您必须回答您的问题，有很多方法可以做到。您的两个身份函数都不是目标语言中 lambda 演算身份函数的 HOAS 实现，而是作用于Terms 的 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 ()。