[ghc-steering-committee] Recommendation for #378: support the design for dependent types

Richard Eisenberg rae at richarde.dev
Mon Apr 19 16:03:44 UTC 2021



> On Apr 19, 2021, at 3:03 AM, Alejandro Serrano Mena <trupill at gmail.com> wrote:
> 
> 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.

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 https://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0000-dependent-type-design.rst#learnability-of-haskell <https://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0000-dependent-type-design.rst#learnability-of-haskell>

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.

Richard

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20210419/4b167804/attachment.html>


More information about the ghc-steering-committee mailing list