On Tue, May 4, 2010 at 2:43 PM, Gregory Crosswhite
I definitely like that idea. :-) Is this similar to the notion of dependent types?
That's where things tend to wind up eventually, yes. Although, with Haskell as it stands, a great deal of unused information is already present outside the type system, sufficient to automatically prove a range of "easy" properties of code. For instance, consider Neil Mitchell's Catch tool[0], which seems to handle things like the "secondElement" function discussed. Of course, actually writing such a checker is not so easy, and encoding the results of something like Catch in the type system leads to either convoluted type metaprogramming hacks or to new extensions creeping slowly toward full dependent types. - C. [0] http://community.haskell.org/~ndm/catch/