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

[Alejandro Serrano Mena]

 Hi,

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.

In summary: I am in favor of this proposal.

Regards,
Alejandro


On 19 Apr 2021 at 18:29:06, Vitaly Bragilevsky <bravit111 at gmail.com> wrote:

> 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/20210422/13203b44/attachment.html>