Hello,<br><br>As the authors point out [1], coal-face time needs to be expended before real world adoption of Dependently-Typed functional programming.&nbsp; But let&#39;s get the ball rolling.&nbsp; They say that haskell programmers are normally averse to dependent types.&nbsp; Is this true?&nbsp; It seems to me that one of the appeals of Haskell is the ability to program in a &quot;prove perfect, write once&quot; (elegant) style.&nbsp; Is not dependent typing a good move towards this goal?.&nbsp; It addresses a problem [2] with which we, in our everyday common inter-hominem usage, can deal -- with which (ideal) Haskell should deal. 
<br><br>While the major Haskell implementations would require a substantial overhaul, the change at the syntactic level appears to be minimal.&nbsp; There also needs to be advance with respect to programmer development (automatic edit-time inference of (some) types). What are peoples&#39; thoughts on adding dependent types to haskell as a non-incremental evolutionary step?&nbsp; 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?
<br><br>Vivian<br><br>[1] <a href="http://www.informatik.uni-bonn.de/~loeh/LambdaPi.html">http://www.informatik.uni-bonn.de/~loeh/LambdaPi.html</a><br>[2] <a href="http://thread.gmane.org/gmane.comp.lang.haskell.cafe/21314">
http://thread.gmane.org/gmane.comp.lang.haskell.cafe/21314</a><br>