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

[Alejandro Serrano Mena]

 Dear Committee,

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.

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.

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?

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?).

Regards,
Alejandro


On 18 Apr 2021 at 11:26:14, Joachim Breitner <mail at joachim-breitner.de>
wrote:

> Dear Committee,
>
> Richard has now revised the “Design for Dependent Types” proposal,
>
> and has resubmitted it.
>
> I am in support of this proposal. I expect it will be painful at times
> to go that route, and it will creak at the edges, but my sense is that
> this eventual unification of types and terms is something that will
> become something we’d expect from a “modern language”, a bit like we
> expect function types and lambdas these days, and I have some hope that
> eventually, in a relatively far away future, Haskell will nicer and
> simpler because of this
>
> The alternative, sticking to a non-dependent design (and yes, getting
> some benefits from that too), could lead to Haskell becoming a
> “language of the 00s”. Useful, mature, great to get work done, still
> something that not everybody knows and you can still feel a bit special
> for knowing it. But no longer the language that is _both_ productively
> usable and at the same time incorporates new, research-close features.
> It might become a bit like Perl in that sense. (Ok, that’s a bit too
> gloomy … take it as hyperbole).
>
>
> I expect that discouraging punning will be maybe the most painful
> part of that route, for the wider community.
>  import GHC.Tupe; swap ::
> Tuple [a,b] -> Tuple [b,a]
> just isn’t as smooth as `swap :: (a,b) ->
> (b,a)`.
> (And we can’t even cargo-cult from the ML family and use
> `(a * b) -> (b * a)` for the type of types…)
> I acknowledge that, I wish
> there was a better solution, but what’s in #378 seems to be the least
> bad.
>
>
> I am amused that this proposal rests on a PEP, and happy to see that
> the LSP gets a more central role in the language design ;-)
>
> Cheers,
> Joachim
>
>
> PS: Quick note about #291 (type variables in patterns), just to record
> my current thinking:
>
> I understand the reasoning, it would be nice to
> treat a `@(Maybe a)` argument like a `(Just x)` argument in patterns,
> binding `a`. But I am not convinced we can afford to toss out the
> ability to use an _occurence_ of a type `a`. My interpretation of
> #378’s implication on #291 is that we’ll have to find a way to
> distinguish binders from ocurrences that works independently of types
> and values (I believe we do need it for types, and I think we should
> have this for values as well anyways, as PatternSynonyms _should_ be
> able to abstract over patterns that have _required_ values, not just
> required constraints.)
>
> --
> Joachim Breitner
>  mail at joachim-breitner.de
>  http://www.joachim-breitner.de/
>
>
> _______________________________________________
> 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/9a519d21/attachment.html>