Writing a Haskell program for typechecking programs written in an imperative programming language

Question

I am trying to write a program in Haskell to type check programs written in an imperative programming language.

Here is the abstract syntax:

---

    type Name = String

-- a program is a series (list) of variable declarations and a series (list) of statements.

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

-- a variable declaration is a type and a variable name

    type TypeEnv = (Type,Name)

-- a type is either "int" or "bool", or "int[]..[]" or "bool[]..[]"

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

-- a statement is either...

   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

-- an expression is either...

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

---

I do not need anyone to completely answer my question, but I would like to provide what I have so far, and if someone could point me in the right direction or let me know if I am doing it completely wrong, that would be very helpful.

The function to type check the program begins at typecheck. typecheck uses typecheckstmt to type check the first statement and typecheckstmtlist to typecheck the rest of the program. Then, these functions use typecheckexp to type check any expressions. Obviously, I have a very basic skeleton of an implementation. I just want to know if I am headed in the right direction, and if anyone has any pointers.

---

   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

---

I am also a little fuzzy on exactly what needs to be checked. Obviously if you are assigning and comparing variables/expressions, you want them to be the same type.

Any help would be much appreciated.

Answer 1

Since there isn't a specific question I'll just offer some general advice on the problem.

Looks like you're on the right track. Your approach is correct you need to walk your syntax tree and check each subexpression, failing if your types don't match.

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

At the toplevel you'll apply your expression level checker across all expressions and then and all the results together to get whether your program as a whole typechecks.

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

If your types are all declared up front and the TypeEnv is not altered as a result of traveresing the AST then this approach will work. If you are building up definitions as you walk the tree then consider wrapping your typechecker in a State monad.

Obviously if you are assigning and comparing variables/expressions,

Depending on your frontend language you'll need to decide whether to add explicit type declarations ( i.e. int a) for variables or whether you'll try and deduce them from context of the program, which is a separate task called type inference. If you have explicit declarations from the user then you can simply mechanically check the given types against the uses of the variable and determine if they match. Your types are all simple monotypes so this is easy as you can attach (derving Eq) to your Type and get type comparison.

Another case to consider is error reporting, with your given AST there is no position information attached so if you walk the tree and fail midways you'll have no way to tell the user what failed and where. If you're parsing the frontend language from a parser like Parsec you can tag each data type (Expr Pos) with the information when constructing the syntax tree.

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

For ease of use you might look into a generics library like Uniplate which will let you apply functions and traverse your AST without so much boilerplate. A contrived example to extract all nodes of a specific type might be:

{-# 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")))