是否可以将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函数的fun1情况，使其行为与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

如果你试图在you中定义术语，就像它通常使用的方式一样，那么你就错了。除了在解释器中，您不应该在构造函数上匹配模式。HOAS中的身份如下：

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

实际上，完全不允许模式匹配是非常常见的，使用类似于

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

还需要注意的是，var案例丢失了--因为vars总是作为lam的一个参数提供。

HOAS的诀窍是使用Haskell的lambda来实现目标语言的lambda，这样您就可以使用裸lambda演算(加上一些额外的语法)编写术语。

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

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 ()。