I'm not knowledgeable enough in type systems to understand the paper, therefore I do not know if this email answers anything about your "request for comments".
For what I understand of the current possibilities of GHC, being able to use types for ensuring the axioms of algebra (groups, rings and fields) would be a great extension. The vector space package on hackage looks like a proof-of-concept of the possibilities of GHC's type system, which is obviously not suitable for production code. Such a typeclass (or whatever you call it) replacing Num, Real, etc. would be a good thing, in particular for eliminating fortan and matlab from the math laboratories ;-) As a former OCaml programmer, *the* thing that I miss is the exception system. I know about the challenge of keeping purity, but a type system redesign could be an opportunity to change this (or I did not understand anything, in this case please excuse me !). Cheers, Pierre-Etienne El 14/05/2010, a las 08:59, Simon Peyton-Jones escribió: > Friends > > Many of you will know that I've been muttering about re-engineering GHC's > type inference engine for some time now. Dimitrios, Tom, Martin and I have > just completed an epic paper describing the Glorious New Framework that forms > the substance of the above mutterings: > http://haskell.org/haskellwiki/Simonpj/Talk:OutsideIn > > We'd love comments and feedback. Dimitrios and I plan to roll up our sleeves > and implement it in June. > > Simon > > Modular type inference with local assumptions: OutsideIn(X) > > Abstract. Advanced type system features, such as GADTs, type classes, and > type families have have proven to be invaluable language extensions for > ensuring data invariants and program correctness among others. Unfortunately, > they pose a tough problem for type inference, because they introduce local > type assumptions. > > In this article we present a novel constraint-based type inference approach > for local type assumptions. Our system, called OutsideIn(X), is parameterised > over the particular underlying constraint domain X, in the same way as HM(X). > This stratification allows us to use a common metatheory and inference > algorithm. > > Going beyond the general framework, we also give a particular constraint > solver for X = type classes + GADTs + type families, a non-trivial challenge > in its own right. > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
