On Sun, Jul 15, 2007 at 09:04:16AM +1200, Vivian McPhail wrote:
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
Dependant types aren't new, they're ten times older than Haskell ;) I don't even think that adding dependant types to Haskell would be that hard. Most of the needed infrastructure (notably the binder rule, lexically scoped type variables, and explicit instantiation) already exists in the implementation of rank-N types in GHC. I think much of the work would be in revising Core (currently it uses a variant of Barandregt's λω, which is strictly less powerful (IIUC) than the full dependant λC) and flattening the typeinfer/kindinfer staging. Of course, since Haskell is not strongly normalizing, we would not be able to use a calculus where applications of CONV are implicit. Interaction with qualified types (type classes, MPTC, fundeps, implicit parameters, extensible records, associated type synonym equality predicates, etc) could be interesting, in both senses of the word. Stefan