Разница между вызовом по значению и переводчиком по имени для лямбда-исчисления

В другом вопросе Боб представил следующий интерпретатор для нетипизированного лямбда-исчисления.

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)

Иван Захарящев отметил, что этот переводчик является наемным по причине F f -> f (interpret env e2), Как реализация интерпретатора вызова по имени будет отличаться от представленной выше?

Плоткин изучал стратегии " по именам" и "по стоимости" для оценки лямбда-исчисления в 1970-х годах.

Источник

2 ответа

Решение

Я не думаю, что правильный вызов по имени возможен с исходным определением данных. F (Value a -> Value a) имеет Value a в качестве аргумента, поэтому у нас нет другого выбора, кроме как передать какое-то уже интерпретированное значение, и оно будет вызываться по необходимости в поведении редукции Haskell.

Мы могли бы изменить определение данных:

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

А также пусть интерпретатор возвращает явные выражения:

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 #-} и использовать простые лямбды и приложения вместо вышеупомянутого механизма.

Источник

CBV/CBN - это понятия, связанные со стратегией оценки лямбда-исчисления, т. Е. Связанные с выбором редекс в сокращении лямбда-терминов. В интерпретаторе операционного стиля, который сокращает представление терминов, вы можете правильно говорить о 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). (Как утверждает Луки, оперативно 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

Это гарантирует, что в функцию не будут переданы недооцененные блоки, если они уже не находятся в среде. Среда, однако, заполняется только при оценке лямбда, которая будет вставлять значения v,g выше в окружающей среде. Следовательно, никакие громоотводы не будут вставлены туда.

Источник
Другие вопросы по тегам