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

Question

В другом вопросе Боб представил следующее interpreter for the untyped lambda calculus.

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 remarked что этот интерпретатор вызов по значению за счет F f -> f (interpret env e2). Каким образом реализация интерпретатора по имени может отличаться от представленного выше?

Плоткин изучил call-by-name and call-by-value strategies для оценки исчисления лямбда в 1970-х годах.

Answer 1

Я не думаю, что надлежащее имя по вызову возможно с исходным определением данных. 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 #-} 

Теперь, вместо того, чтобы хранить в преобразователь, в среде, мы храним partial application object, а затем оценивать его отдельно на разных сайтах.

force и delay необходимы для предотвращения GHC от плавающих вне тела функций, thereby recovering sharing. В качестве альтернативы, можно компилировать с {-# OPTIONS -fno-full-laziness #-} и использовать простые лямбды и приложения, а вместо вышеуказанной машины.

Answer 2

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

Чтобы получить нетерпеливую (ОЦК) семантику, мы можем заставить аргумент перед вызовом:

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 выше в окружающую среду. Следовательно, там не будет добавлено никаких трюков.