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

问题背景 #

我正在开发基于Haskell的Lambda演算解释器，需要为和类型实现语义规则，目前已有Lexer、Interpreter、TypeChecker模块的简化代码。需要为Inl、Inr及Case表达式添加语义规则，解决以下两个核心问题：

1. 扩展isvalue、step和typeof函数处理和类型相关表达式 #

1.1 扩展isvalue判断值 #

和类型的注入式构造器Inl/Inr包裹的表达式是值时，整个构造式就是值。直接在isvalue的模式匹配中添加分支：

isvalue :: Expr -> Bool
isvalue (Var _) = True
isvalue (Lam _ _) = True
-- 新增和类型值判断
isvalue (Inl e) = isvalue e
isvalue (Inr e) = isvalue e
-- 其他原有分支保持不变

1.2 扩展step实现求值步骤 #

分三类情况处理：

• 先求值构造器内部的表达式：如果Inl/Inr包裹的表达式还不是值，先步进求值内部：

  step :: Expr -> Expr
  -- 新增Inl/Inr内部求值
  step (Inl e) | not (isvalue e) = Inl (step e)
  step (Inr e) | not (isvalue e) = Inr (step e)
  

• Case表达式的步进规则：
  1. 先求值被检查的表达式（scrutinee），直到它成为值：

     step (Case e e1 e2) | not (isvalue e) = Case (step e) e1 e2
     

  2. 当scrutinee是Inl v时，将左分支lambda的绑定变量替换为v，得到求值结果：

     step (Case (Inl v) (Lam x e1) _) = subst x v e1
     

  3. 当scrutinee是Inr v时，同理处理右分支：

     step (Case (Inr v) _ (Lam x e2)) = subst x v e2
     

• 原有step的其他分支（如lambda应用等）保持不变。

1.3 扩展typeof实现类型检查 #

首先需要在类型定义中添加和类型的表示：

data Ty = VarTy String | FunTy Ty Ty | SumType Ty Ty -- 新增SumType

然后扩展typeof函数：

• Inl的类型检查：假设Inl携带目标和类型（避免隐式推导的歧义），检查内部表达式类型匹配和类型的左分支：

  typeof :: Context -> Expr -> Either String Ty
  typeof ctx (Inl sumTy e) = do
    tyE <- typeof ctx e
    case sumTy of
      SumType tyL tyR -> if tyE == tyL then return sumTy else throwError "Inl表达式类型与和类型左分支不匹配"
      _ -> throwError "Inl的目标类型不是和类型"
  

• Inr的类型检查：逻辑和Inl对称：

  typeof ctx (Inr sumTy e) = do
    tyE <- typeof ctx e
    case sumTy of
      SumType tyL tyR -> if tyE == tyR then return sumTy else throwError "Inr表达式类型与和类型右分支不匹配"
      _ -> throwError "Inr的目标类型不是和类型"
  

• Case的类型检查：验证scrutinee是和类型，且两个分支都是接收对应分支类型、返回相同结果类型的lambda：

  typeof ctx (Case e e1 e2) = do
    tyScrut <- typeof ctx e
    case tyScrut of
      SumType tyL tyR -> do
        -- 检查左分支类型：接收tyL，返回tyRes
        ty1 <- typeof ctx e1
        case ty1 of
          FunTy tyL tyRes -> do
            -- 检查右分支类型：接收tyR，返回相同的tyRes
            ty2 <- typeof ctx e2
            case ty2 of
              FunTy tyR tyRes' -> if tyRes == tyRes' then return tyRes else throwError "Case两个分支返回类型不一致"
              _ -> throwError "Case右分支不是函数类型"
          _ -> throwError "Case左分支不是函数类型"
      _ -> throwError "Case的被检查表达式不是和类型"
  

2. 修改subst函数支持和类型构造 #

subst需要递归遍历所有和类型相关的表达式节点，替换其中的变量，同时注意避免lambda的变量捕获（原有lambda分支的处理逻辑保持不变）：

subst :: String -> Expr -> Expr -> Expr
subst x v (Var y) | x == y = v
                  | otherwise = Var y
subst x v (Lam y e) | x == y = Lam y e -- 变量捕获，不替换
                    | otherwise = Lam y (subst x v e) -- 递归替换内部
-- 新增和类型相关的替换分支
subst x v (Inl sumTy e) = Inl sumTy (subst x v e)
subst x v (Inr sumTy e) = Inr sumTy (subst x v e)
subst x v (Case e e1 e2) = Case (subst x v e) (subst x v e1) (subst x v e2)
-- 其他原有表达式类型的替换分支保持不变

内容的提问来源于stack exchange，提问作者Narcisismo