Haskell中的Monadic类型检查器-Java 学习之路

我正在从BNFC开始在Haskell中编写解析器和类型检查器 . 类型检查器的主要功能实现如下：

typecheck :: Program -> Err ()
typecheck (PDefs ds) = do
    env  <- foldM (\env  (DFun typ id args _ _) -> 
               updateFun env id (argTypes args,typ) ) (emptyEnv) (ds)
    mapM_ (checkDef env) ds 
    where argTypes = map (\(ADecl _ typ _) -> typ)

其中 PDefs ， DFun 和 ADecl 是在语言的抽象语法中定义的代数数据类型的构造函数， checkDef 和 updateFun 是函数 . Program 是语法的"starting point" . 使用的monad是monad Err ：

data Err a = Ok a | Bad String
       deriving (Read, Show, Eq, Ord)

    instance Monad Err where
       return      = Ok
       fail        = Bad
       Ok a  >>= f = f a
       Bad s >>= f = Bad s

typechecker 函数在"main"模块中调用（在类型检查之前有词法和sintax分析）：

check :: String -> IO ()
    check s = do
               case pProgram (myLexer s) of
                  Bad err -> do
                          putStrLn "SYNTAX ERROR"
                          putStrLn err
                          exitFailure
                  Ok  tree -> do 
                          case typecheck tree of
                             Bad err -> do
                                 putStrLn "TYPE ERROR"
                                 putStrLn err
                                 exitFailure
                             Ok _ -> do
                                 putStrLn "\nParsing e checking ok!"
                                 showTree tree

（ tree 是解析器构建的抽象语法树）

如果作为输入传递的程序中存在类型错误，则类型检查器将返回错误，指出错误并且不会继续 . 有没有办法允许类型检查器在单次执行中列出输入中的所有错误？

1 回答

正如@ mb14的评论中所述，通常的方法包括做两件事：

首先，不要返回类型检查树或错误，而是准备始终返回类型检查树以及零或更多错误的日志 . 这可以通过 Writer monad轻松完成 .
其次，每当检测到错误时，记录错误，尝试通过假设类型检查的节点的某些有效类型来恢复，并继续进行类型检查 .

在这个简单的方案中，类型检查总是返回一个类型化的树 . 如果错误消息的日志为空，则类型检查已成功，并且键入的树有效 . 否则，类型检查已失败并出现给定的错误集，并且可以丢弃键入的树 . 在更复杂的方案中，您可以区分日志中的警告和错误，并且如果类型检查包含零个或多个警告但没有错误，则认为类型检查已成功 .

我已经在下面提供了一个完整的技术示例，用于非常简化的语法 . 它只返回顶级类型而不是类型化树，但这只是为了保持代码简单 - 返回类型检查树并不困难 . 使其适应你的语法的困难部分将是确定在发生错误时如何提前（即，提供什么样的有效类型），并且它将高度依赖于程序的细节 . 一些通用技术如下所示：

如果节点始终返回特定类型（例如，下面的 Len ），则始终假定该节点的类型，即使该节点未进行类型检查 .
如果节点组合兼容类型以确定其结果类型（例如，下面的 Plus 或BNF交替），那么当检测到类型不兼容时，请通过其第一个参数的类型确定节点的类型 .

无论如何，这是完整的例子：

import Control.Monad.Writer

-- grammar annotated with node ids ("line numbers")
type ID = String
data Exp = Num  ID Double         -- numeric literal
         | Str  ID String        -- string literal
         | Len  ID Exp           -- length of a string expression
         | Plus ID Exp Exp       -- sum of two numeric expressions
                                 -- or concat of two strings
-- expression types
data Type = NumT | StrT deriving (Show, Eq)

-- Expressions:
--    exp1 =    1 + len ("abc" + "def")
--    exp2 =    "abc" + len (3 + "def")
-- annotated with node ids
exp1, exp2 :: Exp
exp1 = Plus "T1" (Num "T2" 1)
                 (Len "T3" (Plus "T4" (Str "T5" "abc")
                                      (Str "T6" "def")))
exp2 = Plus "T1" (Str "T2" "abc")
                 (Len "T3" (Plus "T4" (Num "T5" 3)
                                      (Str "T6" "def")))
-- type check an expression
data Error = Error ID String deriving (Show)
type TC = Writer [Error]

typeCheck :: Exp -> TC Type
typeCheck (Num _ _) = return NumT
typeCheck (Str _ _) = return StrT
typeCheck (Len i e) = do
  t <- typeCheck e
  when (t /= StrT) $
    tell [Error i ("Len: applied to bad type " ++ show t)]
  return NumT  -- whether error or not, assume NumT
typeCheck (Plus i d e) = do
  s <- typeCheck d
  t <- typeCheck e
  when (s /= t) $
    tell [Error i ("Plus: incompatible types "
                   ++ show s ++ " and " ++ show t
                   ++ ", assuming " ++ show s ++ " result")]
  return s -- in case of error assume type of first arg

compile :: String -> Exp -> IO ()
compile progname e = do
  putStrLn $ "Running type check on " ++ progname ++ "..."
  let (t, errs) = runWriter (typeCheck e)
  case errs of
    [] -> putStrLn ("Success!  Program has type " ++ show t)
    _  -> putStr ("Errors:\n" ++ 
            unlines (map fmt errs) ++ "Type check failed.\n")
      where fmt (Error i s) = "   in term " ++ i ++ ", " ++ s

main :: IO ()
main = do compile "exp1" exp1
          compile "exp2" exp2

它生成输出：

Running type check on exp1...
Success!  Program has type NumT
Running type check on exp2...
Errors:
   in term T4, Plus: incompatible types NumT and StrT, assuming NumT result
   in term T3, Len: applied to bad type NumT
   in term T1, Plus: incompatible types StrT and NumT, assuming StrT result
Type check failed.

回复于 2024-04-28T03:10:23+08:00

Haskell中的Monadic类型检查器

1 回答

相关问题