Monadic type checker in Haskell

Question

I am writing parser and type checking in Haskell starting with BNFC. The main type checking function 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 constructs of algebraic data types defined in the abstract language syntax, and checkDef and updateFun are functions. Program is the starting point of grammar. Monad used Err monad:

  data Err a = Ok a | Bad String deriving (Read, Show, Eq, Ord) instance Monad Err where return = Ok fail = Bad Ok a >>= f = fa Bad s >>= f = Bad s 

The typechecker function typechecker called in the "main" module (where there is lexical and parsing before type checking):

  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 an abstract construction of a syntax tree using a parser)

If the program passed as input has a type error, then the type checking function returns an error indicating that it is not, and it does not continue. Is there a way to allow type checking to list all errors in the input file in one run?

Answer 1

As usual in @ mb14's comments, the usual method involves doing two things:

• First, instead of returning a type-checking tree or an error, be prepared to always return a type-checking tree along with a log with zero or more errors. This is easy to accomplish with Monad Writer .
• Secondly, whenever an error is detected, write down the error, try to recover, assuming that the valid type is using a valid type, and continue with the type check.

In this simple scheme, type checking always returns a typed tree. If the error message log is empty, the type check was successful and the entered tree is valid. Otherwise, the type check completed with the given set of errors, and the typed tree can be discarded. In a more complex scheme, you can distinguish between warnings and errors in your log and consider type checking successful if it contains zero or more warnings, but without errors.

I have included a complete example of the technique below for a very simplified grammar. It returns only the top-level type instead of the typed tree, but this is just to keep the code simple - returning a tree checked by type is not difficult. The hard part in adapting to your grammar will determine how to move forward (that is, what is the actual type for delivery) when an error occurs, and it will greatly depend on the details of your program. The following are some common methods:

• If node always returns a specific type (for example, Len below), always assume that type for node, even if node does not check the type.
• If a node combines compatible types to determine its type of result (for example, Plus below or BNF alternation), then when type incompatibility is detected, take the type of node, which will determine the type of its first argument.

Anyway, here is a 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 ie) = 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 ide) = 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 is) = " 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.