<div dir="ltr"><div dir="ltr"><br></div><font face="arial, sans-serif"><br></font><div class="gmail_quote"><div dir="ltr" class="gmail_attr"><font face="arial, sans-serif">On Wed, 6 Oct 2021 at 21:24, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>> wrote:<br></font></div><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" style="overflow-wrap: break-word;">
<div class="gmail-m_-2913048578943876266WordSection1">
<p class="MsoNormal" style="margin-left:36pt"><font face="arial, sans-serif"> <br></font></p>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:36pt">
<font face="arial, sans-serif">I suggest the User Guide needs an example where a constraint needed for matching (presumably via a View pattern) is not amongst the constraints carried inside the data constructor, nor amongst those needed for building.
Then the limitations in the current design would be more apparent for users.<u></u><u></u></font></p>
<p class="MsoNormal"><span><font face="arial, sans-serif"><u></u> <u></u></font></span></p>
<p class="MsoNormal"><span><font face="arial, sans-serif">The <a href="https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pattern_synonyms.html?highlight=pattern%20syn#typing-of-pattern-synonyms" target="_blank">
user manual</a> does already speak about the type of a builder, here:</font></span></p></div></div></blockquote><div><p class="gmail-m_-2913048578943876266first" style="margin-left:36pt"><font face="arial, sans-serif">...<br class="gmail-Apple-interchange-newline"> How could we make that clearer?<br></font></p><p class="MsoNormal"><font face="arial, sans-serif"><br></font></p><p class="MsoNormal"><font face="arial, sans-serif">This point in that section of the Guide is wrong/misleading:</font></p><p class="MsoNormal"><font face="arial, sans-serif"><br></font></p><p class="MsoNormal"><font face="arial, sans-serif"> </font></p><ul class="gmail-simple" style="box-sizing:border-box;margin:0px 0px 24px;padding:0px;list-style-position:initial;line-height:24px;color:rgb(64,64,64)"><li style="box-sizing:border-box;list-style:disc;margin-left:24px"><font face="arial, sans-serif" style=""><span style="background-color:rgb(252,252,252)">⟨CReq⟩ are the constraints </span><em style="background-color:rgb(252,252,252);box-sizing:border-box">required</em><span style="background-color:rgb(252,252,252)"> to ma</span><span style="background-color:rgb(255,255,255)">tch the <span class="gmail-highlighted" style="background-image:initial;background-position:initial;background-size:initial;background-repeat:initial;background-origin:initial;background-clip:initial;box-sizing:border-box;display:inline-block;padding:0px 6px">pattern</span>.</span></font></li></ul></div><div><font face="arial, sans-serif"><CReq> must be the union of the constraints required to match the pattern, _plus_ required to build with the pattern -- if it is bidirectional.</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">Then thank you Simon, but it's the type of the _matcher_ that's problematic. The only mechanism for getting the constraints needed for building is by polluting the constraints needed for matching. Here's a (crude, daft) example, using guards to 'raise' a required-for-failing-to-build that isn't required-for-successful-building nor for-matching</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">> pattern TwoNode :: (Show a, Ord a) => () => a -> a -> Tree a -- GHC insists on both constraints as Req'd</font></div><div><font face="arial, sans-serif">><br>> pattern TwoNode x y <- Node Empty x (Leaf y) where<br>> TwoNode x y | x > y = Node Empty x (Leaf y)<br>> | otherwise = error (show x ++ " not greater " ++ show y)<br><br></font></div><div><font face="arial, sans-serif">To quote you from May 1999</font></div><div><font face="arial, sans-serif"><br></font></div><div><pre style="color:rgb(0,0,0)"><font face="arial, sans-serif">> But when you take a constructor *apart*, the invariant must hold
> by construction: you couldn't have built the thing you are taking
> apart unless invariant held. So enforcing the invariant again is
> redundant; and in addition it pollutes the type of selectors.
</font></pre><font face="arial, sans-serif">`Show a` must have "held by construction" of the `Node`. But the PatSyn's constraints are requiring more than that was true in some distant line of code: </font> it wants <i>evidence</i> in the form of a dictionary at the point of deconstructing; since the build was successful, I ipso facto don't want to `show` anything in consuming it. An `instance Foldable Tree` has no mechanism to pass in any such dictionaries (which'll anyway be redundant, as you say).</div><div><br></div><div><br></div><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" style="overflow-wrap: break-word;"><div class="gmail-m_-2913048578943876266WordSection1"><div style="border-top:none;border-right:none;border-bottom:none;border-left:1.5pt solid blue;padding:0cm 0cm 0cm 4pt"><div><div><blockquote style="border-top:none;border-right:none;border-bottom:none;border-left:1pt solid rgb(204,204,204);padding:0cm 0cm 0cm 6pt;margin-left:4.8pt;margin-right:0cm">
</blockquote>
</div>
</div>
</div>
</div>
</div>
</blockquote></div></div>