Haskell, лямбда-исчисление для оценки

Question

(рисунок 1)

Часть простого типизированного лямбда-исчисления (рисунок 1), это реализовано в Haskell, как указано ниже.

evaluate expression = do 
     case expression of 
     (Application (Lambda x ltype term) value) | isValue value = True -> substitute term x value 
     (Application value e2) | isValue value = True -> let e22 = evaluate e2 in Application value e22 
     (Application e1 e2) -> let e11 = evaluate e1 in Application e11 e2 

Однако, это не работает для этих тестов,

1) print (evaluate (Application (Var "x") (Var "y")))

2) print (evaluate (Application (Constant 3) (Var "y")) "(Constant 3) является значение"

Но для первый тестовый пример, я знаю, потому что (Var "x") как e1 является терминалом, поэтому он не может перейти. Означает ли это, что я должен добавить случай Stuck? Но я хочу вернуть результат, предполагающий успех переходов, если это возможно.

Спасибо заранее ...

Answer 1

Если вы разрабатываете свой лямбда-исчисление AST, как что-то вроде

data Exp = Var String 
     | Constant Int 
     | App Exp Exp 
     | Lam String Exp 

интерпретатор evaluate :: Exp -> Out может произвести ряд значений, некоторые результат плохо введенный ввод. Например,

evaluate (Lam "f" (Lam "x" (App (Var "f") (Var "x"))) 
-- type like (a -> b) -> a -> b 

evaluate (Var "x") 
-- open term, evaluation gets stuck 

evaluate (App (Lam "x" (Constant 4)) (Constant 3)) 
-- term results in a constant 

Мы должны будем представить все эти типы в возвращаемом типе. Типичный способ сделать это - использовать универсальный тип, такой как

data Out 
    = Stuck 
    | I Int 
    | F (Out -> Out) 

, который снова подчеркивает необходимость в застрявшем корпусе. Если мы исследуем App ветви evaluate

evaluate (App e1 e2) = case evaluate e1 of 
    Stuck -> Stuck 
    I i -> Stuck 
    F f -> f (evaluate e2) 

шоу как Stuck случаев и поднимаются наверх и может возникнуть из слабо типизированных условий.

---

В Haskell существует множество способов написания типично типизированного типичного типа лямбда-исчисления. Я очень люблю Higher-Order Abstract Syntax Final Encoding. Это чудесно симметрично.

class STLC rep where 
    lam :: (rep a -> rep b) -> rep (a -> b) 
    app :: rep (a -> b) -> (rep a -> rep b) 
    int :: Int -> rep Int 

newtype Interpreter a = Reify { interpret :: a } -- just the identity monad 

instance STLC Interpreter where 
    lam f = Reify $ interpret . f . Reify 
    app f a = Reify $ interpret f $ interpret a 
    int  = Reify 

В этой формулировке, это вообще невозможно, чтобы написать тип STLC rep => rep a, который не очень хорошо напечатанный и никогда не торчит. Тип interpret указывает на это, а

interpret :: Interpreter a -> a 

Нет Out -type в поле зрения.

Answer 2

Но как работает substitute (то есть, какова реализация функции substitute в haskell).