Haskell，用于评估的 lambda 演算

Question

(图1)

简单类型 lambda 演算的一部分(图 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")) “(常量 3)是一个值”

但是，对于第一个测试用例，我知道这是因为 (Var "x")如 e1是终端所以它不能过渡。这是否意味着我应该添加 Stuck案件？但如果可能的话，我想返回一个表明转换成功的输出。

先感谢您...

Answer 1

如果您将 lambda 演算 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 中编写类型良好的简单类型 lambda 演算类型。我很喜欢 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 - 输入视线。