Re: [Haskell-cafe] Type checking with Haskell
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 [EMAIL PROTECTED] 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/ ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking with Haskell
Joel, How do you implement type checking in haskell? You might want to check out Typing Haskell in Haskell [1] by Mark P. Jones. Cheers, Stefan [1] Jones, Mark P. Typing Haskell in Haskell. In Erik Meijer, editor, Proceedings of the 1999 Haskell Workshop, Friday October 9th, 1999, Paris, France. 1999. The proceedings of the workshop have been published as a technical report (UU- CS-1999-28) at Utrecht University. http://www.cs.uu.nl/research/ techreps/UU-CS-1999-28.html ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking with Haskell
On Apr 12, 2007, at 1:07 PM, Stefan Holdermans wrote: You might want to check out Typing Haskell in Haskell [1] by Mark P. Jones. Must be _the_ paper as Don suggested it as well. I also looked at my copy of Andrew Appel's compilers in ML book and realized that I should be going about it differently than I thought, i.e. figuring out and returning the type of an expression rather than matching constructors. Oh, well. Thanks, Joel -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Type checking with Haskell
Hi Joel, You may like to check out my mini-interpreter called (cheekily) baskell: http://www.cs.mu.oz.au/~bjpop/code.html It has type inference, and it is pretty straightforward. I wrote it for teaching purposes. First, I pass over the AST and generate a set of typing constraints. They are just equality constraints. Then I solve the constraints. Couldn't be much simpler than that. Mind you, the input language is pretty minimal (no type classes etcetera). Cheers, Bernie. -Original Message- From: [EMAIL PROTECTED] [mailto:haskell-cafe- [EMAIL PROTECTED] On Behalf Of Joel Reymont Sent: 12 April 2007 13:04 To: Haskell Cafe Subject: [Haskell-cafe] Type checking with Haskell 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? Thanks, Joel -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking with Haskell
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 [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking with Haskell
Thanks Stefan! On Apr 12, 2007, at 3:00 PM, Stefan O'Rear wrote: Your problem, as I understand it, is even simpler than most since there are no higher order functions and no arguments. I do have functions and arguments but I don't have HOF. (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.) I'm not sure how to do this, quite honestly. The language is dynamically typed so I have to infer variable types from their usage, function return types from what is assigned to the function name (last assignment in program, Fun = xxx). I also have to infer if variables are of a series type by checking if any references are made to the previous values of those variables. I don't think it's possible to fuse type checking with parsing here. -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking with Haskell
On Apr 12, 2007, at 3:00 PM, Stefan O'Rear wrote: Also, GHC runs typechecking *before* desugaring, apparently thinking error messages are more important than programmer sanity :) What would be the benefit of running type checking after desugaring? -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking with Haskell
On 4/12/07, Joel Reymont [EMAIL PROTECTED] wrote: What would be the benefit of running type checking after desugaring? After desugaring, the program is written in a much more simple language (GHC Core). Type checking a desugared program is much easier because the type checker has to deal with much less language constructs than in the original program. The disadvantage is that after desugaring a lot of the original program is lost so that the type checker can't give an error message that exactly describes the location and reason of the error. Bas van Dijk ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking with Haskell
It's so much easier to write the type checker because it's only a few constructs left in the language. But from a user's perspective it's a really bad idea. -- Lennart On Apr 12, 2007, at 15:25 , Joel Reymont wrote: On Apr 12, 2007, at 3:00 PM, Stefan O'Rear wrote: Also, GHC runs typechecking *before* desugaring, apparently thinking error messages are more important than programmer sanity :) What would be the benefit of running type checking after desugaring? -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
