[ghc-steering-committee] A plea against "fancy types" in GHC2021

[Spiwack, Arnaud]

On Wed, Dec 9, 2020 at 11:21 AM Simon Peyton Jones via
ghc-steering-committee <ghc-steering-committee at haskell.org> wrote:

> I’d like to train Haskell users to get used to MonoLocalBinds.  I simply
> don’t know a way to give reliable, predictable *type generalisation* (to
> get polymorphic types) for local bindings, in the presence of GADTs etc.  I
> don’t think that situation is going to improve (i.e. it’s not a short term
> problem) … indeed it may become more pressing as the type system advances.
> It’s switched on by TypeFamilies, and I think GADTs, so many of us are
> using it anyway.
>
>
>
> Most local bindings are not polymorphic, so no problem; those that are
> probably deserve a type signature anyway.   But I accept that there is a
> cost here: we’re giving up on generalisation for local bindings.
>
>
>
> So if we are thinking about the long term future of the language, I think
> MonoLocalBinds will be a part of it.
>

(I was arguing in the same direction in the other thread before I saw
Simon's email)

I would like to add that, personally, in the past few years, I've been
completely converted to the MonoLocalBinds religion. Generalising is hard.
Generalising non-pure-ML types and terms is often impossible. The
algorithmic of generalising is really tricky. You need to care about scopes
(don't generalise a variable which is used by someone else!).
Generalisation tends to end up taking over the entire type checking
algorithm. And it shouldn't be surprising that it is hard: we're changing
existential quantifiers into universal quantifiers. It's a weird thing to
do.

Generalising at toplevel is much easier. Though, to be honest, I'm
increasingly of the opinion that MonoLocalBinds doesn't go far enough, and
that we oughtn't generalise at top level either (unless we have a type
signature). And, actually, this is what happens with multiplicities in GHC
9.0: we never infer a multiplicity-polymorphic type. (it's not really a big
restriction since we tend to write signatures at toplevel always, anyway).

As a side remark: I don't think MonoLocalBind ever caused a file of mine to
stop compiling when I turn on TypeFamilies or GADTs (which does happen to
most of my files). So I assume that I don't tend to rely on generalisation
all that much.

PS: I'd like to add that I'm really happy that we are having these
discussions. There seems to be a lot of implicitness in how GHC is
designed, and facing GHC2021 forces us to reveal this implicitness. This
is, in my opinion, immensely productive.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20201209/d2b425d2/attachment.html>