<div dir="auto"><div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Sep 6, 2020, 7:24 AM Ignat Insarov <<a href="mailto:kindaro@gmail.com">kindaro@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> If a value of the<br>
transient instantiation of `defaultY` _(that exists only in the moment<br>
before its field is updated)_ is never observed, why does it need to<br>
be monomorphized? Why not be lazy about it?</blockquote></div></div><div dir="auto"><br></div><div dir="auto">You could just as well ask why ‘(== [])’ or ‘(== Nothing)’ require an ‘Eq’ constraint even though it will provably never be used. The reason, of course, is that the typechecker is only using purely local reasoning—yes, if you inlined that function far enough into any use site, it would lead to showing the ‘Eq’ redundant; and here, if you examined the update as a whole, you would find the type of the subterm is redundant as well.</div><div dir="auto"><br></div><div dir="auto">The same is true for typeclasses generally—instead of having bounded polymorphism, we could just substitute types and see what happens, like C++ templates do, but having the requirements stated in the type improves the predictability of whether something will typecheck, and improves the quality of error messages when it doesn’t.</div><div dir="auto"><br></div><div dir="auto">Basically, we accept that types will always be an <i>approximation</i> of terms. You can draw the line at different points—with refinement types, you can reason about the particular values or ranges of integers, for instance, instead of the coarse-grained ‘Int’. But all solutions that give you finer granularity also have tradeoffs in terms of ergonomics and predictability. Haskell has largely chosen to draw the line at “syntax-directed” as our criterion for how checking ought to work, assigning a type to every subterm in the same way, without context. This has turned out to be pretty usable in practice, even if there are some frustrating circumstances like this where you as a human can plainly <i>see</i> a fact that the typechecker cannot.</div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto"></div></div>