如何在 Haskell Lambda 演算解释器中实现 Sum 类型语义规则？

Question

我正在 Haskell 中开发 lambda 演算解释器，我需要帮助实现总和类型的语义规则。下面是我的代码的简化版本，包含词法分析器、解释器和类型检查器模块。

Lexer.hs

module Lexer where 

import Data.Char 

data Ty = TBool
        | TNum
        | TFun Ty Ty 
        | TSum Ty Ty 
        deriving (Show, Eq)

data Expr = BTrue
          | BFalse
          | Num Int 
          | Add Expr Expr 
          | And Expr Expr 
          | If Expr Expr Expr 
          | Var String
          | Lam String Ty Expr 
          | App Expr Expr 
          | Paren Expr
          | Eq Expr Expr
          | Inl Expr 
          | Inr Expr
          | Case Expr Expr Expr
          deriving (Show, Eq)

data Token = TokenTrue 
           | TokenFalse 
           | TokenNum Int 
           | TokenAdd 
           | TokenAnd
           | TokenIf 
           | TokenThen
           | TokenElse 
           | TokenVar String 
           | TokenLam
           | TokenColon
           | TokenArrow 
           | TokenLParen
           | TokenRParen
           | TokenBoolean
           | TokenNumber
           | TokenEq
           | TokenInl
           | TokenInr
           | TokenCase
           | TokenBar
           | TokenOf
           deriving Show 

isToken :: Char -> Bool
isToken c = elem c "->&|="

lexer :: String -> [Token]
lexer [] = [] 
lexer ('+':cs) = TokenAdd : lexer cs 
lexer ('\\':cs) = TokenLam : lexer cs
lexer (':':cs) = TokenColon : lexer cs
lexer ('(':cs) = TokenLParen : lexer cs
lexer (')':cs) = TokenRParen : lexer cs
lexer (c:cs) | isSpace c = lexer cs 
             | isDigit c = lexNum (c:cs)
             | isAlpha c = lexKW (c:cs)
             | isToken c = lexSymbol (c:cs)
lexer _ = error "Lexical error: caracter inválido!"

lexNum :: String -> [Token]
lexNum cs = case span isDigit cs of 
              (num, rest) -> TokenNum (read num) : lexer rest 

lexKW :: String -> [Token]
lexKW cs = case span isAlpha cs of 
             ("true", rest)  -> TokenTrue : lexer rest 
             ("false", rest) -> TokenFalse : lexer rest 
             ("if", rest)    -> TokenIf : lexer rest 
             ("then", rest)  -> TokenThen : lexer rest 
             ("else", rest)  -> TokenElse : lexer rest 
             ("Bool", rest)  -> TokenBoolean : lexer rest 
             ("Number", rest)  -> TokenNumber : lexer rest 
             ("inl", rest) -> TokenInl : lexer rest
             ("inr", rest) -> TokenInr : lexer rest
             ("case", rest) -> TokenCase : lexer rest
             ("of", rest) -> TokenOf : lexer rest
             (var, rest)     -> TokenVar var : lexer rest 

lexSymbol :: String -> [Token]
lexSymbol cs = case span isToken cs of
                   ("->", rest) -> TokenArrow  : lexer rest
                   ("&&", rest) -> TokenAnd    : lexer rest
                   ("==", rest) -> TokenEq     : lexer rest
                   ("|", rest) -> TokenBar : lexer rest
                   _ -> error "Lexical error: símbolo inválido!"

解释器.hs

module Interpreter where

import Lexer

subst :: String -> Expr -> Expr -> Expr
subst x n b@(Var v) = if v == x then
                        n
                      else
                        b
subst x n (Lam v t b) = Lam v t (subst x n b)
subst x n (App e1 e2) = App (subst x n e1) (subst x n e2)
subst x n (Add e1 e2) = Add (subst x n e1) (subst x n e2)
subst x n (And e1 e2) = And (subst x n e1) (subst x n e2)
subst x n (If e e1 e2) = If (subst x n e) (subst x n e1) (subst x n e2)
subst x n (Paren e) = Paren (subst x n e)
subst x n (Eq e1 e2) = Eq (subst x n e1) (subst x n e2)
subst x n (Inl b) = Inl (subst x n b)
subst x n (Inr b) = Inr (subst x n b) 
subst x n (Case e1 e2 e3) = Case (subst x n e1)(subst x n e2)(subst x n e3)

subst x n e = e

isvalue :: Expr -> Bool
isvalue BTrue = True
isvalue BFalse = True
isvalue (Num _) = True
isvalue (Lam _ _ _) = True
isvalue (Inl _) = True
isvalue (Inr _) = True
isvalue (Case _ _ _) = True
isvalue _ = False

step :: Expr -> Maybe Expr
step (Add (Num n1) (Num n2)) = Just (Num (n1 + n2))
step (Add (Num n1) e2) = case step e2 of
                           Just e2' -> Just (Add (Num n1) e2')
                           _        -> Nothing
step (Add e1 e2) = case step e1 of
                     Just e1' -> Just (Add e1' e2)
                     _        -> Nothing
