[Haskell-cafe] Modular type inference

[Pierre-Etienne Meunier]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe