haskell - 编写 Haskell 程序来对用命令式编程语言编写的程序进行类型检查

Question

我正在尝试用 Haskell 编写一个程序来类型检查用命令式编程语言编写的程序。

这是抽象语法:

---

    type Name = String

--程序是一系列(列表)变量声明和一系列(列表)语句。

    type Prog = ([TypeEnv],[Stmt])

--变量声明是类型和变量名

    type TypeEnv = (Type,Name)

-- 类型可以是“int”或“bool”，或者“int[]..[]”或“bool[]..[]”

   data Type = BaseType BT | ArrayType BT Int deriving Show
   data BT = TyInt | TyBool deriving Show

-- 语句可以是...

   data Stmt =
   Assign Name Exp                -- ...assignment (<name> := <exp>;)
   | If Exp [Stmt] [Stmt]           -- ...if-then-else (if <bexp> { <stmt>* } else { <stmt>* })
   | While Exp [Stmt]               -- ...a while-loop (while <bexp> { <stmt>*> })
   | Let Name Exp [Stmt]            -- ...let bindings (let <name>=<exp> in { <stmt> *}) 
   | LetArray Name [Exp] Exp [Stmt] -- ...let-array binding (letarray <name> [ <exp> ] .. [ <exp> ] := <exp> in { <stmt>* })
   | Case Exp [(Int,[Stmt])]        -- ...a case statements
   | For Name Exp Exp [Stmt]        -- ...a for-loop
   | ArrayAssign Name [Exp] Exp       -- ...or array assignment (<name> [ <exp> ] .. [ <exp> ] := <exp>;)
   deriving Show

-- 表达式可以是...

data Exp =
Add Exp Exp             -- ...addition (<exp> + <exp>)
| Sub Exp Exp             -- ...subtract (<exp> - <exp>)
| Mul Exp Exp             -- ...multiplication (<exp> * <exp>)
| Neg Exp                 -- ...negation (-<exp>)
| Var Name                -- ...a variable (<name>)
| LitInt Int              -- ...an integer literal (e.g. 3, 0, 42, 1999)
| VarArray Name [Exp]     -- ...or an array lookup (<name> [ <exp> ])
| IsEq Exp Exp            -- ...test for equality (<exp> == <exp>)
| IsNEq Exp Exp           -- ...test for inequality (<exp> != <exp>)
| IsGT Exp Exp            -- ...test for greater-than (<exp> > <exp>)
| IsLT Exp Exp            -- ...test for less-than (<exp> < <exp>)
| IsGTE Exp Exp           -- ...test for greater-or-equal (<exp> >= <exp>)
| IsLTE Exp Exp           -- ...test for less-or-equal (<exp> <= <exp>)
| And Exp Exp             -- ...boolean and (<bexp> && <bexp>)
| Or Exp Exp              -- ...boolean or (<bexp> || <bexp>)
| Not Exp                 -- ...boolean negation (!<bexp>)
| LitBool Bool            -- ... or a boolean literal (true or false)
deriving Show

---

我不需要任何人完全回答我的问题，但我想提供到目前为止我所拥有的内容，如果有人可以指出我正确的方向，或者让我知道我是否完全错误地做，那就会非常有帮助。

对程序进行类型检查的函数从 typecheck 开始。 typecheck 使用 typecheckstmt 对第一个语句进行类型检查，并使用 typecheckstmtlist 对程序的其余部分进行类型检查。然后，这些函数使用 typecheckexp 对任何表达式进行类型检查。显然，我有一个非常基本的实现框架。我只是想知道我是否朝着正确的方向前进，以及是否有人有任何指示。

