Что требуется для того, чтобы расширить реализацию нетипизированного лямбда-исчисления, чтобы охватить просто типизированное лямбда-исчисление?

Мэтт Майт говорит о реализации интерпретатора лямбда-исчисления в 7 строках схемы:

; 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)

Теперь это не просто типизированное лямбда-исчисление. В ядре Хаскелла есть Промежуточный язык, который сильно напоминает Систему F. Некоторые (в том числе Саймон Пейтон Джонс) назвали это реализацией лямбда-исчисления с простыми типами.

Мой вопрос: что требуется для расширения реализации нетипизированного лямбда-исчисления, чтобы охватить лямбда-исчисление простого типа?

Источник

3 ответа

Решение

Совершенно неясно, что вы спрашиваете, но я могу придумать пару правильных ответов:

  • Представление нужно будет изменить, чтобы приспособить аннотации типов к переменным, введенным лямбда-абстракциями.

  • В зависимости от вашего представления, может быть возможно представлять не правильно напечатанные термины. Если это так, вы захотите реализовать проверку типов.

  • Для оценки вам не нужно ничего менять в вашем LC-оценщике, кроме как игнорировать аннотации типов (в этом весь смысл удаления типа). Тем не менее, если вы пишете оценщик, который в основном evalUntyped . eraseTypesвам, возможно, будет сложнее доказать, что она полная, чем если бы вы написали сделанный на заказ evalTyped функция.

Источник

Простое типизированное лямбда-исчисление (STLC) просто добавляет средство проверки типов в систему, которую вы описываете. То есть вы можете думать об этом оценщике как о "системе времени выполнения" для STLC.

Боковой узел: аннотации типов обычно добавляются к языку, чтобы упростить работу средства проверки типов, но в этом нет необходимости.

Источник

Есть несколько превосходных ответов выше - и я не собираюсь отвлекать их.

С точки зрения реализации средства проверки типов - это проще в Haskell (хотя это, вероятно, может быть перенесено в Scheme).

Вот проверка простого типа в Haskell, которая является реализацией лямбда-исчисления с простым типом:

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:

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
Источник
Другие вопросы по тегам