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/
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
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/
I feel I should set aside a Friday of every week just to read the Haskell papers :-). After skimming through "Typing Haskell in Haskell" I have a couple of questions... Are type constructors (TyCon) applicable to Haskell only? Mine is a Pascal-like language. How would I type Pascal functions as opposed to Haskell ones? It seems that the approach is the same and I still need TyCon "(->)". Thanks, Joel -- http://wagerlabs.com/
On Apr 12, 2007, at 14:37 , Joel Reymont wrote:
I feel I should set aside a Friday of every week just to read the Haskell papers :-).
After skimming through "Typing Haskell in Haskell" I have a couple of questions...
Are type constructors (TyCon) applicable to Haskell only? Mine is a Pascal-like language.
How would I type Pascal functions as opposed to Haskell ones? It seems that the approach is the same and I still need TyCon "(->)".
Thanks, Joel
Here are some lecture notes about implementing type checking for an imperative language from a programming languages course: http://www.cs.chalmers.se/Cs/Grundutb/Kurser/progs/current/lectures/ proglang-08.html /Björn
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: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe- bounces@haskell.org] 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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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
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/
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/
On 4/12/07, Joel Reymont
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
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?
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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@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/
participants (8)
-
Bas van Dijk -
Bernie Pope -
Bjorn Bringert -
Derek Elkins -
Joel Reymont -
Lennart Augustsson -
Stefan Holdermans -
Stefan O'Rear