lambda演算的按值调用解释器和按名称调用解释器之间的差异

Question

在另一个问题中，Bob为非类型lambda演算提供了以下解释器。

data Expr = Var String | Lam String Expr | App Expr Expr
data Value a = V a | F (Value a -> Value a)
interpret :: [(String, Value a)] -> Expr -> Value a
interpret env (Var x) = case lookup x env of
  Nothing -> error "undefined variable"
  Just v -> v
interpret env (Lam x e) = F (v -> interpret ((x, v):env) e)
interpret env (App e1 e2) = case interpret env e1 of
  V _ -> error "not a function"
  F f -> f (interpret env e2)

Ivan Zakharyaschev指出，由于F f -> f (interpret env e2)，这个解释器是按值调用的按名称调用解释器的实现与上面介绍的有什么不同

Plotkin在20世纪70年代研究了评估lambda演算的按名称调用和按值调用策略。

Answer 1

我认为使用原始数据定义不可能进行正确的名称调用。F (Value a -> Value a)有Value a作为参数，所以我们别无选择，只能传入一些已经解释的值，并且它将根据Haskell约简行为的需要进行调用。

我们可以修改数据定义：

data Value a = V a | F ((() -> Value a) -> Value a)

还让解释器返回显式thunks：

interpret :: [(String, () -> Value a)] -> Expr -> () -> Value a
interpret env (Var x) = delay (case lookup x env of
  Nothing -> error "undefined variable"
  Just v -> force v)
interpret env (Lam x e) = delay (F (v -> force (interpret ((x, v):env) e)))
interpret env (App e1 e2) = delay (case force (interpret env e1) of
  V _ -> error "not a function"
  F f -> f (interpret env e2))
force :: (() -> a) -> a
force f = f ()
{-# NOINLINE force #-}
delay :: a -> () -> a
delay a () = a
{-# NOINLINE delay #-}

现在，我们不再在环境中存储thunk，而是存储一个部分应用程序对象，然后在不同的调用站点分别对其进行评估。

需要force和delay来防止GHC浮出功能体，从而恢复共享。或者，可以使用{-# OPTIONS -fno-full-laziness #-}进行编译，并使用简单的lambda和应用程序来代替上述机制。

Answer 2

CBV/CBN是与lambda演算的评估策略有关的概念，即与lambda项约简中redex的选择有关。在减少术语表示的操作风格解释器中，您可以正确地谈论CBV/CBN。

在像发布的这样的指称风格的解释器中，我会谈论热切语义与懒惰语义，而不是CBV/CBN。当然，热切对应CBV，懒惰对应CBN。

由于Haskell是懒惰的，代码

interpret env (App e1 e2) = case interpret env e1 of
  V _ -> error "not a function"
  F f -> f (interpret env e2)

实现了懒惰语义（CBN）。（正如luqui所说，GHC在操作上会以随需应变的方式减少这种情况）。

为了获得一个热切的（CBV）语义，我们可以在调用之前强制参数：

interpret env (App e1 e2) = case interpret env e1 of
  V _ -> error "not a function"
  F f -> case interpret env e2 of
         V v -> f v
         F g -> f g

这确保了没有未评估的thunk被馈送到函数，除非它们已经在环境中。但是，只有在计算lambda时才会填充环境，lambda将在环境中插入上面的值v和g。因此，不会在那里插入暴徒。