Re: Datatype contexts considered not so harmful
Anthony Clayden <[email protected]> Thu, 28 Jul 2022 19:11:16 +1200
| Newsgroups | gmane.comp.lang.haskell.hugs.user |
|---|---|
| Message-ID | <CABU_mxiNeixsbd_6wyLW5Fi-FRSwXZPT8L5kt7Q5BqU8ARP--g@mail.gmail.com> |
--===============7929602681237970898== Content-Type: multipart/alternative; boundary="000000000000c24d9a05e4d83d00" --000000000000c24d9a05e4d83d00 Content-Type: text/plain; charset="UTF-8" My proof-of-concept for this as of last year was flaky. I think I've now got it robust: - all DatatypeContexts apply for all constructors, irrespective of which type params the constructor mentions; - If a data constructor+fields appears in a pattern match, no constraints inferred; - whether using positional or labelled field syntax; - using field labels as selectors also doesn't infer constraints (they're as-if pattern matching); - numeric literals in patterns do raise a Num/Integral/Fractional constraint ... - ... even if nested inside a data constructor. (That's something I broke back in October.) 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. Back to the glorious GHC 1999 (and even pre-1991) future! And "Bleah!" right back to Wadler. AntC On Mon, 11 Oct 2021 at 19:40, Anthony Clayden <[email protected]> wrote: > > 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. > > http://web.archive.org/web/20151208175102/http://code.haskell.org/~dons/haskell-1990-2000/threads.html#04062, > 'Contexts on datatype declarations', starting at SPJ's opener. > > The Report has this example, section 4.2.1: > > > data Eq a => Set a = NilSet | ConsSet a (Set a) -- with inferred > types > > -- NilSet :: forall a. Set a > > -- ConsSet :: forall a. Eq a => a -> Set a -> a > > (If, per Wadler's response, he thinks "a type will make no sense without > the > constraints", what sense is there in having a `NilSet` without > constraints?) > > 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.) > > 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.) > > 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. > > 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. > > 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 > https://mail.haskell.org/pipermail/haskell-cafe/2004-March/005995.html > > As SPJ points out later in the 1999 thread > > > 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. > > > (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.) > > 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`. > > I can (just about) see use cases for datatypes that both have global > contexts and GADT constructors. > > AntC > > --000000000000c24d9a05e4d83d00 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"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 construc= tor mentions;</div><div>- If a data constructor+fields appears in a pattern= match, no constraints inferred;</div><div>- whether using positional or la= belled 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 s= omething I broke back in October.)</div><div><br></div><div>It turned out t= o only need a few lines of code added to the compiler. It was finding _wher= e_ 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! A= nd "<span style=3D"color:rgb(0,0,0)">Bleah!</span>" right back to= Wadler.</div><div><br></div><div>AntC</div><div><br></div></div><br><div c= lass=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Mon, 11 Oct 2= 021 at 19:40, Anthony Clayden <<a href=3D"mailto:anthony.d.clayden@gmail= .com">[email protected]</a>> wrote:<br></div><blockquote class= =3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rg= b(204,204,204);padding-left:1ex"><div dir=3D"ltr"><font face=3D"arial, sans= -serif"><br></font><div><font face=3D"arial, sans-serif">There's a disc= ussion in May 1999 pointing out the H98 Report is "inexplicit" wr= t the semantics of pattern matching on datatypes with a context.</font></di= v><div><font face=3D"arial, sans-serif"><a href=3D"http://web.archive.org/w= eb/20151208175102/http://code.haskell.org/~dons/haskell-1990-2000/threads.h= tml#04062" target=3D"_blank">http://web.archive.org/web/20151208175102/http= ://code.haskell.org/~dons/haskell-1990-2000/threads.html#04062</a>, 'Co= ntexts on datatype declarations', starting at SPJ's opener.<br></fo= nt></div><div><font face=3D"arial, sans-serif"><br></font></div><div><font = face=3D"arial, sans-serif">The Report has this example, section 4.2.1:</fon= t></div><div><font face=3D"arial, sans-serif"><br></font></div><div><font f= ace=3D"arial, sans-serif">>=C2=A0 =C2=A0 data Eq a =3D> Set a =3D Nil= Set | ConsSet a (Set a)=C2=A0 =C2=A0 =C2=A0-- with inferred types<br></font= ></div><div><font face=3D"arial, sans-serif">>=C2=A0 =C2=A0 -- NilSet ::= forall a. Set a</font></div><div><font face=3D"arial, sans-serif">>=C2= =A0 =C2=A0 -- ConsSet :: forall a. Eq a =3D> a -> Set a -> a</font= ></div><div><font face=3D"arial, sans-serif"><br></font></div><div><font fa= ce=3D"arial, sans-serif">(If, per Wadler's response, he thinks "a= =C2=A0<span style=3D"color:rgb(0,0,0);font-size:1em">type will make no sens= e without the</span></font></div><div><font face=3D"arial, sans-serif"><spa= n style=3D"color:rgb(0,0,0);font-size:1em">constraints</span>", what s= ense is there in having a `NilSet` without constraints?)</font></div><div><= font face=3D"arial, sans-serif"><br></font></div><div><font face=3D"arial, = sans-serif">Ref the q SPJ poses, it's _not_ the case that a selector fu= nction always gets the constraint inferred. (As of Hugs 2006 and GHC 8.10.)= </font></div><div><font face=3D"arial, sans-serif"><br></font></div><div><f= ont face=3D"arial, sans-serif">If a selector function pattern matches on `C= onsSet`, `Eq a =3D>` is indeed inferred. But if matching on only `NilSet= `, or only on a bare var/wildcard pattern, no constraint. (In practice of c= ourse you would be matching on `ConsSet`, so this point is purely academic.= )</font></div><div><font face=3D"arial, sans-serif"><br></font></div><div><= font face=3D"arial, sans-serif">Anyhoo, this behaviour doesn't deliver = Wadler's objective. And I find it weird you have to look at the term le= vel to explain the type. Since `data Eq a =3D> ...` prefixes the type an= d constructors, I'd expect the behaviour to apply at _type_ level.</fon= t></div><div><font face=3D"arial, sans-serif"><br></font></div><div><font f= ace=3D"arial, sans-serif">If I bend Hugs to behave=C2=A0same as-was GHC (no= constraint inferred if purely matching), I get the benefit I can declare i= nstances 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 =3D>`, but there's no means to p= ass in a dictionary.</font></div><div><font face=3D"arial, sans-serif"><br>= </font></div><div><font face=3D"arial, sans-serif">I can't declare a Fu= nctor 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 preservi= ng 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=3D"arial,= sans-serif"><a href=3D"https://mail.haskell.org/pipermail/haskell-cafe/200= 4-March/005995.html" target=3D"_blank">https://mail.haskell.org/pipermail/h= askell-cafe/2004-March/005995.html</a><br></font></div><div><font face=3D"a= rial, sans-serif"><br></font></div><div><font face=3D"arial, sans-serif">As= SPJ points out later in the 1999 thread</font></div><div><pre style=3D"col= or:rgb(0,0,0)"><font face=3D"arial, sans-serif">> But when you ta= ke 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=3D"arial, sans-serif"><br></font></div><di= v><font face=3D"arial, sans-serif">(I note GHC's=C2=A0Pattern Synonyms = seem to have fallen into the same hephalump trap of polluting constraints f= or matching with constraints needed only for building.)</font></div><div><f= ont face=3D"arial, sans-serif"><br></font></div><div><font face=3D"arial, s= ans-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 di= ctionary at each node and 'Provide' it on pattern matching. Whereas= for `Set` it's crucial you have exactly the same constraint 'all t= he way down', and all nodes type `Set a`.</font></div><div><font face= =3D"arial, sans-serif"><br></font></div><div><font face=3D"arial, sans-seri= f">I can (just about) see use cases for datatypes=C2=A0that both have globa= l contexts and GADT constructors.</font></div><div><font face=3D"arial, san= s-serif"><br></font></div><div><font face=3D"arial, sans-serif">AntC</font>= </div><div><br></div></div> </blockquote></div> --000000000000c24d9a05e4d83d00-- --===============7929602681237970898== Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: base64 Content-Disposition: inline X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KSHVncy1Vc2Vy cyBtYWlsaW5nIGxpc3QKSHVncy1Vc2Vyc0BoYXNrZWxsLm9yZwpodHRwOi8vbWFpbC5oYXNrZWxs Lm9yZy9jZ2ktYmluL21haWxtYW4vbGlzdGluZm8vaHVncy11c2Vycwo= --===============7929602681237970898==--