<html><body><div dir=""><div dir="ltr">
    Hi,</div><div dir="ltr"><br></div><div dir="ltr">Thanks Richard and Vitaly for your answers. I am happy with the opt-in principle as a guideline, and I pretty much appreciate having this written down. Hopefully the Core Libraries Committee also follows this path, and ensures that the base libraries in the ecosystem can still be used without opting into DH.</div><div dir="ltr"><br></div><div dir="ltr">In summary: I am in favor of this proposal.</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 19 Apr 2021 at 18:29:06, Vitaly Bragilevsky <<a href="mailto:bravit111@gmail.com">bravit111@gmail.com</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 dir="ltr"><div>Dear Committee,</div><div><br></div>I support this proposal. I think, that the hardest problem when teaching Haskell is not to get through the basics. Many of us who have teaching experience all know how to get that done. The real problems come with type-level magic and workarounds involving singletons. I often find that it's much easier to explain and solve the very same problems in Idris than in Haskell. If we want to use the corresponding features in Haskell (and many of Haskellers really want that), we must make them clearer. I believe that DH (as sketched in this proposal) is the right way to do that. <div><br></div><div>Every now and then I hear the question if we are going to get dependent types in Haskell. I'm sure, Richard answers this question on a daily basis. I consider accepting this proposal as a clear statement to those who wait for dependent types in Haskell. So, let's do that!<div><br></div><div>Vitaly</div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">пн, 19 апр. 2021 г. в 19:04, Richard Eisenberg <<a href="mailto:rae@richarde.dev">rae@richarde.dev</a>>:<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 style="overflow-wrap: break-word;"><br><div><br><blockquote type="cite"><div>On Apr 19, 2021, at 3:03 AM, Alejandro Serrano Mena <<a href="mailto:trupill@gmail.com" target="_blank">trupill@gmail.com</a>> wrote:</div><div><div><div dir=""><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></div></div></blockquote><div><br></div><div>Both of these are great points to raise. For (1): we will have to continue to use good taste in designing the Prelude/`base` and other libraries. Lots of fancy features have existed in Haskell for decades, but we have been careful in how these are exposed to users. One small blunder happened a few years ago when `:t ($)` became very unwieldy (showing $'s levity polymorphism), and that got fixed before release. Another blunder (in my opinion) is that the type of length now requires understanding Foldable -- but the code around Foldable & Traversable is all Haskell98 anyway. It remains vitally important that error messages and GHCi interactions remain understandable to beginners. I personally would consider it a failure of this project if that were not to be the case. I have added some thoughts around this to the proposal at <a href="https://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0000-dependent-type-design.rst#learnability-of-haskell" target="_blank">https://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0000-dependent-type-design.rst#learnability-of-haskell</a></div><div><br></div><div>For (2): This is harder. I suppose a researcher could consider Haskell without -XLinearTypes -XDependentTypes, but any GHC-based implementation would be out of reach, then. Regardless, many Haskell-based research papers already choose a slice of GHC/Haskell to study, and I expect that to continue to be the case. However, I acknowledge that research accessibility may decrease with this change.</div></div><div><br></div><div>Richard</div><br></div>_______________________________________________<br>
ghc-steering-committee mailing list<br>
<a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a><br>
<a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br>
</blockquote></div>

        </blockquote>
    </div>
</div></div></body></html>