## User login## Navigation |
## Type Theory## Combining lazy and eager evaluation of termsIn an attempt to combine some of the benefits of lazy and eager evaluation, I have implemented a language with an evaluation strategy which is strict with respect to divergence, but performs lazy evaluation on certain intermediate subterms to allow a more expressive use of recursion. Tim Sweeney started this interesting Types-list thread. A summary of the responses he receieved is here. ## Higher-order 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 type-compatible arguments are type-compatible; 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 higher-order module language integrated with the core language and with the module checking being a part of the regular typechecking.
## Eliminating Array Bound Checking through Non-dependent 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 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: Type-based static analyzer for the Pi-CalculusTyPiCal is a type-based static analyzer for the pi-calculus. The current version of TyPiCal provides four kinds of program analyses or program transformations: lock-freedom analysis, deadlock-freedom analysis, useless-code 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 types## Wobbly types: type inference for generalised algebraic data types
By Bryn Keller at 2004-07-19 16:19 | Functional | Type Theory | 7 comments | other blogs | 8603 reads
## Constraint-Based Type Inference for Guarded Algebraic Data Types
Constraint-Based Type Inference for Guarded Algebraic Data Types. Vincent Simonet and Francois Pottier.
Seems rather interesting. |
## Browse archives## Active forum topics |

## Recent comments

3 days 10 hours ago

3 days 10 hours ago

6 days 5 hours ago

1 week 1 day ago

1 week 2 days ago

1 week 2 days ago

1 week 2 days ago

1 week 5 days ago

1 week 5 days ago

1 week 6 days ago