[Haskell-cafe] Haskell and the Software design process

[Casey McCann]

On Tue, May 4, 2010 at 2:43 PM, Gregory Crosswhite
<gcross at phys.washington.edu> wrote:
> 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/