Haskell 中的 Monadic 类型检查器
Monadic type checker in Haskell
我正在 Haskell 从 BNFC 开始编写解析器和类型检查器。类型检查器的主要功能实现如下:
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"模块中被调用(在类型检查之前有词法和语法分析):
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
是解析器构建的抽象语法树)
如果作为输入传递给类型检查程序的程序中存在类型错误,returns 会出现一个错误,说明错误并且不会继续。有没有办法让类型检查器在一次执行中列出输入中的所有错误?
正如@mb14 的评论中所涵盖的那样,通常的方法包括做两件事:
- 首先,不要 return 将 类型检查树 或 错误,准备好 always return 类型检查树以及零个或多个错误的日志。这很容易用
Writer
monad 完成。
- 其次,每当检测到错误时,记录错误,尝试通过假定正在接受类型检查的节点的某些有效类型来恢复,并继续进行类型检查。
在这个简单的方案中,类型检查总是 return 类型树。如果错误消息日志为空,则类型检查成功,类型树有效。否则,类型检查因给定的错误集而失败,可以丢弃类型化的树。在更复杂的方案中,您可以区分日志中的警告和错误,如果包含零个或多个警告但没有错误,则认为类型检查已成功。
我在下面包含了一个非常简化的语法的完整技术示例。它只是 return 顶级类型而不是类型树,但这只是为了保持代码简单 -- return 类型检查树并不困难。使它适应你的语法的困难部分将是确定发生错误时如何向前推进(即,提供什么有效类型),这将在很大程度上取决于你的程序的细节。下面说明了一些通用技术:
- 如果节点总是 return 特定类型(例如下面的
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.
我正在 Haskell 从 BNFC 开始编写解析器和类型检查器。类型检查器的主要功能实现如下:
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"模块中被调用(在类型检查之前有词法和语法分析):
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
是解析器构建的抽象语法树)
如果作为输入传递给类型检查程序的程序中存在类型错误,returns 会出现一个错误,说明错误并且不会继续。有没有办法让类型检查器在一次执行中列出输入中的所有错误?
正如@mb14 的评论中所涵盖的那样,通常的方法包括做两件事:
- 首先,不要 return 将 类型检查树 或 错误,准备好 always return 类型检查树以及零个或多个错误的日志。这很容易用
Writer
monad 完成。 - 其次,每当检测到错误时,记录错误,尝试通过假定正在接受类型检查的节点的某些有效类型来恢复,并继续进行类型检查。
在这个简单的方案中,类型检查总是 return 类型树。如果错误消息日志为空,则类型检查成功,类型树有效。否则,类型检查因给定的错误集而失败,可以丢弃类型化的树。在更复杂的方案中,您可以区分日志中的警告和错误,如果包含零个或多个警告但没有错误,则认为类型检查已成功。
我在下面包含了一个非常简化的语法的完整技术示例。它只是 return 顶级类型而不是类型树,但这只是为了保持代码简单 -- return 类型检查树并不困难。使它适应你的语法的困难部分将是确定发生错误时如何向前推进(即,提供什么有效类型),这将在很大程度上取决于你的程序的细节。下面说明了一些通用技术:
- 如果节点总是 return 特定类型(例如下面的
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.