<div dir="ltr"><div dir="ltr">On Wed, Dec 9, 2020 at 11:21 AM Simon Peyton Jones via ghc-steering-committee <<a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a>> wrote:<br></div><div dir="ltr"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">





<div lang="EN-GB">
<div><span>I’d like to train Haskell users to get used to MonoLocalBinds.  I simply don’t know a way to give reliable, predictable
<i>type generalisation</i> (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.</span>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>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.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>So if we are thinking about the long term future of the language, I think MonoLocalBinds will be a part of it.</span></p></div></div></blockquote><div><br></div><div>(I was arguing in the same direction in the other thread before I saw Simon's email)</div><div><br></div><div>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.<br></div><div><br></div><div>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).</div><div><br></div><div>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.<br></div><div><br></div><div>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.<br></div></div></div>
</div>