(Succ Haskell') `and` $ dependent types

[Vivian McPhail]

Hello,

As the authors point out [1], coal-face time needs to be expended before
real world adoption of Dependently-Typed functional programming.  But let's
get the ball rolling.  They say that haskell programmers are normally averse
to dependent types.  Is this true?  It seems to me that one of the appeals
of Haskell is the ability to program in a "prove perfect, write once"
(elegant) style.  Is not dependent typing a good move towards this goal?.
It addresses a problem [2] with which we, in our everyday common
inter-hominem usage, can deal -- with which (ideal) Haskell should deal.

While the major Haskell implementations would require a substantial
overhaul, the change at the syntactic level appears to be minimal.  There
also needs to be advance with respect to programmer development (automatic
edit-time inference of (some) types). What are peoples' thoughts on adding
dependent types to haskell as a non-incremental evolutionary step?  Does the
haskell community want to stick with conservative additions to Haskell and a
static base, or does the haskell community want to stay in step with the
best theoretical developments?

Vivian

[1] http://www.informatik.uni-bonn.de/~loeh/LambdaPi.html
[2] http://thread.gmane.org/gmane.comp.lang.haskell.cafe/21314
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-prime/attachments/20070715/8d4d161e/attachment.htm