TypeCastery
Anthony Clayden <[email protected]> Thu, 4 Oct 2018 00:45:08 +1300
| Newsgroups | gmane.comp.lang.haskell.hugs.user |
|---|---|
| Message-ID | <CAM7nRYTYJo7feDLvUh8OHTPqSA-=xfX1Kzouwrj0roTN4XiA6A@mail.gmail.com> |
--===============0349836246219615252== Content-Type: multipart/alternative; boundary="000000000000a9f23205775192d2" --000000000000a9f23205775192d2 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable A typical consequence of combining FunDeps + Overlapping instances is that you have to make the result parameter more general than it needs be, then use a TypeCast constraint to improve it. There's a classic example in the HList paper [*], Section 9 'A generic type equality predicate'. > class TypeEq x y b | x y -> b > > instance TypeEq x x HTrue -- HTrue, HFalse are just two datatypes > > instance (TypeCast HFalse b) > =3D> TypeEq x y b -- can't put TypeEq= x y HFalse (And really all of the tricky type improvement in that paper boils down to that technique, whether or not there's an explicit TypeEq test.) The paper says the TypeEq solution is GHC-specific. That's true but .... I wonder if they discussed their results with the Hugs team at the time, because it's not needed drastic surgery to make Hugs do that. (Perhaps I broke something, but if so it's going to take a convoluted example to find it. I've built a routine that merges TRex records by matching label names, with horrendous amounts of overlap and typecasting.) The technique relies on TypeCast, which does use FunDeps to mutually improve/unify its two parameters. Nowadays in GHC you'd use the (~) constraint. TypeCast does use a complicated chain of "indirection" superconstraints on instances, but does not use overlaps -- indeed there's only a single instance for each of the classes involved. I'd been happily using the version of TypeCast given in Appendix D 'Generic type unification cont'd'. Then I re-read the paper, which claimed it didn't work in Hugs [Section 9 'Reification of type unification']: "The most generic implementation of TypeCast, which works for both Hugs and GHC, is ... For this implementation to work, we need ... Otherwise, type simplification will ... and thereby inline the unification." IOW unification will be too 'eager'/too smart and see that we're trying to evade the FunDep consistency rule. "Alas, this implementation [Appendix D alternative] is specific to GHC; it does not work in Hugs because of the peculiarities of that system with regard to MPTCs and functional dependencies, ..." I'm experiencing that the Section 9 implementation claimed to work in Hugs, doesn't; and the Appendix D implementation claimed to not work in Hugs, does. That's using the legitimate distro version of Hugs Sep2006. Possibly Hugs changed after 2004 when the HList work was reported. (In Section 6 of the paper "We give up on persuading Hugs." so I guess they didn't explore further.) That is, the Section 9 implementation exhibits the 'eager' type unification, whether or not I declare TypeCast in a separate module and "import it at a higher level in the module hierarchy" [Section 9]. That is, if I'm doing that right: what does "separate compilation" mean in context of Hugs? It's an interpreter not a compiler; it doesn't produce executables/object code. Indeed if you import a library -- even one of the standard Report-defined libraries, it goes and gets the library source and compiles that alongside the client program. There's no Haskell interface/.hi files that I can see(?) Oh, and there's another advantage to avoiding separate compilation: Hugs can see all the instances and their constraints (and instances of the constraint classes) across all the modules. So no 'orphan instances' -- the problems with which were amongst the reasons for Section 6 'Overlapping banned'. "we do not want to depend on the doubtful future of overlapping instances in general ... GHC's instance selection is lazy, whereas Hugs' is eager". This leads the paper on to "what's known as the Data.Typeable approach at the type level". But the cure is worse than the disease! It's just not scalable and not workable. So the version of HList that has persisted to this day does use the combo of Fundeps + Overlaps, and despite the paper's misgivings, that has persistently been stable in GHC. No "doubtful future" after a dozen years. To pick up a misrepresentation: "GHC's instance selection is lazy": no, GHC's validation of overlapping instances is lazy; but its selection is eager, too eager: it commits to an instance inside each module, ignoring the possibility this module is imported into another with an overlapping module which is a better fit. Whereas the alleged "Hugs' is eager" is also opposite to the truth: Hugs' selection of an instance is delayed as much as possible until it's sure there's only one fit (it can see all instances in all imports). Validation of overlap is eager: instances (heads) must be in strict substitution sequence. That's often a nuisance, but a price I'm prepared to pay to get better coherence. 'Orphan instances' (and overlap thereof) are certainly a danger in GHC. Avoiding them was part of the motivation for Closed Type Families to be grouped in a single syntactic unit/in a single module. And yet GHC knows how to defer instance selection if there's no unique/suitable instance visible in a module. Why can't it do that everywhere? Or at least warn if imports contain instances that are overlapped in a different module. Then it seems to me: * not only does GHC have a "bogus" implementation of the FunDep consistency rule; but also * GHC's implementation of Overlaps is broken. Hugs' implementation of both is a lot more restrictive, and more coherent. I'm not finding it prevents any programs. It does require I structure them in specific ways. AntC [*] Strongly Typed Heterogeneous Collections 2004, Oleg Kiselyov, Ralf L=C3=A4mmel, Keean Schupke --000000000000a9f23205775192d2 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"auto">A typical consequence of combining FunDeps + Overlapping = instances is that you have to make the result parameter more general than i= t needs be, then use a TypeCast constraint to improve it.</div><div dir=3D"= auto"><br></div><div dir=3D"auto">There's a classic example in the HLis= t paper [*], Section 9 'A generic type equality predicate'.</div><d= iv dir=3D"auto"><br></div><div dir=3D"auto">> class TypeEq x y b =C2=A0|= x y -> b</div><div dir=3D"auto">></div><div dir=3D"auto">> instan= ce TypeEq x x HTrue =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= =C2=A0 -- HTrue, HFalse are just two datatypes</div><div dir=3D"auto">>= </div><div dir=3D"auto">> instance (TypeCast HFalse b)</div><div dir=3D"= auto">> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= =3D> TypeEq x y b =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0-- can't put TypeEq x y HFalse</div><div dir=3D"auto">= <br></div><div dir=3D"auto">(And really all of the tricky type improvement = in that paper boils down to that technique, whether or not there's an e= xplicit TypeEq test.)</div><div dir=3D"auto"><br></div><div dir=3D"auto">Th= e paper says the TypeEq solution is GHC-specific. That's true but .... = I wonder if they discussed their results with the Hugs team at the time, be= cause it's not needed drastic surgery to make Hugs do that. (Perhaps I = broke something, but if so it's going to take a convoluted example to f= ind it. I've built a routine that merges TRex records by matching label= names, with horrendous amounts of overlap and typecasting.)</div><div dir= =3D"auto"><br></div><div dir=3D"auto">The technique relies on TypeCast, whi= ch does use FunDeps to mutually improve/unify its two parameters. Nowadays = in GHC you'd use the (~) constraint. TypeCast does use a complicated ch= ain of "indirection" superconstraints on instances, but does not = use overlaps -- indeed there's only a single instance for each of the c= lasses involved. I'd been happily using the version of TypeCast given i= n Appendix D 'Generic type unification cont'd'. Then I re-read = the paper, which claimed it didn't work in Hugs [Section 9 'Reifica= tion of type unification']:</div><div dir=3D"auto"><br></div><div dir= =3D"auto">"The most generic implementation of TypeCast, which works fo= r both Hugs and GHC, is ... For this implementation to work, we need ... Ot= herwise, type simplification will ... and thereby inline the unification.&q= uot; IOW unification will be too 'eager'/too smart and see that we&= #39;re trying to evade the FunDep consistency rule.</div><div dir=3D"auto">= "Alas, this implementation [Appendix D alternative] is specific to GHC= ; it does not work in Hugs because of the peculiarities of that system with= regard to MPTCs and functional dependencies, ..."</div><div dir=3D"au= to"><br></div><div dir=3D"auto">I'm experiencing that the Section 9 imp= lementation claimed to work in Hugs, doesn't; and the Appendix D implem= entation claimed to not work in Hugs, does. That's using the legitimate= distro version of Hugs Sep2006. Possibly Hugs changed after 2004 when the = HList work was reported. (In Section 6 of the paper "We give up on per= suading Hugs." so I guess they didn't explore further.)</div><div = dir=3D"auto"><br></div><div dir=3D"auto">That is, the Section 9 implementat= ion exhibits the 'eager' type unification, whether or not I declare= TypeCast in a separate module and "import it at a higher level in the= module hierarchy" [Section 9]. That is, if I'm doing that right: = what does "separate compilation" mean in context of Hugs? It'= s an interpreter not a compiler; it doesn't produce executables/object = code. Indeed if you import a library -- even one of the standard Report-def= ined libraries, it goes and gets the library source and compiles that along= side the client program. There's no Haskell interface/.hi files that I = can see(?)</div><div dir=3D"auto"><br></div><div dir=3D"auto">Oh, and there= 's another advantage to avoiding separate compilation: Hugs can see all= the instances and their constraints (and instances of the constraint class= es) across all the modules. So no 'orphan instances' -- the problem= s with which were amongst the reasons for Section 6 'Overlapping banned= '. "we do not want to depend on the doubtful future of overlapping= instances in general ... GHC's instance selection is lazy, whereas Hug= s' is eager".</div><div dir=3D"auto"><br></div><div dir=3D"auto">T= his leads the paper on to "what's known as the Data.Typeable appro= ach at the type level". But the cure is worse than the disease! It'= ;s just not scalable and not workable. So the version of HList that has per= sisted to this day does use the combo of Fundeps + Overlaps, and despite th= e paper's misgivings, that has persistently been stable in GHC. No &quo= t;doubtful future" after a dozen years.</div><div dir=3D"auto"><br></d= iv><div dir=3D"auto">To pick up a misrepresentation: "GHC's instan= ce selection is lazy": no, GHC's validation of overlapping instanc= es is lazy; but its selection is eager, too eager: it commits to an instanc= e inside each module, ignoring the possibility this module is imported into= another with an overlapping module which is a better fit. Whereas the alle= ged "Hugs' is eager" is also opposite to the truth: Hugs'= selection of an instance is delayed as much as possible until it's sur= e there's only one fit (it can see all instances in all imports). Valid= ation of overlap is eager: instances (heads) must be in strict substitution= sequence. That's often a nuisance, but a price I'm prepared to pay= to get better coherence.</div><div dir=3D"auto"><br></div><div dir=3D"auto= ">'Orphan instances' (and overlap thereof) are certainly a danger i= n GHC. Avoiding them was part of the motivation for Closed Type Families to= be grouped in a single syntactic unit/in a single module. And yet GHC know= s how to defer instance selection if there's no unique/suitable instanc= e visible in a module. Why can't it do that everywhere? Or at least war= n if imports contain instances that are overlapped in a different module.</= div><div dir=3D"auto"><br></div><div dir=3D"auto">Then it seems to me:</div= ><div dir=3D"auto">* not only does GHC have a "bogus" implementat= ion of the FunDep consistency rule; but also</div><div dir=3D"auto">* GHC&#= 39;s implementation of Overlaps is broken.</div><div dir=3D"auto"><br></div= ><div dir=3D"auto">Hugs' implementation of both is a lot more restricti= ve, and more coherent. I'm not finding it prevents any programs. It doe= s require I structure them in specific ways.</div><div dir=3D"auto"><br></d= iv><div dir=3D"auto"><br></div><div dir=3D"auto">AntC</div><div dir=3D"auto= "><br></div><div dir=3D"auto"><br></div><div dir=3D"auto">[*] Strongly Type= d Heterogeneous Collections 2004, Oleg Kiselyov, Ralf L=C3=A4mmel, Keean Sc= hupke</div> --000000000000a9f23205775192d2-- --===============0349836246219615252== Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: base64 Content-Disposition: inline X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KSHVncy1Vc2Vy cyBtYWlsaW5nIGxpc3QKSHVncy1Vc2Vyc0BoYXNrZWxsLm9yZwpodHRwOi8vbWFpbC5oYXNrZWxs Lm9yZy9jZ2ktYmluL21haWxtYW4vbGlzdGluZm8vaHVncy11c2Vycwo= --===============0349836246219615252==--