<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, 7 Jan 2022 at 09:08, Richard Eisenberg <<a href="mailto:lists@richarde.dev">lists@richarde.dev</a>> wrote:<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 style="overflow-wrap: break-word;"><br><div><br><blockquote type="cite"><div>On Jan 5, 2022, at 9:19 PM, Anthony Clayden <<a href="mailto:anthony.d.clayden@gmail.com" target="_blank">anthony.d.clayden@gmail.com</a>> wrote:</div><br><div><div style="font-family:Helvetica;font-size:14px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none"><font face="monospace">So Pattern syns seem to be giving exactly the 'stupid theta' behaviour.</font></div></div></blockquote><div><br></div><div>In your example, yes: the Required context is "stupid" in the way that "stupid theta" is. The reason to have a Required context is if your pattern synonym does computation that requires a constraint. ...</div></div></div></blockquote><div><br></div><div>I don't think that's the only (or even the chief) reason. Wadler's response on that 1999 thread is telling</div><div><br></div><div>"<span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em">Often, a type will make no sense without the </span><span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em">constraints; e.g., an association list type Alist a b makes no sense </span><span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em">unless Eq a holds.  The class constraints on data declarations were a </span><span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em">simple way for the user to ask the compiler to enforce this invariant. </span><span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em">They have compile-time effect only, no effect whatsoever on run-time </span><span style="font-size:1em;color:rgb(0,0,0);font-family:monospace,monospace">(in particular, no dictionaries should be passed).</span>  "</div><div><br></div><div>And yet he's somehow forgotten his own design for constraints: the _only_ way to enforce a constraint is by providing evidence in the form of a dictionary. (This is especially impossible for a constructor class where it's the (invisible) argument type to the constructor that wants the constraint.) That's why I agree with SPJ 1999 here: on a pattern match there's no mechanism to pass in a constraint (dictionary-as-evidence); and you're not doing computation in merely matching -- it doesn't even need `Eq`. </div><div><br></div><div>In a pattern</div><div><br></div><div>>    baz (MkT 3 3) = "Three"               -- desugars to</div><div>>    baz (MkT x y) | x == fromInteger #3#, y == fromInteger #3# = "Three"</div><div><br></div><div>It's the appearance of the `==` and `fromInteger` that Require `(Eq a, Num a)`; I don't expect them Provided by `T`'s nor `MkT`'s Datatype context. And in general, guards can induce arbitrary computation; it's not the responsibility of the datatype declarer to anticipate that. (A Separation of Concerns argument.)</div><div><br></div><div>So I want constraints 'Required' for building -- that is constraints 'sighted' whether or not any computation involved; but not 'Provided' by matching -- because they're already sighted by the very fact of having built the pattern (to paraphrase SPJ1999). Thanks for pointing out that proposal. I guess it'll achieve what I want for a BST or Wadler's assoc list; would be nice to see an explicit example.</div><div><br></div><div>I don't want to use a GADT here, because it's the same constraint on every data constructor; and a BST recurses with the same constraint; holding identical dictionaries inside each node is just clutter. Something accessing the BST (probably) needs to bring its `Ord` dictionary with it (`elem` for example); but not necessarily (`count`, `toList` or `show`).</div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow-wrap: break-word;"><div><div><br></div><blockquote type="cite"><div><div style="font-family:Helvetica;font-size:14px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none"><font face="monospace"><br></font></div><div style="font-family:Helvetica;font-size:14px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none"><font face="monospace">The User Guide <a href="https://downloads.haskell.org/~ghc/8.10.7/docs/html/users_guide/glasgow_exts.html#typing-of-pattern-synonyms" target="_blank">https://downloads.haskell.org/~ghc/8.10.7/docs/html/users_guide/glasgow_exts.html#typing-of-pattern-synonyms</a><span> </span>says</font></div><div style="font-family:Helvetica;font-size:14px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none"><font face="monospace"><br></font></div><ul style="font-family:Helvetica;font-size:14px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none"><li><div style="margin:0px"><font face="monospace">⟨CProv⟩ are the constraints <em>made available (provided)</em> by a successful pattern match.</font></div></li></ul><div style="font-family:Helvetica;font-size:14px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none"><font face="monospace"><font><span style="font-size:14px">But it doesn't mean that. It's more like "</span></font><span style="font-size:14px">⟨CProv⟩ are the constraints made available *in addition to </span><span style="font-size:14px">⟨CReq⟩* (provided union required) by a successful pattern match."</span></font></div></div></blockquote><br></div><div>I agree with the user guide here: the Provided constraints are made available. The Required constraint must *already* be available before the pattern match,</div></div></blockquote><div><br></div><div>I disagree. To "be available" requires a dictionary. A pattern synonym gets desugarred, it doesn't hold a dictionary itself. The dictionary *was* "already available" at the time of building; but it's no longer available unless the PatSyn got desugarred to a GADT with that dictionary inside. I want these PatSyns desugarred to ordinary H98 data constructors.</div><div><br></div><div>And I want an empty Provided `:: (Ord a) => () => a -> a -> T a` to mean nothing is Provided, not even what was Required.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow-wrap: break-word;"><div><br></div><div><br></div><div>To get the pre-1999 behavior, you would need a different type for a pattern synonym used as a pattern than for one used as an expression. This is the subject of the accepted-but-not-implemented <a href="https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bidir-constr-sigs.rst" target="_blank">https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bidir-constr-sigs.rst</a></div><div><br></div><div><br></div></div></blockquote><div><br></div><div><br></div><div><br></div><div>AntC</div><div> </div></div></div>