<div dir="ltr">My proof-of-concept for this as of last year was flaky. I think I've now got it robust:<div><br></div><div>- all DatatypeContexts apply for all constructors, irrespective of which type params the constructor mentions;</div><div>- If a data constructor+fields appears in a pattern match, no constraints inferred;</div><div>- whether using positional or labelled field syntax;</div><div>- using field labels as selectors also doesn't infer constraints (they're as-if pattern matching);</div><div>- numeric literals in patterns do raise a Num/Integral/Fractional constraint ...</div><div>- ... even if nested inside a data constructor. (That's something I broke back in October.)</div><div><br></div><div>It turned out to only need a few lines of code added to the compiler. It was finding _where_ to position them that needed a huge amount of trial and error.</div><div><br></div><div>Back to the glorious GHC 1999 (and even pre-1991) future! And "<span style="color:rgb(0,0,0)">Bleah!</span>" right back to Wadler.</div><div><br></div><div>AntC</div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 11 Oct 2021 at 19:40, Anthony Clayden <<a href="mailto:anthony.d.clayden@gmail.com">anthony.d.clayden@gmail.com</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 dir="ltr"><font face="arial, sans-serif"><br></font><div><font face="arial, sans-serif">There's a discussion in May 1999 pointing out the H98 Report is "inexplicit" wrt the semantics of pattern matching on datatypes with a context.</font></div><div><font face="arial, sans-serif"><a href="http://web.archive.org/web/20151208175102/http://code.haskell.org/~dons/haskell-1990-2000/threads.html#04062" target="_blank">http://web.archive.org/web/20151208175102/http://code.haskell.org/~dons/haskell-1990-2000/threads.html#04062</a>, 'Contexts on datatype declarations', starting at SPJ's opener.<br></font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">The Report has this example, section 4.2.1:</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">> data Eq a => Set a = NilSet | ConsSet a (Set a) -- with inferred types<br></font></div><div><font face="arial, sans-serif">> -- NilSet :: forall a. Set a</font></div><div><font face="arial, sans-serif">> -- ConsSet :: forall a. Eq a => a -> Set a -> a</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">(If, per Wadler's response, he thinks "a <span style="color:rgb(0,0,0);font-size:1em">type will make no sense without the</span></font></div><div><font face="arial, sans-serif"><span style="color:rgb(0,0,0);font-size:1em">constraints</span>", what sense is there in having a `NilSet` without constraints?)</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">Ref the q SPJ poses, it's _not_ the case that a selector function always gets the constraint inferred. (As of Hugs 2006 and GHC 8.10.)</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">If a selector function pattern matches on `ConsSet`, `Eq a =>` is indeed inferred. But if matching on only `NilSet`, or only on a bare var/wildcard pattern, no constraint. (In practice of course you would be matching on `ConsSet`, so this point is purely academic.)</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">Anyhoo, this behaviour doesn't deliver Wadler's objective. And I find it weird you have to look at the term level to explain the type. Since `data Eq a => ...` prefixes the type and constructors, I'd expect the behaviour to apply at _type_ level.</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">If I bend Hugs to behave same as-was GHC (no constraint inferred if purely matching), I get the benefit I can declare instances for constructor classes (including Foldable) over type constructor `Set`. Whereas the post-May 199 behaviour disallows this: pattern matching in the method decls wants an `Eq a =>`, but there's no means to pass in a dictionary.</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">I can't declare a Functor instance, because building the result applies the data constructors, so does want a dictionary; again there's no means to pass one in. I can simulate `fmap` via Foldable's `foldMap`, because that wants a Monoid instance for the builder, and that does see the element type as well as the constructor. (The builder can squish out resulting duplicates, so preserving the invariant of `Set`.) Not being able to declare `Set` an instance of Functor is a Good Thing. Nor of Monad</font></div><div><font face="arial, sans-serif"><a href="https://mail.haskell.org/pipermail/haskell-cafe/2004-March/005995.html" target="_blank">https://mail.haskell.org/pipermail/haskell-cafe/2004-March/005995.html</a><br></font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">As SPJ points out later in the 1999 thread</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></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">(I note GHC's Pattern Synonyms seem to have fallen into the same hephalump trap of polluting constraints for matching with constraints needed only for building.)</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">If you're thinking "but hasn't GHC solved all this with GADTs?" I say no: their sweet spot is where there's different constraints down the structure; you can't help but hold a different dictionary at each node and 'Provide' it on pattern matching. Whereas for `Set` it's crucial you have exactly the same constraint 'all the way down', and all nodes type `Set a`.</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">I can (just about) see use cases for datatypes that both have global contexts and GADT constructors.</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">AntC</font></div><div><br></div></div>
</blockquote></div>