2

Matt Might谈到在7 行 Scheme中实现Lambda Calculus解释器：

; eval takes an expression and an environment to a value
(define (eval e env) (cond
  ((symbol? e)       (cadr (assq e env)))
  ((eq? (car e) 'λ)  (cons e env))
  (else              (apply (eval (car e) env) (eval (cadr e) env)))))

; apply takes a function and an argument to a value
(define (apply f x)
  (eval (cddr (car f)) (cons (list (cadr (car f)) x) (cdr f))))

; read and parse stdin, then evaluate:
(display (eval (read) '())) (newline)

现在这不是简单类型的 Lambda 演算。在Haskell 的核心中，有一种与System F非常相似的中间语言。一些人（包括Simon Peyton Jones）称其为简单类型 Lambda 演算的实现。

我的问题是：扩展无类型 Lambda 演算实现以涵盖简单类型 Lambda 演算需要什么？

4

3 回答 3

4

很不清楚你在问什么，但我能想到几个有效的答案：

  • 需要更改表示以适应 lambda 抽象引入的变量的类型注释。

  • 根据您的表示，可能会表示非良好类型的术语。如果是这样，您将需要实现类型检查器。

  • 对于评估，您不需要更改 LC 评估器中的任何内容，除了忽略类型注释（这是类型擦除的全部意义）。但是，如果您编写一个基本上是 的评估器，那么与编写定制函数evalUntyped . eraseTypes相比，您可能更难证明它是完全的。evalTyped

于 2016-06-21T05:39:57.723 回答
1

简单类型的 lambda 演算 (STLC) 只是将类型检查器添加到您描述的系统中。也就是说，您可以将此评估器视为 STLC 的“运行时系统”。

侧节点：通常将类型注释添加到语言中以简化类型检查器的工作，但它们不是必需的。

于 2016-06-21T17:19:38.477 回答
0

上面有一些很好的答案——我无意贬低它们。

在实现类型检查器方面 - 在 Haskell 中它更简单（尽管可以想象这可以移植到 Scheme）。

这是 Haskell中的简单类型检查器，它是简单类型化 Lambda 演算的实现：

type OType = ObjType (Fix ObjType)
type OEnvironment = Map TermIdentifier OType

check :: OEnvironment -> Term OType -> OType
check env (Var i) = case lookup i env of
                      Nothing -> error $ "Unbound variable " ++ i
                      Just v -> v
check env (App f p) = let t_f = check env f
                          t_p = check env p
                       in case t_f of
                            Fun (Fix t_p') (Fix r)
                              | t_p == t_p' -> r
                              | otherwise -> error "Parameter mismatch"
                            _ -> error "Applied a non-function"
check env (Lam i ty t) = let r = check (insert i ty env) t
                          in Fun (Fix ty) (Fix r)

这是Haskell 中简单类型 Lambda 演算的另一种实现：

import Control.Applicative ((<$), (<$>))
import Control.Monad (guard)
import Safe (atMay)

data Type
    = Base
    | Arrow Type Type
    deriving (Eq, Ord, Read, Show)

data Term
    = Const
    | Var Int -- deBruijn indexing; the nearest enclosing lambda binds Var 0
    | Lam Type Term
    | App Term Term
    deriving (Eq, Ord, Read, Show)

check :: [Type] -> Term -> Maybe Type
check env Const = return Base
check env (Var v) = atMay env v
check env (Lam ty tm) = Arrow ty <$> check (ty:env) tm
check env (App tm tm') = do
    Arrow i o <- check env tm
    i' <- check env tm'
    guard (i == i')
    return o

eval :: Term -> Term
eval (App tm tm') = case eval tm of
    Lam _ body -> eval (subst 0 tm' body)
eval v = v

subst :: Int -> Term -> Term -> Term
subst n tm Const = Const
subst n tm (Var m) = case compare m n of
    LT -> Var m
    EQ -> tm
    GT -> Var (m-1)
subst n tm (Lam ty body) = Lam ty (subst (n+1) tm body)
subst n tm (App tm' tm'') = App (subst n tm tm') (subst n tm tm'')

evalMay :: Term -> Maybe Term
evalMay tm = eval tm <$ check [] tm
于 2016-06-23T11:46:33.787 回答