Monadic type checker in Haskell
I'm writing a parser and a type checker in Haskell starting from BNFC. The main function of the type checker is implemented as follows:
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)
where PDefs , DFun , and ADecl are constructrors of algebraic data types defined in the abstract syntax of the language and checkDef and updateFun are functions. Program is the "starting point" of the grammar. The monad used is the 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
The typechecker function is called in the "main" module (where before the type check there are the lexical and the sintax analysis):
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 is the abstract syntax tree build by the parser)
If there's a type error in the program passed as input the type checker returns an error saying what is wrong and it doesn't continue. Is there a way to allow the type checker to list all the errors in the input in a single execution?
As mostly covered in @mb14's comments, the usual method involves doing two things:
Writer monad. In this simple scheme, the type checking always returns a typed tree. If the log of error messages is empty, the type check has succeeded, and the typed tree is valid. Otherwise, the type check has failed with the given set of errors, and the typed tree can be discarded. In a more complex scheme, you could differentiate between warnings and errors in your log, and consider the type checking to have succeeded if it contains zero or more warnings, but no errors.
I've included a complete example of the technique below for a very simplified grammar. It only returns the top-level type instead of the typed tree, but this is just to keep the code simple -- returning a type-checked tree is not difficult. The hard part in adapting it to your grammar will be determining how to forge ahead (ie, what valid type to supply) when an error occurs, and it will be highly dependent on the details of your program. Some general techniques are illustrated below:
Len below), always assume that type for the node, even if the node doesn't type-check. Plus below, or a BNF alternation), then when a type incompatibility is detected, take the type of the node to be determined by the type of its first argument. Anyway, here is the complete example:
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
It generates the output:
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中生成一个独特的值