Dear Committee,
Richard has now revised the “Design for Dependent Types” proposal, and has resubmitted it.
I am in support of this proposal. I expect it will be painful at times to go that route, and it will creak at the edges, but my sense is that this eventual unification of types and terms is something that will become something we’d expect from a “modern language”, a bit like we expect function types and lambdas these days, and I have some hope that eventually, in a relatively far away future, Haskell will nicer and simpler because of this The alternative, sticking to a non-dependent design (and yes, getting some benefits from that too), could lead to Haskell becoming a “language of the 00s”. Useful, mature, great to get work done, still something that not everybody knows and you can still feel a bit special for knowing it. But no longer the language that is _both_ productively usable and at the same time incorporates new, research-close features. It might become a bit like Perl in that sense. (Ok, that’s a bit too gloomy … take it as hyperbole). I expect that discouraging punning will be maybe the most painful part of that route, for the wider community. import GHC.Tupe; swap :: Tuple [a,b] -> Tuple [b,a] just isn’t as smooth as `swap :: (a,b) -> (b,a)`. (And we can’t even cargo-cult from the ML family and use `(a * b) -> (b * a)` for the type of types…) I acknowledge that, I wish there was a better solution, but what’s in #378 seems to be the least bad. I am amused that this proposal rests on a PEP, and happy to see that the LSP gets a more central role in the language design ;-) Cheers, Joachim PS: Quick note about #291 (type variables in patterns), just to record my current thinking: I understand the reasoning, it would be nice to treat a `@(Maybe a)` argument like a `(Just x)` argument in patterns, binding `a`. But I am not convinced we can afford to toss out the ability to use an _occurence_ of a type `a`. My interpretation of #378’s implication on #291 is that we’ll have to find a way to distinguish binders from ocurrences that works independently of types and values (I believe we do need it for types, and I think we should have this for values as well anyways, as PatternSynonyms _should_ be able to abstract over patterns that have _required_ values, not just required constraints.) -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/