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