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

[Vitaly Bragilevsky]

Dear Committee,

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.

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!

Vitaly

пн, 19 апр. 2021 г. в 19:04, Richard Eisenberg <rae at richarde.dev>:

>
>
> 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
>
> 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
>
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20210419/4a21e0c9/attachment.html>