---

   typecheck :: Prog -> Bool
   typecheck _ = True
   typecheck (types, x: xs) = (typecheckstmt types x) && (typecheckstmtlist types xs)

   typecheckstmt :: [TypeEnv] -> Stmt -> Bool
   typecheckstmt _ _ = True
   typecheckstmt types (Assign x e) = if checkequaltypes x e
                  then True && typecheckexp types e
                  else False
   typecheckstmt types (If e stmtlst1 stmtlst2) = typecheckexp types e 
                       && typecheckstmtlist types stmtlst1 
                       && typecheckstmtlist types stmtlst2
   typecheckstmt types (While e stmtlst) = typecheckexp types e 
                    && typecheckstmtlist types stmtlst
   typecheckstmt types (Let x e stmtlst) = if checkequaltype types x e
                       then True && typecheckexp types e
                             && typecheckstmtlist types stmtlst
                       else False
   typecheckstmt types (LetArray x es e2 stmtlst) = 
   typecheckstmt types (Case e cases) = 
   typecheckstmt types (For x e1 e2 stmtlst) = if checkequaltype types x e1 
                           && checkequaltype types x e2 
                           then True && typecheckstmtlist stmtlst 
                           else False
   typecheckstmt types (ArrayAssign x es e2) = 

   typecheckstmtlist :: [TypeEnv] -> [Stmt] -> Bool
   typecheckstmtlist _ _ = True
   typecheckstmtlist types [x] = typecheckstmt types x
   typecheckstmtlist types x:xs = typecheckstmt types x && typecheckstmtlist types xs


   typecheckexp :: [TypeEnv] -> Exp -> Bool
   typecheckexp types (Add e1 e2) = 
   typecheckexp types (Sub e1 e2) =
   typecheckexp types (Mul e1 e2) =
   typecheckexp types (Neg e1) =
   typecheckexp types (Var x) =
   typecheckexp types (LitInt i) = 
   typecheckexp types (VarArray x explist) =
   typecheckexp types (IsEq e1 e2) = 
   typecheckexp types (IsNEq e1 e2) = 
   typecheckexp types (IsGT e1 e2) = 
   typecheckexp types (IsLT e1 e2) = 
   typecheckexp types (IsGTE e1 e2) =
   typecheckexp types (IsLTE e1 e2) = 
   typecheckexp types (And e1 e2) =
   typecheckexp types (Or e1 e2) = 
   typecheckexp types (Not e) = 
   typecheckexp types (LitBool Bool) = 

   typecheckexplist :: [TypeEnv] -> [Exp] -> Bool
   typecheckexplist _ _ = True
   typecheckexplist types [x] = typecheckexp types x
   typecheckexplist types x:xs = typecheckexp types x && typecheckexplist types xs

   checkequaltype :: [TypeEnv] -> Name -> Exp -> Bool
   checkequaltype types x e = getTypeOfVar types x && getTypeOfExp types e

   getTypeOfVar :: [TypeEnv] -> Name -> Type

   getTypeOfExp :: [TypeEnv] -> Exp -> Type

---

我对到底需要检查什么也有点模糊。显然，如果您要分配和比较变量/表达式，您希望它们具有相同的类型。

任何帮助将不胜感激。

Answer 1

由于没有具体问题，我只会就该问题提供一些一般性建议。

看来您走在正确的道路上。您的方法是正确的，您需要遍历语法树并检查每个子表达式，如果您的类型不匹配，则会失败。

typecheckexp :: [TypeEnv] -> Exp -> Bool
typecheckexp types (Add e1 e2) = 
  case (te1, te2) of
    (Just TyInt, Just TyInt) -> True
     _ -> False
  where
    te1 = getTypeOfExp e1
    te2 = getTypeOfExp e2

在顶层，您将在所有表达式中应用表达式级别检查器，然后和将所有结果放在一起，以确定您的程序是否作为一个整体进行类型检查。

typecheckexplist :: [TypeEnv] -> [Exp] -> Bool
typecheckexplist env stmts = and (map (typecheckexp env) stmts)

如果您的类型都是预先声明的，并且 TypeEnv 没有因遍历 AST 而改变，那么这种方法将起作用。如果您在遍历树时构建定义，请考虑将类型检查器包装在 State monad 中。 .

Obviously if you are assigning and comparing variables/expressions,

根据您的前端语言，您需要决定是否为变量添加显式类型声明(即 int a)，或者是否尝试从程序的上下文中推断它们，这是一个称为类型推断的单独任务。如果您有来自用户的显式声明，那么您可以简单地根据变量的使用来机械地检查给定类型并确定它们是否匹配。您的类型都是简单的单型，因此这很容易，因为您可以将 (derving Eq) 附加到您的 Type 并进行类型比较。

另一个需要考虑的情况是错误报告，对于给定的 AST，没有附加位置信息，因此如果您遍历树并中途失败，您将无法告诉用户失败的原因和位置。如果您从 Parsec 等解析器解析前端语言，则可以在构建语法树时使用信息标记每个数据类型 (Expr Pos)。

data Expr t = Add t (Expr t) (Expr t) | ... 
data Pos = Pos { line :: Integer , col :: Integer }

为了便于使用，您可以考虑使用像 Uniplate 这样的泛型库，它可以让您应用函数并遍历 AST，而无需太多样板文件。提取特定类型的所有节点的人为示例可能是:

{-# LANGUAGE DeriveDataTypeable #-}
module Expr where

import Data.Data
import Data.Typeable
import Data.Generics.Uniplate.Data

data Expr = Val String
          | Add Expr Expr
          | Sub Expr Expr
          | Div Expr Expr
          | Mul Expr Expr
          | Neg Expr
          deriving (Show, Eq, Data, Typeable)

vars :: Expr -> [String]
vars ex = [i | Val i <- universe ex]

test :: [String]
test = vars (Add (Val "a") (Mul (Val "b") (Val "c")))