[Haskell-cafe] Type checking with Haskell

[Derek Elkins]

Stefan O'Rear wrote:
> 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 

Just for interest:

Chapter 31 of Shriram Krishnamurthi's "Programming Languages: Application and 
Interpretation" has an interesting perspective on Haskell style polymorphism 
http://www.cs.brown.edu/~sk/Publications/Books/ProgLangs/