[Haskell-cafe] Type checking with Haskell

[Stefan O'Rear]

On Thu, Apr 12, 2007 at 01:04:13PM +0100, Joel Reymont wrote:
> Folks,
> 
> The ghc/compiler/typecheck directory holds a rather large body of  
> code and quick browsing through did not produce any insight.
> 
> How do you implement type checking in haskell?
> 
> Assume I have an Expr type with a constructor per type and functions  
> can take lists of expressions. Do I create a function taking an Expr,  
> pattern-matching on appropriate constructor and returning True on a  
> match and False otherwise?

The Glasgow Haskell typechecker is big not because type checking is
hard, but because GHC Haskell is a very big language.  Also, GHC runs
typechecking *before* desugaring, apparently thinking error messages
are more important than programmer sanity :)

A typechecker for a simpler language can be implemented quite easily:

--- Simply typed lambda calculus

data Typ = Int | Real | Bool | Fn Typ Typ
data Exp = Lam Typ Exp | Var Int | App Exp Exp

typeCheck' :: [Typ] -> Exp -> Maybe Typ
typeCheck' cx (Lam ty bd) = fmap (Fn ty) (typeCheck' (ty:cx) bd)
typeCheck' cx (Var i)     = Just (cx !! i)
typeCheck' cx (App fn vl) = do Fn at rt <- typeCheck' cx fn
                               pt       <- typeCheck' cx vl
                               guard (at == pt)
                               return rt

Your problem, as I understand it, is even simpler than most since
there are no higher order functions and no arguments.

---

data Typ = Real | Int | Bool | String

tc2 a b ta tb tr | typeCheck a == ta && typeCheck b == tb = Just tr
                 | otherwise                              = Nothing

typeCheck :: Exp -> Maybe Typ
typeCheck (IAdd a b) = tc2 a b Int Int Int
...

(That said, it would probably be better to fuse parsing and type
checking in this case so that you do not need to track source
positions.)

Stefan