(Succ Haskell') `and` $ dependent types

[Stefan O'Rear]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell-prime/attachments/20070714/948a6e87/attachment.bin