User loginNavigation 
Type TheoryHigherorder module system of ML is actually possible in Haskell
A nice post from Oleg on the Haskell mailing list shows how to implement high order modules, and more specifically translucent applicative functors in idiomatic Haskell.
Thus different instantiations of the functor with respect to typecompatible arguments are typecompatible; and yet the functor hides the representation details behind the unbreakable abstraction barrier. The work is inspired by (our own) Ken Shan's work that can be found here. Oleg concludes, The example illustrates that Haskell already has a higherorder module language integrated with the core language and with the module checking being a part of the regular typechecking.
Eliminating Array Bound Checking through Nondependent types
Oleg posted this pertinent message on the Haskell mailing list. It's always nice to see cool examples such as this.
Having saiod that, I must also say that I agree with Conor McBride who wrote that anyone who would argue (and I'm not saying you do) that work to try to make more advanced type systems and stronger static guarantees more convenient and wellsupported is not necessary because it happens to be possible to bang out this or that example in Haskell as it stands if you think about it hard enough, is adopting the position of the ostrich. Making type systems more expressive is a worthy goal. You want them to remain decidable (i.e., static), of course. Can we at least agree on that? ;) TyPiCal: Typebased static analyzer for the PiCalculusTyPiCal is a typebased static analyzer for the picalculus. The current version of TyPiCal provides four kinds of program analyses or program transformations: lockfreedom analysis, deadlockfreedom analysis, uselesscode elimination, and information flow analysis. Type system is an ordinary type system extended so that channel types carry precise information about how each channel is used. This allows a type inferencer to obtain information about the behavior of a process. Wobbly typesWobbly types: type inference for generalised algebraic data types
Edit: Made the title into a hyperlink, as the "Postscript" link could easily get lost in a sea of blue text... Edit 2:Quoted the article with a plainol' <blockquote> instead. Better? By Bryn Keller at 20040719 16:19  Functional  Type Theory  7 comments  other blogs  10322 reads
ConstraintBased Type Inference for Guarded Algebraic Data Types
ConstraintBased Type Inference for Guarded Algebraic Data Types. Vincent Simonet and Francois Pottier.
Guarded algebraic data types subsume the concepts known in the literature as indexed types, guarded recursive datatype constructors, and firstclass phantom types, and are closely related to inductive types. They have the distinguishing feature that, when typechecking a function defined by cases, every branch may be checked under different typing assumptions. This mechanism allows exploiting the presence of dynamic tests in the code to produce extra static type information. We propose an extension of the constraintbased type system HM(X) with deep pattern matching, guarded algebraic data types, and polymorphic recursion. We prove that the type system is sound and that, provided recursive function definitions carry a type annotation, type inference may be reduced to constraint solving. Then, because solving arbitrary constraints is expensive, we further restrict the form of type annotations and prove that this allows producing socalled tractable constraints. Last, in the specific setting of equality, we explain how to solve tractable constraints. To the best of our knowledge, this is the first generic and comprehensive account of type inference in the presence of guarded algebraic data types. Seems rather interesting. 
Browse archivesActive forum topicsNew forum topics

Recent comments
1 hour 17 min ago
2 weeks 2 days ago
2 weeks 2 days ago
3 weeks 3 days ago
3 weeks 3 days ago
3 weeks 3 days ago
3 weeks 3 days ago
3 weeks 3 days ago
4 weeks 2 days ago
4 weeks 3 days ago