step (And BTrue e2) = Just e2
step (And BFalse _) = Just BFalse
step (And e1 e2) = case step e1 of
                     Just e1' -> Just (And e1' e2)
                     _        -> Nothing
step (If BTrue e1 _) = Just e1
step (If BFalse _ e2) = Just e2
step (If e e1 e2) = case step e of
                      Just e' -> Just (If e' e1 e2)
                      _       -> Nothing
step (App e1@(Lam x t b) e2) | isvalue e2 = Just (subst x e2 b)
                             | otherwise = case step e2 of
                                             Just e2' -> Just (App e1 e2')
                                             _        -> Nothing
step (App e1 e2) = case step e1 of
                     Just e1' -> Just (App e1' e2)
                     _        -> Nothing
step (Paren e) = Just e
step (Eq e1 e2) | isvalue e1 && isvalue e2 = if e1 == e2 then
                                               Just BTrue
                                             else
                                               Just BFalse
                | isvalue e1 = case step e2 of
                                 Just e2' -> Just (Eq e1 e2')
                                 _        -> Nothing
                | otherwise = case step e1 of
                                Just e1' -> Just (Eq e1' e2)
                                _        -> Nothing

step e = Just e

eval :: Expr -> Expr
eval e | isvalue e = e
       | otherwise = case step e of
                       Just e' -> eval e'
                       _       -> error "Interpreter error!"

类型检查器.hs

module TypeChecker where

import Lexer

type Ctx = [(String, Ty)]

typeof :: Ctx -> Expr -> Maybe Ty
typeof _ BTrue = Just TBool
typeof _ BFalse = Just TBool
typeof _ (Num _) = Just TNum
typeof ctx (Add e1 e2) = case (typeof ctx e1, typeof ctx e2) of
                           (Just TNum, Just TNum) -> Just TNum
                           _                       -> Nothing
typeof ctx (And e1 e2) = case (typeof ctx e1, typeof ctx  e2) of
                           (Just TBool, Just TBool) -> Just TBool
                           _                         -> Nothing
typeof ctx (If e e1 e2) =
    case typeof ctx e of
      Just TBool -> case (typeof ctx e1, typeof ctx e2) of
                      (Just t1, Just t2) -> if t1 == t2 then
                                              Just t1
                                            else
                                              Nothing
                      _                  -> Nothing
      _          -> Nothing
typeof ctx (Var v) = lookup v ctx
typeof ctx (Lam v t1 b) = let Just t2 = typeof ((v, t1):ctx) b
                            in Just (TFun t1 t2)
typeof ctx (App t1 t2) = case (typeof ctx t1, typeof ctx t2) of
                           (Just (TFun t11 t12), Just t2) -> if t11 == t2 then
                                                               Just t12
                                                             else
                                                               Nothing
                           _                              -> Nothing
typeof ctx (Eq e1 e2) = case (typeof ctx e1, typeof ctx e2) of
                          (Just t1, Just t2) -> if t1 == t2 then
                                                  Just TBool
                                                else
                                                  Nothing
                          _                  -> Nothing
typeof ctx (Paren e) = typeof ctx e

typecheck :: Expr -> Expr
typecheck e = case typeof [] e of
                Just _ -> e
                _      -> error "Type error"

我想将总和类型（Inl、Inr 和 Case）的语义规则添加到我的解释器和类型检查器中。您能指导我如何正确实现这些结构的语义规则吗？

这是我的具体问题：

1. 我应该如何扩展 isvalue、step 和 typeof 函数来处理 Inl、Inr 和 Case 表达式？
2. 替换函数 subst 需要进行哪些修改才能支持这些结构？

任何帮助或示例将不胜感激!!!!!!!!!!

Answer 1

我将提供一些提示。

isvalue (Inl _) = True
isvalue (Inr _) = True
isvalue (Case _ _ _) = True

这些都是错误的。例如，

Inr (Add (Num 1) (Num 3))

不是一个值。

Case ....

从来都不是一个值。

typeof (Inl ...)

无法合理定义。例如， 对于所有

typeof (Inl BTrue)

，

TSum TBool t

应该是

t

，这是没有意义的。处理这种多态类型是很棘手的。我建议您将“其他”类型添加到语法中，例如允许

Inl TInt BTrue

，使其具有类型

TSum TBool TInt

。

Case Expr Expr Expr

不忠实于您发布的语法，因为您忘记了两个分支中的绑定变量。考虑将

Case Expr String Expr String Expr

替换为

case e of inl x => e' | inr y => e''

。 （或者，您可以使用语法

case e (\x -> e) (\y -> e)

来保留

Case Expr Expr Expr

，但您需要根据您发布的规则调整打字规则。）

subst x n (Lam v t b) = Lam v t (subst x n b)

仅当

n

没有自由变量时才是正确的，例如一个值。你这么认为吗？否则我们需要留意捕获的变量。

subst x n (Inl b) = Inl (subst x n b)
subst x n (Inr b) = Inr (subst x n b) 

这看起来不错。

subst x n (Case e1 e2 e3) = Case (subst x n e1)(subst x n e2)(subst x n e3)

这应该适应上面给出的新的

Case

定义。对于

Lam

案例的相同评论也适用于此处。