<html><body><div dir=""><div dir="ltr">
Dear Committee,</div><div dir="ltr"><br></div><div dir="ltr">I still have mixed feeling about this, but they are more about the whole “Dependent Haskell” project as a whole than about this specific proposal, which I find now in really good shape.</div><div dir="ltr"><br></div><div dir="ltr">On the one hand, I fear that by introducing more and more DH features, the language will morph into something difficult to reconcile with “basic Haskell”. After all, if we have dependent features available, why not use it in the Prelude and other libraries? This would make Haskell harder to use in (1) teaching, since newcomers would need more time to understand those features, and (2) research, since to build a tool on top of Haskell (think of LiquidHaskell) you’ll need to buy the whole “dependent + linear paradigm” too.</div><div dir="ltr"><br></div><div dir="ltr">On the other hand, the status of type-level computation in GHC is less than ideal: too many separate extensions, each of them adding a tiny bit of expressiveness, and a handful of folklore tricks. On that regard, having a prospective design of the future is great, because (1) it allows for a more cohesive set of features, and (2) helps on focusing the goals of the broader community. And since GHC already have some of those features, it’s actually possible to stop the boat sailing on the direction of dependent + linear types?</div><div dir="ltr"><br></div><div dir="ltr">Is this the design we want? is yet another question. I am quite confident about the maturity of the design, knowing that the authors have been working on this problem for years (even more a decade?).</div><div dir="ltr"><br></div><div dir="ltr">Regards,</div><div dir="ltr">Alejandro</div><div dir="ltr"><br><br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On 18 Apr 2021 at 11:26:14, Joachim Breitner <<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a>> wrote:<br></div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div>
<div>
Dear Committee,<br><br><blockquote type="cite"> Richard has now revised the “Design for Dependent Types” proposal,<br></blockquote>and has resubmitted it. <br><br>I am in support of this proposal. I expect it will be painful at times<br>to go that route, and it will creak at the edges, but my sense is that<br>this eventual unification of types and terms is something that will<br>become something we’d expect from a “modern language”, a bit like we<br>expect function types and lambdas these days, and I have some hope that<br>eventually, in a relatively far away future, Haskell will nicer and<br>simpler because of this <br><br>The alternative, sticking to a non-dependent design (and yes, getting<br>some benefits from that too), could lead to Haskell becoming a<br>“language of the 00s”. Useful, mature, great to get work done, still<br>something that not everybody knows and you can still feel a bit special<br>for knowing it. But no longer the language that is _both_ productively<br>usable and at the same time incorporates new, research-close features.<br>It might become a bit like Perl in that sense. (Ok, that’s a bit too gloomy … take it as hyperbole).<br><br><br>I expect that discouraging punning will be maybe the most painful<br>part of that route, for the wider community.<br> import GHC.Tupe; swap ::<br>Tuple [a,b] -> Tuple [b,a]<br>just isn’t as smooth as `swap :: (a,b) -><br>(b,a)`.<br>(And we can’t even cargo-cult from the ML family and use<br>`(a * b) -> (b * a)` for the type of types…)<br>I acknowledge that, I wish<br>there was a better solution, but what’s in #378 seems to be the least<br>bad.<br><br><br>I am amused that this proposal rests on a PEP, and happy to see that<br>the LSP gets a more central role in the language design ;-)<br><br>Cheers,<br>Joachim<br><br><br>PS: Quick note about #291 (type variables in patterns), just to record<br>my current thinking: <br><br>I understand the reasoning, it would be nice to<br>treat a `@(Maybe a)` argument like a `(Just x)` argument in patterns,<br>binding `a`. But I am not convinced we can afford to toss out the<br>ability to use an _occurence_ of a type `a`. My interpretation of<br>#378’s implication on #291 is that we’ll have to find a way to<br>distinguish binders from ocurrences that works independently of types<br>and values (I believe we do need it for types, and I think we should<br>have this for values as well anyways, as PatternSynonyms _should_ be<br>able to abstract over patterns that have _required_ values, not just<br>required constraints.)<br><br>-- <br>Joachim Breitner<br> <a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a><br> <a href="http://www.joachim-breitner.de/">http://www.joachim-breitner.de/</a><br><br><br>_______________________________________________<br>ghc-steering-committee mailing list<br><a href="mailto:ghc-steering-committee@haskell.org">ghc-steering-committee@haskell.org</a><br><a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br>
</div>
</div>
</blockquote>
</div>
</div></div></body></html>