diff --git a/COPYING b/COPYING new file mode 100644 --- /dev/null +++ b/COPYING @@ -0,0 +1,674 @@ + GNU GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The GNU General Public License is a free, copyleft license for +software and other kinds of works. + + The licenses for most software and other practical works are designed +to take away your freedom to share and change the works. By contrast, +the GNU General Public License is intended to guarantee your freedom to +share and change all versions of a program--to make sure it remains free +software for all its users. We, the Free Software Foundation, use the +GNU General Public License for most of our software; it applies also to +any other work released this way by its authors. You can apply it to +your programs, too. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +them if you wish), that you receive source code or can get it if you +want it, that you can change the software or use pieces of it in new +free programs, and that you know you can do these things. + + To protect your rights, we need to prevent others from denying you +these rights or asking you to surrender the rights. Therefore, you have +certain responsibilities if you distribute copies of the software, or if +you modify it: responsibilities to respect the freedom of others. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must pass on to the recipients the same +freedoms that you received. You must make sure that they, too, receive +or can get the source code. And you must show them these terms so they +know their rights. + + Developers that use the GNU GPL protect your rights with two steps: +(1) assert copyright on the software, and (2) offer you this License +giving you legal permission to copy, distribute and/or modify it. + + For the developers' and authors' protection, the GPL clearly explains +that there is no warranty for this free software. For both users' and +authors' sake, the GPL requires that modified versions be marked as +changed, so that their problems will not be attributed erroneously to +authors of previous versions. + + Some devices are designed to deny users access to install or run +modified versions of the software inside them, although the manufacturer +can do so. This is fundamentally incompatible with the aim of +protecting users' freedom to change the software. The systematic +pattern of such abuse occurs in the area of products for individuals to +use, which is precisely where it is most unacceptable. Therefore, we +have designed this version of the GPL to prohibit the practice for those +products. If such problems arise substantially in other domains, we +stand ready to extend this provision to those domains in future versions +of the GPL, as needed to protect the freedom of users. + + Finally, every program is threatened constantly by software patents. +States should not allow patents to restrict development and use of +software on general-purpose computers, but in those that do, we wish to +avoid the special danger that patents applied to a free program could +make it effectively proprietary. To prevent this, the GPL assures that +patents cannot be used to render the program non-free. + + The precise terms and conditions for copying, distribution and +modification follow. + + TERMS AND CONDITIONS + + 0. Definitions. + + "This License" refers to version 3 of the GNU General Public License. + + "Copyright" also means copyright-like laws that apply to other kinds of +works, such as semiconductor masks. + + "The Program" refers to any copyrightable work licensed under this +License. Each licensee is addressed as "you". "Licensees" and +"recipients" may be individuals or organizations. + + To "modify" a work means to copy from or adapt all or part of the work +in a fashion requiring copyright permission, other than the making of an +exact copy. The resulting work is called a "modified version" of the +earlier work or a work "based on" the earlier work. + + A "covered work" means either the unmodified Program or a work based +on the Program. + + To "propagate" a work means to do anything with it that, without +permission, would make you directly or secondarily liable for +infringement under applicable copyright law, except executing it on a +computer or modifying a private copy. Propagation includes copying, +distribution (with or without modification), making available to the +public, and in some countries other activities as well. + + To "convey" a work means any kind of propagation that enables other +parties to make or receive copies. Mere interaction with a user through +a computer network, with no transfer of a copy, is not conveying. + + An interactive user interface displays "Appropriate Legal Notices" +to the extent that it includes a convenient and prominently visible +feature that (1) displays an appropriate copyright notice, and (2) +tells the user that there is no warranty for the work (except to the +extent that warranties are provided), that licensees may convey the +work under this License, and how to view a copy of this License. If +the interface presents a list of user commands or options, such as a +menu, a prominent item in the list meets this criterion. + + 1. Source Code. + + The "source code" for a work means the preferred form of the work +for making modifications to it. "Object code" means any non-source +form of a work. + + A "Standard Interface" means an interface that either is an official +standard defined by a recognized standards body, or, in the case of +interfaces specified for a particular programming language, one that +is widely used among developers working in that language. + + The "System Libraries" of an executable work include anything, other +than the work as a whole, that (a) is included in the normal form of +packaging a Major Component, but which is not part of that Major +Component, and (b) serves only to enable use of the work with that +Major Component, or to implement a Standard Interface for which an +implementation is available to the public in source code form. A +"Major Component", in this context, means a major essential component +(kernel, window system, and so on) of the specific operating system +(if any) on which the executable work runs, or a compiler used to +produce the work, or an object code interpreter used to run it. + + The "Corresponding Source" for a work in object code form means all +the source code needed to generate, install, and (for an executable +work) run the object code and to modify the work, including scripts to +control those activities. However, it does not include the work's +System Libraries, or general-purpose tools or generally available free +programs which are used unmodified in performing those activities but +which are not part of the work. For example, Corresponding Source +includes interface definition files associated with source files for +the work, and the source code for shared libraries and dynamically +linked subprograms that the work is specifically designed to require, +such as by intimate data communication or control flow between those +subprograms and other parts of the work. + + The Corresponding Source need not include anything that users +can regenerate automatically from other parts of the Corresponding +Source. + + The Corresponding Source for a work in source code form is that +same work. + + 2. Basic Permissions. + + All rights granted under this License are granted for the term of +copyright on the Program, and are irrevocable provided the stated +conditions are met. This License explicitly affirms your unlimited +permission to run the unmodified Program. The output from running a +covered work is covered by this License only if the output, given its +content, constitutes a covered work. This License acknowledges your +rights of fair use or other equivalent, as provided by copyright law. + + You may make, run and propagate covered works that you do not +convey, without conditions so long as your license otherwise remains +in force. You may convey covered works to others for the sole purpose +of having them make modifications exclusively for you, or provide you +with facilities for running those works, provided that you comply with +the terms of this License in conveying all material for which you do +not control copyright. Those thus making or running the covered works +for you must do so exclusively on your behalf, under your direction +and control, on terms that prohibit them from making any copies of +your copyrighted material outside their relationship with you. + + Conveying under any other circumstances is permitted solely under +the conditions stated below. Sublicensing is not allowed; section 10 +makes it unnecessary. + + 3. Protecting Users' Legal Rights From Anti-Circumvention Law. + + No covered work shall be deemed part of an effective technological +measure under any applicable law fulfilling obligations under article +11 of the WIPO copyright treaty adopted on 20 December 1996, or +similar laws prohibiting or restricting circumvention of such +measures. + + When you convey a covered work, you waive any legal power to forbid +circumvention of technological measures to the extent such circumvention +is effected by exercising rights under this License with respect to +the covered work, and you disclaim any intention to limit operation or +modification of the work as a means of enforcing, against the work's +users, your or third parties' legal rights to forbid circumvention of +technological measures. + + 4. Conveying Verbatim Copies. + + You may convey verbatim copies of the Program's source code as you +receive it, in any medium, provided that you conspicuously and +appropriately publish on each copy an appropriate copyright notice; +keep intact all notices stating that this License and any +non-permissive terms added in accord with section 7 apply to the code; +keep intact all notices of the absence of any warranty; and give all +recipients a copy of this License along with the Program. + + You may charge any price or no price for each copy that you convey, +and you may offer support or warranty protection for a fee. + + 5. Conveying Modified Source Versions. + + You may convey a work based on the Program, or the modifications to +produce it from the Program, in the form of source code under the +terms of section 4, provided that you also meet all of these conditions: + + a) The work must carry prominent notices stating that you modified + it, and giving a relevant date. + + b) The work must carry prominent notices stating that it is + released under this License and any conditions added under section + 7. This requirement modifies the requirement in section 4 to + "keep intact all notices". + + c) You must license the entire work, as a whole, under this + License to anyone who comes into possession of a copy. This + License will therefore apply, along with any applicable section 7 + additional terms, to the whole of the work, and all its parts, + regardless of how they are packaged. This License gives no + permission to license the work in any other way, but it does not + invalidate such permission if you have separately received it. + + d) If the work has interactive user interfaces, each must display + Appropriate Legal Notices; however, if the Program has interactive + interfaces that do not display Appropriate Legal Notices, your + work need not make them do so. + + A compilation of a covered work with other separate and independent +works, which are not by their nature extensions of the covered work, +and which are not combined with it such as to form a larger program, +in or on a volume of a storage or distribution medium, is called an +"aggregate" if the compilation and its resulting copyright are not +used to limit the access or legal rights of the compilation's users +beyond what the individual works permit. Inclusion of a covered work +in an aggregate does not cause this License to apply to the other +parts of the aggregate. + + 6. Conveying Non-Source Forms. + + You may convey a covered work in object code form under the terms +of sections 4 and 5, provided that you also convey the +machine-readable Corresponding Source under the terms of this License, +in one of these ways: + + a) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by the + Corresponding Source fixed on a durable physical medium + customarily used for software interchange. + + b) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by a + written offer, valid for at least three years and valid for as + long as you offer spare parts or customer support for that product + model, to give anyone who possesses the object code either (1) a + copy of the Corresponding Source for all the software in the + product that is covered by this License, on a durable physical + medium customarily used for software interchange, for a price no + more than your reasonable cost of physically performing this + conveying of source, or (2) access to copy the + Corresponding Source from a network server at no charge. + + c) Convey individual copies of the object code with a copy of the + written offer to provide the Corresponding Source. This + alternative is allowed only occasionally and noncommercially, and + only if you received the object code with such an offer, in accord + with subsection 6b. + + d) Convey the object code by offering access from a designated + place (gratis or for a charge), and offer equivalent access to the + Corresponding Source in the same way through the same place at no + further charge. You need not require recipients to copy the + Corresponding Source along with the object code. If the place to + copy the object code is a network server, the Corresponding Source + may be on a different server (operated by you or a third party) + that supports equivalent copying facilities, provided you maintain + clear directions next to the object code saying where to find the + Corresponding Source. Regardless of what server hosts the + Corresponding Source, you remain obligated to ensure that it is + available for as long as needed to satisfy these requirements. + + e) Convey the object code using peer-to-peer transmission, provided + you inform other peers where the object code and Corresponding + Source of the work are being offered to the general public at no + charge under subsection 6d. + + A separable portion of the object code, whose source code is excluded +from the Corresponding Source as a System Library, need not be +included in conveying the object code work. + + A "User Product" is either (1) a "consumer product", which means any +tangible personal property which is normally used for personal, family, +or household purposes, or (2) anything designed or sold for incorporation +into a dwelling. In determining whether a product is a consumer product, +doubtful cases shall be resolved in favor of coverage. For a particular +product received by a particular user, "normally used" refers to a +typical or common use of that class of product, regardless of the status +of the particular user or of the way in which the particular user +actually uses, or expects or is expected to use, the product. A product +is a consumer product regardless of whether the product has substantial +commercial, industrial or non-consumer uses, unless such uses represent +the only significant mode of use of the product. + + "Installation Information" for a User Product means any methods, +procedures, authorization keys, or other information required to install +and execute modified versions of a covered work in that User Product from +a modified version of its Corresponding Source. The information must +suffice to ensure that the continued functioning of the modified object +code is in no case prevented or interfered with solely because +modification has been made. + + If you convey an object code work under this section in, or with, or +specifically for use in, a User Product, and the conveying occurs as +part of a transaction in which the right of possession and use of the +User Product is transferred to the recipient in perpetuity or for a +fixed term (regardless of how the transaction is characterized), the +Corresponding Source conveyed under this section must be accompanied +by the Installation Information. But this requirement does not apply +if neither you nor any third party retains the ability to install +modified object code on the User Product (for example, the work has +been installed in ROM). + + The requirement to provide Installation Information does not include a +requirement to continue to provide support service, warranty, or updates +for a work that has been modified or installed by the recipient, or for +the User Product in which it has been modified or installed. Access to a +network may be denied when the modification itself materially and +adversely affects the operation of the network or violates the rules and +protocols for communication across the network. + + Corresponding Source conveyed, and Installation Information provided, +in accord with this section must be in a format that is publicly +documented (and with an implementation available to the public in +source code form), and must require no special password or key for +unpacking, reading or copying. + + 7. Additional Terms. + + "Additional permissions" are terms that supplement the terms of this +License by making exceptions from one or more of its conditions. +Additional permissions that are applicable to the entire Program shall +be treated as though they were included in this License, to the extent +that they are valid under applicable law. If additional permissions +apply only to part of the Program, that part may be used separately +under those permissions, but the entire Program remains governed by +this License without regard to the additional permissions. + + When you convey a copy of a covered work, you may at your option +remove any additional permissions from that copy, or from any part of +it. (Additional permissions may be written to require their own +removal in certain cases when you modify the work.) You may place +additional permissions on material, added by you to a covered work, +for which you have or can give appropriate copyright permission. + + Notwithstanding any other provision of this License, for material you +add to a covered work, you may (if authorized by the copyright holders of +that material) supplement the terms of this License with terms: + + a) Disclaiming warranty or limiting liability differently from the + terms of sections 15 and 16 of this License; or + + b) Requiring preservation of specified reasonable legal notices or + author attributions in that material or in the Appropriate Legal + Notices displayed by works containing it; or + + c) Prohibiting misrepresentation of the origin of that material, or + requiring that modified versions of such material be marked in + reasonable ways as different from the original version; or + + d) Limiting the use for publicity purposes of names of licensors or + authors of the material; or + + e) Declining to grant rights under trademark law for use of some + trade names, trademarks, or service marks; or + + f) Requiring indemnification of licensors and authors of that + material by anyone who conveys the material (or modified versions of + it) with contractual assumptions of liability to the recipient, for + any liability that these contractual assumptions directly impose on + those licensors and authors. + + All other non-permissive additional terms are considered "further +restrictions" within the meaning of section 10. If the Program as you +received it, or any part of it, contains a notice stating that it is +governed by this License along with a term that is a further +restriction, you may remove that term. If a license document contains +a further restriction but permits relicensing or conveying under this +License, you may add to a covered work material governed by the terms +of that license document, provided that the further restriction does +not survive such relicensing or conveying. + + If you add terms to a covered work in accord with this section, you +must place, in the relevant source files, a statement of the +additional terms that apply to those files, or a notice indicating +where to find the applicable terms. + + Additional terms, permissive or non-permissive, may be stated in the +form of a separately written license, or stated as exceptions; +the above requirements apply either way. + + 8. Termination. + + You may not propagate or modify a covered work except as expressly +provided under this License. Any attempt otherwise to propagate or +modify it is void, and will automatically terminate your rights under +this License (including any patent licenses granted under the third +paragraph of section 11). + + However, if you cease all violation of this License, then your +license from a particular copyright holder is reinstated (a) +provisionally, unless and until the copyright holder explicitly and +finally terminates your license, and (b) permanently, if the copyright +holder fails to notify you of the violation by some reasonable means +prior to 60 days after the cessation. + + Moreover, your license from a particular copyright holder is +reinstated permanently if the copyright holder notifies you of the +violation by some reasonable means, this is the first time you have +received notice of violation of this License (for any work) from that +copyright holder, and you cure the violation prior to 30 days after +your receipt of the notice. + + Termination of your rights under this section does not terminate the +licenses of parties who have received copies or rights from you under +this License. If your rights have been terminated and not permanently +reinstated, you do not qualify to receive new licenses for the same +material under section 10. + + 9. Acceptance Not Required for Having Copies. + + You are not required to accept this License in order to receive or +run a copy of the Program. Ancillary propagation of a covered work +occurring solely as a consequence of using peer-to-peer transmission +to receive a copy likewise does not require acceptance. However, +nothing other than this License grants you permission to propagate or +modify any covered work. These actions infringe copyright if you do +not accept this License. Therefore, by modifying or propagating a +covered work, you indicate your acceptance of this License to do so. + + 10. Automatic Licensing of Downstream Recipients. + + Each time you convey a covered work, the recipient automatically +receives a license from the original licensors, to run, modify and +propagate that work, subject to this License. You are not responsible +for enforcing compliance by third parties with this License. + + An "entity transaction" is a transaction transferring control of an +organization, or substantially all assets of one, or subdividing an +organization, or merging organizations. If propagation of a covered +work results from an entity transaction, each party to that +transaction who receives a copy of the work also receives whatever +licenses to the work the party's predecessor in interest had or could +give under the previous paragraph, plus a right to possession of the +Corresponding Source of the work from the predecessor in interest, if +the predecessor has it or can get it with reasonable efforts. + + You may not impose any further restrictions on the exercise of the +rights granted or affirmed under this License. For example, you may +not impose a license fee, royalty, or other charge for exercise of +rights granted under this License, and you may not initiate litigation +(including a cross-claim or counterclaim in a lawsuit) alleging that +any patent claim is infringed by making, using, selling, offering for +sale, or importing the Program or any portion of it. + + 11. Patents. + + A "contributor" is a copyright holder who authorizes use under this +License of the Program or a work on which the Program is based. The +work thus licensed is called the contributor's "contributor version". + + A contributor's "essential patent claims" are all patent claims +owned or controlled by the contributor, whether already acquired or +hereafter acquired, that would be infringed by some manner, permitted +by this License, of making, using, or selling its contributor version, +but do not include claims that would be infringed only as a +consequence of further modification of the contributor version. For +purposes of this definition, "control" includes the right to grant +patent sublicenses in a manner consistent with the requirements of +this License. + + Each contributor grants you a non-exclusive, worldwide, royalty-free +patent license under the contributor's essential patent claims, to +make, use, sell, offer for sale, import and otherwise run, modify and +propagate the contents of its contributor version. + + In the following three paragraphs, a "patent license" is any express +agreement or commitment, however denominated, not to enforce a patent +(such as an express permission to practice a patent or covenant not to +sue for patent infringement). To "grant" such a patent license to a +party means to make such an agreement or commitment not to enforce a +patent against the party. + + If you convey a covered work, knowingly relying on a patent license, +and the Corresponding Source of the work is not available for anyone +to copy, free of charge and under the terms of this License, through a +publicly available network server or other readily accessible means, +then you must either (1) cause the Corresponding Source to be so +available, or (2) arrange to deprive yourself of the benefit of the +patent license for this particular work, or (3) arrange, in a manner +consistent with the requirements of this License, to extend the patent +license to downstream recipients. "Knowingly relying" means you have +actual knowledge that, but for the patent license, your conveying the +covered work in a country, or your recipient's use of the covered work +in a country, would infringe one or more identifiable patents in that +country that you have reason to believe are valid. + + If, pursuant to or in connection with a single transaction or +arrangement, you convey, or propagate by procuring conveyance of, a +covered work, and grant a patent license to some of the parties +receiving the covered work authorizing them to use, propagate, modify +or convey a specific copy of the covered work, then the patent license +you grant is automatically extended to all recipients of the covered +work and works based on it. + + A patent license is "discriminatory" if it does not include within +the scope of its coverage, prohibits the exercise of, or is +conditioned on the non-exercise of one or more of the rights that are +specifically granted under this License. You may not convey a covered +work if you are a party to an arrangement with a third party that is +in the business of distributing software, under which you make payment +to the third party based on the extent of your activity of conveying +the work, and under which the third party grants, to any of the +parties who would receive the covered work from you, a discriminatory +patent license (a) in connection with copies of the covered work +conveyed by you (or copies made from those copies), or (b) primarily +for and in connection with specific products or compilations that +contain the covered work, unless you entered into that arrangement, +or that patent license was granted, prior to 28 March 2007. + + Nothing in this License shall be construed as excluding or limiting +any implied license or other defenses to infringement that may +otherwise be available to you under applicable patent law. + + 12. No Surrender of Others' Freedom. + + If conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot convey a +covered work so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you may +not convey it at all. For example, if you agree to terms that obligate you +to collect a royalty for further conveying from those to whom you convey +the Program, the only way you could satisfy both those terms and this +License would be to refrain entirely from conveying the Program. + + 13. Use with the GNU Affero General Public License. + + Notwithstanding any other provision of this License, you have +permission to link or combine any covered work with a work licensed +under version 3 of the GNU Affero General Public License into a single +combined work, and to convey the resulting work. The terms of this +License will continue to apply to the part which is the covered work, +but the special requirements of the GNU Affero General Public License, +section 13, concerning interaction through a network will apply to the +combination as such. + + 14. Revised Versions of this License. + + The Free Software Foundation may publish revised and/or new versions of +the GNU General Public License from time to time. Such new versions will +be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + + Each version is given a distinguishing version number. If the +Program specifies that a certain numbered version of the GNU General +Public License "or any later version" applies to it, you have the +option of following the terms and conditions either of that numbered +version or of any later version published by the Free Software +Foundation. If the Program does not specify a version number of the +GNU General Public License, you may choose any version ever published +by the Free Software Foundation. + + If the Program specifies that a proxy can decide which future +versions of the GNU General Public License can be used, that proxy's +public statement of acceptance of a version permanently authorizes you +to choose that version for the Program. + + Later license versions may give you additional or different +permissions. However, no additional obligations are imposed on any +author or copyright holder as a result of your choosing to follow a +later version. + + 15. Disclaimer of Warranty. + + THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY +APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT +HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY +OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM +IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF +ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. Limitation of Liability. + + IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS +THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY +GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE +USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF +DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD +PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), +EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF +SUCH DAMAGES. + + 17. Interpretation of Sections 15 and 16. + + If the disclaimer of warranty and limitation of liability provided +above cannot be given local legal effect according to their terms, +reviewing courts shall apply local law that most closely approximates +an absolute waiver of all civil liability in connection with the +Program, unless a warranty or assumption of liability accompanies a +copy of the Program in return for a fee. + + END OF TERMS AND CONDITIONS + + How to Apply These Terms to Your New Programs + + If you develop a new program, and you want it to be of the greatest +possible use to the public, the best way to achieve this is to make it +free software which everyone can redistribute and change under these terms. + + To do so, attach the following notices to the program. It is safest +to attach them to the start of each source file to most effectively +state the exclusion of warranty; and each file should have at least +the "copyright" line and a pointer to where the full notice is found. + + + Copyright (C) + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see . + +Also add information on how to contact you by electronic and paper mail. + + If the program does terminal interaction, make it output a short +notice like this when it starts in an interactive mode: + + Copyright (C) + This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'. + This is free software, and you are welcome to redistribute it + under certain conditions; type `show c' for details. + +The hypothetical commands `show w' and `show c' should show the appropriate +parts of the General Public License. Of course, your program's commands +might be different; for a GUI interface, you would use an "about box". + + You should also get your employer (if you work as a programmer) or school, +if any, to sign a "copyright disclaimer" for the program, if necessary. +For more information on this, and how to apply and follow the GNU GPL, see +. + + The GNU General Public License does not permit incorporating your program +into proprietary programs. If your program is a subroutine library, you +may consider it more useful to permit linking proprietary applications with +the library. If this is what you want to do, use the GNU Lesser General +Public License instead of this License. But first, please read +. diff --git a/Language/LOL/Typing.hs b/Language/LOL/Typing.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing.hs @@ -0,0 +1,29 @@ +-- | Type inferencer for LOL (λω language). +-- +-- __Ressources:__ +-- +-- * /Top Quality Type Error Messages/, Bastiaan Heeren, 2005, +-- http://www.open.ou.nl/bhr/TopQuality.pdf +-- +-- * /Interpreting types as abstract values: a tutorial on Hindley-Milner type inference/, +-- Oleg Kiselyov, Chung-chieh Shan, 2008, +-- http://okmij.org/ftp/Haskell/AlgorithmsH.html#teval +-- +-- * /Compositional Type Checking for Hindley-Milner Type Systems with Ad-hoc Polymorphism/, +-- Gergő Érdi, 2011, +-- https://gergo.erdi.hu/projects/tandoori/Tandoori-Compositional-Typeclass.pdf +-- +-- All submodules, in a topological order. +module Language.LOL.Typing + ( module Language.LOL.Typing.Type + , module Language.LOL.Typing.Solver + , module Language.LOL.Typing.Constraint + , module Language.LOL.Typing.Collect + , module Language.LOL.Typing.Expr + ) where + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Solver +import Language.LOL.Typing.Constraint +import Language.LOL.Typing.Collect +import Language.LOL.Typing.Expr diff --git a/Language/LOL/Typing/Collect.hs b/Language/LOL/Typing/Collect.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Collect.hs @@ -0,0 +1,6 @@ +-- | All submodules, in a topological order. +module Language.LOL.Typing.Collect + ( module Language.LOL.Typing.Collect.Constraint + ) where + +import Language.LOL.Typing.Collect.Constraint diff --git a/Language/LOL/Typing/Collect/Constraint.hs b/Language/LOL/Typing/Collect/Constraint.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Collect/Constraint.hs @@ -0,0 +1,174 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +module Language.LOL.Typing.Collect.Constraint where + +-- vim: ft=haskell +-- import Data.Bool +-- import Data.Defaults (Defaults(..)) +import Data.Either (Either(..)) +import Data.Eq (Eq(..)) +import Data.Function (($), (.)) +import Data.Functor ((<$>)) +import qualified Data.List as List +import qualified Data.Foldable as Foldable +import Data.Maybe (Maybe(..)) +import Data.Monoid (Monoid(..), (<>)) +import Data.Text (Text) +import Data.Text.Buildable (Buildable(..)) +import Data.Tuple (fst, snd) +import Text.Show (Show(..)) +import Data.Sequence (Seq) +import qualified Data.Sequence as Seq + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Expr +import Language.LOL.Typing.Solver +import Language.LOL.Typing.Constraint +import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build + +-- * Type 'Collect_Context' + +-- | A 'Polytyref' substitution. +type Collect_Context = [(Name, Polytyref)] + +-- * Type 'Collect_Constraint' + +type Collect_Constraint + = Constraint_Either + Constraint_Monotype + Constraint_Polytype + Collect_Infos + +-- | Build a 'Constraint_Monotype_Unification' lifted into 'Collect_Constraint'. +unifies_with + :: (Monotypeable x, Monotypeable y) + => x -> y + -> Collect_Info_Grammar -> Collect_Constraint +unifies_with x y info = + Constraint_Either $ Left $ + Constraint_Monotype_Unification (monotype x) (monotype y) $ + Collect_Infos [Collect_Info_Grammar info] + +-- | Build a 'Constraint_Polytype_instantiates_to_Monotype' lifted into 'Collect_Constraint'. +instantiates_to + :: (Polytyrefable polyty, Monotypeable monoty) + => polyty -> monoty + -> Collect_Info_Grammar -> Collect_Constraint +instantiates_to p m info = + Constraint_Either $ Right $ + Constraint_Polytype_instantiates_to_Monotype (polytyref p) (monotype m) $ + Collect_Infos [Collect_Info_Grammar info] + +-- | Build a 'Constraint_Polytype_generalizes_from_Monotype' lifted into 'Collect_Constraint'. +generalizes_from + :: Monotypeable monoty + => Polyvar -> monoty -> Collect_Context + -> Collect_Info_Grammar -> Collect_Constraint +generalizes_from p m ctx info = + Constraint_Either $ Right $ + Constraint_Polytype_generalizes_from_Monotype + p (context_rigtypes ctx, monotype m) $ + Collect_Infos [Collect_Info_Grammar info] + +-- | Build a 'Constraint_Polytype_generalized_by_Monotype' lifted into 'Collect_Constraint'. +generalized_by + :: (Polytyrefable polyty, Monotypeable monoty) + => polyty -> monoty -> Collect_Context + -> Collect_Info_Grammar -> Collect_Constraint +generalized_by p m ctx info = + Constraint_Either $ Right $ + Constraint_Polytype_generalized_by_Monotype + (context_rigtypes ctx, polytyref p) (monotype m) $ + Collect_Infos [Collect_Info_Grammar info] + +-- * Type 'Collect_Info' + +data Collect_Info + = Collect_Info_Solver (Solver_Info Collect_Infos) + | Collect_Info_Grammar Collect_Info_Grammar + deriving (Eq, Show) +newtype Collect_Infos + = Collect_Infos [Collect_Info] + deriving (Eq, Show) + +instance Infoable Info_Monotype Collect_Infos where + info_insert i (Collect_Infos is) = + Collect_Infos $ + ( Collect_Info_Solver $ Solver_Info_Monotype i + ) : is +instance Infoable Info_Polytype Collect_Infos where + info_insert i (Collect_Infos is) = + Collect_Infos $ + ( Collect_Info_Solver $ Solver_Info_Polytype i + ) : is +instance Infoable (Info_Class Collect_Infos) Collect_Infos where + info_insert i (Collect_Infos is) = + Collect_Infos $ + ( Collect_Info_Solver $ Solver_Info_Class i + ) : is + +instance Buildable Collect_Infos where + build (Collect_Infos is) = Build.list is +instance Buildable Collect_Info where + build x = + case x of + Collect_Info_Solver i -> build i + Collect_Info_Grammar i -> build i + +-- ** Type 'Collect_Info_Grammar' + +data Collect_Info_Grammar + = Collect_Info_Grammar_Expr Text + deriving (Eq, Show) +instance Buildable Collect_Info_Grammar where + build x = + case x of + Collect_Info_Grammar_Expr t -> build t + +-- * Type 'Collect_Error' + +data Collect_Error info err + = Collect_Error_Solver [(info, err)] + | Collect_Error_Grammar [Collect_Error_Grammar] + deriving (Eq, Show) + +-- ** Type 'Collect_Error_Grammar' + +data Collect_Error_Grammar + = Collect_Error_Grammar_Variable_not_in_scope Text + deriving (Eq, Show) + +context_insert :: Polytyrefable a => Name -> a -> Collect_Context -> Collect_Context +context_insert i p = ((i, polytyref p) :) + +context_lookup :: Name -> Collect_Context -> Maybe Polytyref +context_lookup = List.lookup + +context_rigtypes :: Collect_Context -> [Rigtype] +context_rigtypes ctx = Monotype_Var <$> subvars (snd <$> ctx) + +hussel :: Seq Collect_Constraint -> Seq Collect_Constraint +hussel = (\(as, bs) -> (snd <$> bs) <> as) . go mempty + where + go :: Seq Polyvar -> Seq Collect_Constraint + -> (Seq Collect_Constraint, Seq (Polyvar, Collect_Constraint)) + go polyvars cs = + case Seq.viewl cs of + Seq.EmptyL -> mempty + (c@(Constraint_Either e) Seq.:< rest) -> + case e of + Right (Constraint_Polytype_instantiates_to_Monotype (Polytyref_Var var) _ _) -> + let (new, gs) = go (var Seq.<| polyvars) rest in + let (gs1, gs2) = Seq.partition ((`Foldable.elem` polyvars) . fst) gs in + ((snd <$> gs2)<>Seq.singleton c<>new, gs1) + Right (Constraint_Polytype_generalizes_from_Monotype var _ _) + | var `Foldable.elem` polyvars -> + let (new, gs) = go polyvars rest in + (new, (var,c) Seq.<| gs) + _ -> + let (new, gs) = go polyvars rest in + let (gs1, gs2) = Seq.partition ((`Foldable.elem` polyvars) . fst) gs in + ((snd <$> gs2)<>Seq.singleton c<>new, gs1) diff --git a/Language/LOL/Typing/Collect/Grammar.ag b/Language/LOL/Typing/Collect/Grammar.ag new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Collect/Grammar.ag @@ -0,0 +1,129 @@ +-- vim: syntax=haskell +optpragmas { +{-# LANGUAGE OverloadedStrings #-} +} +module {Language.LOL.Typing.Collect.Grammar} {} { +import Data.Function (($)) +import Data.Maybe (Maybe(..), maybe) +import Data.Monoid (Monoid(..), (<>)) +import Data.Sequence (Seq, (|>), (<|), (><)) +import qualified Data.Sequence as Seq +import Prelude (Num(..)) + +import Language.LOL.Typing.Collect.Constraint +import Language.LOL.Typing.Type +import Language.LOL.Typing.Expr +import Language.LOL.Typing.Lib.Data.Default (Default(..)) +import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build +} + +include "../Expr/Grammar.ag" + +attr Expr + -- | top-down + inh polytys :: Collect_Context + -- | bottom-up + syn monovar :: Monovar + syn constraints :: {Seq Collect_Constraint} + syn errors use {<>} {[]} :: {[Collect_Error_Grammar]} + -- | both + chn freshvar :: Freshvar +attr Decl + -- | top-down + inh polytys :: Collect_Context + -- | bottom-up + syn polyvar :: Polyvar + syn constraints :: {Seq Collect_Constraint} + syn errors use {<>} {[]} :: {[Collect_Error_Grammar]} + -- | both + chn freshvar :: Freshvar + +sem Expr + | Annot + lhs.constraints = @body.constraints |> + ((@sig `generalized_by` @body.monovar) @lhs.polytys $ + Collect_Info_Grammar_Expr $ "Annot " <> Build.text + (def::Quantification_Build_Options, @sig)) + | Var + lhs.monovar = @loc.monovar + loc.monovar = @lhs.freshvar + lhs.freshvar = @lhs.freshvar + 1 + loc.polyty = context_lookup @name @lhs.polytys + -- loc.term = TeTy_Var_Unknown @name @loc.monovar + lhs.constraints = case @loc.polyty of + Nothing -> mempty + Just p -> Seq.singleton $ + p `instantiates_to` @loc.monovar $ + Collect_Info_Grammar_Expr $ "Var " <> @name + lhs.errors = case @loc.polyty of + Nothing -> [Collect_Error_Grammar_Variable_not_in_scope @name] + Just _ -> [] + | Abst + lhs.monovar = @loc.monovar + loc.monovar = @lhs.freshvar + loc.arg_monovar = @lhs.freshvar + 1 + body.freshvar = @lhs.freshvar + 2 + body.polytys = (@name `context_insert` Monotype_Var @loc.arg_monovar) @lhs.polytys + lhs.constraints = (@loc.monovar `unifies_with` + (Monotype_Var @loc.arg_monovar .->. Monotype_Var @body.monovar) $ + Collect_Info_Grammar_Expr $ "Abst(body) " <> @name) <| + maybe mempty (\sig -> Seq.singleton ((sig `unifies_with` @loc.arg_monovar) $ + Collect_Info_Grammar_Expr $ "Abst(sig) " <> Build.text sig)) @sig >< + @body.constraints + | App + lhs.monovar = @loc.monovar + loc.monovar = @lhs.freshvar + abst.freshvar = @lhs.freshvar + 1 + abst.polytys = @lhs.polytys + arg.polytys = @lhs.polytys + lhs.constraints = @abst.constraints <> + @arg.constraints |> + (@abst.monovar `unifies_with` + (Monotype_Var @arg.monovar .->. Monotype_Var @loc.monovar) $ + Collect_Info_Grammar_Expr $ "App") + | Let + lhs.monovar = @loc.monovar + loc.monovar = @lhs.freshvar + loc.decl_polyvar = @lhs.freshvar + 1 + decl.freshvar = @lhs.freshvar + 2 + decl.polytys = @lhs.polytys + body.polytys = (@name `context_insert` @loc.decl_polyvar) @lhs.polytys + lhs.constraints = let info x = Collect_Info_Grammar_Expr $ "Let" <> "(" <> x <> ") " <> @name in + @decl.constraints >< + (@loc.decl_polyvar `generalizes_from` @decl.monovar) + @lhs.polytys (info "decl") <| + maybe mempty (\sig -> Seq.singleton + ((sig `generalized_by` @decl.monovar) @lhs.polytys $ + Collect_Info_Grammar_Expr $ "Let(sig) " <> + Build.text (def::Quantification_Build_Options, sig))) @sig >< + (@loc.monovar `unifies_with` @body.monovar) (info "body") <| + @body.constraints + | Where + lhs.monovar = @loc.monovar + loc.monovar = @lhs.freshvar + loc.decl_polyvar = @lhs.freshvar + 1 + body.freshvar = @lhs.freshvar + 2 + decl.polytys = @lhs.polytys + body.polytys = (@name `context_insert` @loc.decl_polyvar) @lhs.polytys + lhs.constraints = let info = Collect_Info_Grammar_Expr $ "Where " <> @name in + @decl.constraints >< + (@loc.decl_polyvar `generalizes_from` @decl.monovar) @lhs.polytys info <| + maybe mempty (\sig -> Seq.singleton ((sig `generalized_by` @decl.monovar) @lhs.polytys $ + Collect_Info_Grammar_Expr $ "Where(sig) " <> Build.text + (def::Quantification_Build_Options, sig))) @sig >< + (@loc.monovar `unifies_with` @body.monovar) info <| + @body.constraints + +sem Decl + | Let + -- loc.monovar = Monotype_Var @lhs.freshvar + loc.decl_polyvar = @lhs.freshvar + decl.freshvar = @lhs.freshvar + 1 + decl.polytys = @lhs.polytys + lhs.polyvar = @loc.decl_polyvar + lhs.constraints = let info x = Collect_Info_Grammar_Expr $ "Let" <> "(" <> x <> ") " <> @name in + @decl.constraints >< + (@loc.decl_polyvar `generalizes_from` @decl.monovar) @lhs.polytys (info "decl") <| + maybe mempty (\sig -> Seq.singleton ((sig `generalized_by` @decl.monovar) @lhs.polytys $ + Collect_Info_Grammar_Expr $ "Let(sig) " <> Build.text + (def::Quantification_Build_Options, sig))) @sig diff --git a/Language/LOL/Typing/Constraint.hs b/Language/LOL/Typing/Constraint.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Constraint.hs @@ -0,0 +1,12 @@ +-- | All submodules, in a topological order. +module Language.LOL.Typing.Constraint + ( module Language.LOL.Typing.Constraint.Monotype + , module Language.LOL.Typing.Constraint.Polytype + , module Language.LOL.Typing.Constraint.Extra + , module Language.LOL.Typing.Constraint.Either + ) where + +import Language.LOL.Typing.Constraint.Monotype +import Language.LOL.Typing.Constraint.Polytype +import Language.LOL.Typing.Constraint.Extra +import Language.LOL.Typing.Constraint.Either diff --git a/Language/LOL/Typing/Constraint/Either.hs b/Language/LOL/Typing/Constraint/Either.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Constraint/Either.hs @@ -0,0 +1,53 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +module Language.LOL.Typing.Constraint.Either where + +import Data.Either (Either(..), either) +import Data.Function (($), (.)) +import Data.Functor (Functor(..)) +import Data.Text.Buildable (Buildable(..)) +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Solver + +-- ** Type 'Constraint_Either' + +newtype Constraint_Either f g info + = Constraint_Either (Either (f info) (g info)) + deriving (Show) + +instance + ( Buildable (f info) + , Buildable (g info) + ) => Buildable (Constraint_Either f g info) where + build (Constraint_Either x) = either build build x +instance + ( Functor f + , Functor g + ) => Functor (Constraint_Either f g) where + fmap f (Constraint_Either x) = + Constraint_Either $ + either (Left . fmap f) (Right . fmap f) x +instance + ( Substitutable (f info) + , Substitutable (g info) + ) => Substitutable (Constraint_Either f g info) where + subvars (Constraint_Either x) = either subvars subvars x + substitute sub (Constraint_Either x) = + Constraint_Either $ + either + (Left . (sub `substitute`)) + (Right . (sub `substitute`)) + x +instance + ( Solvable (f info) m + , Solvable (g info) m + ) => Solvable (Constraint_Either f g info) m where + constraint_solver (Constraint_Either x) = either constraint_solver constraint_solver x + constraint_checker (Constraint_Either x) = either constraint_checker constraint_checker x diff --git a/Language/LOL/Typing/Constraint/Extra.hs b/Language/LOL/Typing/Constraint/Extra.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Constraint/Extra.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +module Language.LOL.Typing.Constraint.Extra where + +import Data.Function (($)) +import Data.Functor (Functor(..)) +import Data.Monoid ((<>)) +import Data.Text.Buildable (Buildable(..)) +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Solver + +-- * Type 'Constraint_Extra' + +data Constraint_Extra info + = Constraint_Extra_ToProve Class_Qualifier info + | Constraint_Extra_Assume Class_Qualifier info + deriving (Show) + +instance Functor Constraint_Extra where + fmap f c = + case c of + Constraint_Extra_ToProve p info -> Constraint_Extra_ToProve p (f info) + Constraint_Extra_Assume p info -> Constraint_Extra_Assume p (f info) +instance Buildable info => Buildable (Constraint_Extra info) where + build c = + case c of + Constraint_Extra_ToProve p info -> + build $ Infoed info $ "Prove (" <> build p <> ")" + Constraint_Extra_Assume p info -> + build $ Infoed info $ "Assume (" <> build p <> ")" +instance Substitutable (Constraint_Extra info) where + subvars c = + case c of + Constraint_Extra_ToProve p _ -> subvars p + Constraint_Extra_Assume p _ -> subvars p + sub `substitute` c = + case c of + Constraint_Extra_ToProve p info -> Constraint_Extra_ToProve (sub `substitute` p) info + Constraint_Extra_Assume p info -> Constraint_Extra_Assume (sub `substitute` p) info +instance + ( info ~ Info m + , Show info + , Buildable info + , Solver_Class m + ) => Solvable (Constraint_Extra info) m where + constraint_solver c = + case c of + Constraint_Extra_ToProve p info -> class_qualifier_toprove info p + Constraint_Extra_Assume p info -> class_qualifier_assume info p diff --git a/Language/LOL/Typing/Constraint/Monotype.hs b/Language/LOL/Typing/Constraint/Monotype.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Constraint/Monotype.hs @@ -0,0 +1,64 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +-- | Constraints for /monomorphic types/. +module Language.LOL.Typing.Constraint.Monotype where + +import Control.Applicative (Applicative(..)) +import Data.Eq (Eq(..)) +import Data.Function (on) +import Data.Functor (Functor(..), (<$>)) +import qualified Data.List as List +import Data.Monoid ((<>)) +import Data.Text.Buildable (Buildable(..)) +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Solver + +-- * Type 'Constraint_Monotype_Unification' + +-- | /monotype constraint/. +data Constraint_Monotype info + = Constraint_Monotype_Unification Monotype Monotype info + -- ^ A /monotype unification constraint/. + deriving (Show) + +-- | Infix alias for 'Constraint_Monotype_Unification'. +(.==.) :: Monotype -> Monotype -> info -> Constraint_Monotype info +(.==.) = Constraint_Monotype_Unification + +instance Buildable info => Buildable (Constraint_Monotype info) where + build (Constraint_Monotype_Unification t1 t2 info) = + build t1 <> " == " <> build t2 <> build_info + where + build_info = " {- " <> build info <> " -}" +instance Functor Constraint_Monotype where + fmap f (Constraint_Monotype_Unification t1 t2 info) = + Constraint_Monotype_Unification t1 t2 (f info) +instance Substitutable (Constraint_Monotype info) where + subvars (Constraint_Monotype_Unification t1 t2 _) = subvars t1 `List.union` subvars t2 + sub `substitute` (Constraint_Monotype_Unification t1 t2 info) = + Constraint_Monotype_Unification (sub `substitute` t1) (sub `substitute` t2) info +instance + ( info ~ Info m + , Show info + , Buildable info + , Solver_Constraint m + , Solver_Monotype m + , Solver_Polytype m + ) => Solvable (Constraint_Monotype info) m where + constraint_solver (Constraint_Monotype_Unification t1 t2 info) = + monotype_unify + (info_insert (Info_Monotype_Unification t1 t2) info) + t1 t2 + constraint_checker (Constraint_Monotype_Unification t1 t2 _) = do + Synotype_Substitution{synotypes} <- synotype_substitution + ((==) `on` synexpand synotypes) + <$> monotype_substitute t1 + <*> monotype_substitute t2 diff --git a/Language/LOL/Typing/Constraint/Polytype.hs b/Language/LOL/Typing/Constraint/Polytype.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Constraint/Polytype.hs @@ -0,0 +1,229 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +-- | Constraints for /parametric polymorphism/ and /type class polymorphism/. +module Language.LOL.Typing.Constraint.Polytype where + +import Control.Applicative (Applicative(..)) +import Control.Monad (forM_, join) +import Data.Function (($), (.)) +import Data.Functor (Functor(..), (<$>)) +import qualified Data.List as List +import Data.Monoid ((<>)) +import qualified Data.Sequence as Seq +import Data.Text.Buildable (Buildable(..)) +import qualified Data.Text.Lazy.Builder as Builder +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Solver +import Language.LOL.Typing.Constraint.Monotype +import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build + +-- * Type 'Constraint_Polytype' + +-- | The /polymorphism 'Constraint's/. +data Constraint_Polytype info + = Constraint_Polytype_generalizes_from_Monotype Polyvar ([Rigtype], Monotype) info + -- ^ A /polytype generalization constraint/: + -- assign a 'Polyvar' to the 'Polytype' + -- obtained by generalizing a 'Monotype' to a 'Forall' 'Quantification' + -- over all its 'subvars' except those of the given 'Rigtype's. + -- These excluded 'Rigtype's are used to avoid generalizing + -- 'Monovar's appearing in the /typing context/, + -- since they appear in 'Constraint's that /need/ to be satisfied. + -- + -- NOTE: a 'Constraint_Polytype_generalizes_from_Monotype' requires + -- that the 'Polytype'’s 'quantifiers' have at least the 'qualifiers' + -- of the 'Monotype'’s 'subvars' they generalize. See 'class_polytype_forall'. + | Constraint_Polytype_instantiates_to_Monotype Polytyref Monotype info + -- ^ A /polytype explicit instantiation constraint/ + -- (/explicit/ meaning known when collecting the 'Constraint's): + -- restricts a 'Monotype' to be /less general/ + -- than a 'Polytype' (from given 'Polytyref') + -- i.e. to be an /instance/ of it. + -- + -- NOTE: instantiating a 'Polytyref' + -- implies that the instantiated 'qualifiers' + -- are entailed by the 'qualifiers' in the solving 'Substitution'. + | Constraint_Polytype_implicit_instantiates_to_Monotype ([Rigtype], Monotype) Monotype info + -- ^ A /polytype implicit instantiation constraint/: + -- restrict a 'Monotype' to be an /instance/ of the 'Polytype' + -- obtained by 'generalize'-ing another 'Monotype' + -- over all its 'subvars' except those of the given 'Rigtype's. + -- + -- NOTE: the idea is that such a 'Constraint' + -- can be solved only if no more deductions + -- can be found in the remaining 'Constraint's ('state_constraint_constraints') + -- about the 'quantifiers' of the 'Polytype' returned by 'class_polytype_forall'. + | Constraint_Polytype_generalized_by_Monotype ([Rigtype], Polytyref) Monotype info + -- ^ A /polytype rigidification constraint/: + -- restricts a 'Monotype' to be /more general/ + -- than a 'Polytype' (from given 'Polytyref'). + -- + -- NOTE: determining this requires to know which 'Monovar's in the 'Monotype' + -- are 'Polyvar's, and which are 'Monovar's, hence + -- a set of 'Rigtype's is attached. + -- + -- NOTE: this 'Constraint' becomes important + -- to handle /expression/ with /type signature/, + -- because then the inferred 'Monotype' of the /expression/ + -- should be /more general/ than the /type signature/. + deriving (Show) + +-- | Infix alias for 'Constraint_Polytype_generalized_by_Monotype'. +(.::.) :: Monotype -> Polytyref -> [Rigtype] -> info -> Constraint_Polytype info +(.::.) monoty polyty rigtys = Constraint_Polytype_generalized_by_Monotype (rigtys, polyty) monoty + +instance Functor Constraint_Polytype where + fmap f c = + case c of + Constraint_Polytype_generalizes_from_Monotype polyty monos info -> + Constraint_Polytype_generalizes_from_Monotype polyty monos (f info) + Constraint_Polytype_instantiates_to_Monotype polyref monoty info -> + Constraint_Polytype_instantiates_to_Monotype polyref monoty (f info) + Constraint_Polytype_implicit_instantiates_to_Monotype (monotys, t2) t1 info -> + Constraint_Polytype_implicit_instantiates_to_Monotype (monotys, t2) t1 (f info) + Constraint_Polytype_generalized_by_Monotype ty pair info -> + Constraint_Polytype_generalized_by_Monotype ty pair (f info) +instance Buildable info => Buildable (Constraint_Polytype info) where + build c = + case c of + Constraint_Polytype_generalizes_from_Monotype polyty (rigtys, monoty) info -> + "p" <> build polyty + <> " := Generalize" + <> Build.tuple [build_rigvars rigtys, build monoty] + <> build_info info + Constraint_Polytype_instantiates_to_Monotype polyref monoty info -> + build monoty + <> " := Instantiate" + <> Build.tuple [build polyref] + <> build_info info + Constraint_Polytype_implicit_instantiates_to_Monotype (rigtys, polyty) monoty info -> + build monoty + <> " := Implicit" + <> Build.tuple [build_rigvars rigtys, build polyty] + <> build_info info + Constraint_Polytype_generalized_by_Monotype (rigtys, polyref) monoty info -> + build monoty + <> " := Rigidify" + <> Build.tuple [build_rigvars rigtys, build polyref] + <> build_info info + where + build_info info = " {- " <> build info <> " -}" + build_rigvars :: [Monotype] -> Builder.Builder + build_rigvars = Build.list . (Monotype_Var <$>) . subvars + +instance Substitutable (Constraint_Polytype info) where + subvars c = + case c of + Constraint_Polytype_generalizes_from_Monotype _ (rigtys, monoty) _ -> + subvars rigtys `List.union` subvars monoty + Constraint_Polytype_instantiates_to_Monotype polyref monoty _ -> + subvars monoty `List.union` subvars polyref + Constraint_Polytype_implicit_instantiates_to_Monotype (rigtys, t2) t1 _ -> + subvars t1 `List.union` subvars rigtys `List.union` subvars t2 + Constraint_Polytype_generalized_by_Monotype (rigtys, polyref) monoty _ -> + subvars monoty `List.union` subvars rigtys `List.union` subvars polyref + sub `substitute` c = + case c of + Constraint_Polytype_generalizes_from_Monotype sv (rigtys, monoty) info -> + Constraint_Polytype_generalizes_from_Monotype sv + ( sub `substitute` rigtys + , sub `substitute` monoty ) + info + Constraint_Polytype_instantiates_to_Monotype polyref monoty info -> + Constraint_Polytype_instantiates_to_Monotype + (sub `substitute` polyref) + (sub `substitute` monoty) + info + Constraint_Polytype_implicit_instantiates_to_Monotype (rigtys, t2) t1 info -> + Constraint_Polytype_implicit_instantiates_to_Monotype + ( sub `substitute` rigtys + , sub `substitute` t2 ) + (sub `substitute` t1) + info + Constraint_Polytype_generalized_by_Monotype (rigtys, polyref) monoty info -> + Constraint_Polytype_generalized_by_Monotype + ( sub `substitute` rigtys + , sub `substitute` polyref ) + (sub `substitute` monoty) + info +instance + ( info ~ Info m + , Show info + , Buildable info + , Solver_Constraint m + , Solver_Monotype m + , Solver_Polytype m + , Solver_Class m + ) => Solvable (Constraint_Polytype info) m where + constraint_solver con = + case con of + Constraint_Polytype_generalizes_from_Monotype polyvar (rigtys, monoty) _ -> do + -- NOTE: Here 'monotype_substitution' + -- can be in an inconsistent state, + -- however 'class_reduction' makes it consistent + -- (by calling: 'monotype_substitution_consistentify'), + -- it then applies it to the 'class_qualifiers' + -- (by calling: 'class_qualifiers_map' 'monotype_substitute'). + class_reduction + -- NOTE: Apply 'monotype_substitution' + -- to the 'Monotype's which must remain so, + -- and to the 'Monotype' before generalizing it. + polyty <- join $ class_polytype_forall + <$> monotype_substitute rigtys + <*> monotype_substitute monoty + -- NOTE: The 'Polyvar' given by the 'Constraint' + -- is then associated to the just computed 'Polytype', + -- within 'state_polytype_substitution'. + polytype_insert polyvar polyty + + Constraint_Polytype_instantiates_to_Monotype polyref monoty info -> do + polyty <- polytype_lookup polyref + -- NOTE: get a (known) 'Polytype' from the given 'Polytyref'. + Qualification + { qualifiers + , qualified=inst_monoty + } <- polytype_instantiate monoty polyty + -- NOTE: instantiate the 'Polytype' into a 'Monotype' + -- using the 'polytype_freshvar'. + let info' = info_insert (Info_Polytype_Instantiated polyty) info + forM_ qualifiers $ + -- NOTE: all instantiated 'qualifiers' have to be proven + class_qualifier_toprove $ + info_insert (Info_Monotype_Unification monoty inst_monoty) info' + constraint_push $ + constraint (monoty .==. inst_monoty $ info') + -- NOTE: add a 'Constraint_Monotype_Unification' + -- between the given 'Monotype' and the instantiated 'Polytype', + -- using the 'info' to store the original 'Polytype'. + + Constraint_Polytype_implicit_instantiates_to_Monotype (rigtys, t2) t1 info -> do + polyvar <- polytype_freshvar + constraint_push_many $ constraints $ Seq.fromList + [ Constraint_Polytype_generalizes_from_Monotype polyvar (rigtys, t2) info + , Constraint_Polytype_instantiates_to_Monotype (Polytyref_Var polyvar) t1 info + ] + + Constraint_Polytype_generalized_by_Monotype (rigtys, polyref) monoty info -> do + polyty <- polytype_lookup polyref + let info' = info_insert (Info_Polytype_Rigidified rigtys polyty) info + Qualification + { qualifiers + , qualified=rigid_polyty + } <- polytype_rigvarify info rigtys polyty + forM_ qualifiers $ + -- NOTE: all rigidified 'qualifiers' are assumed. + class_qualifier_assume $ + info_insert (Info_Monotype_Unification rigid_polyty monoty) info' + -- FIXME: Top has (monoty, monoty), but (rigid_polyty, monoty) + -- seems to be the correct thing to do. + constraint_push $ + constraint (monoty .==. rigid_polyty $ info') diff --git a/Language/LOL/Typing/Expr.hs b/Language/LOL/Typing/Expr.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Expr.hs @@ -0,0 +1,18 @@ +-- | All submodules, in a topological order. +-- +-- WARNING: this is a rough draft to experiment +-- with the generation of explicitely typed terms +-- from implicitely typed expressions; +-- see @Expr/Test.hs@. +module Language.LOL.Typing.Expr + ( module Language.LOL.Typing.Expr.Common + , module Language.LOL.Typing.Expr.Grammar + , module Language.LOL.Typing.Expr.Utils + -- , module Language.LOL.Typing.Expr.Write + ) where + +import Language.LOL.Typing.Expr.Calculus () +import Language.LOL.Typing.Expr.Common +import Language.LOL.Typing.Expr.Grammar +import Language.LOL.Typing.Expr.Utils +import Language.LOL.Typing.Expr.Write () diff --git a/Language/LOL/Typing/Expr/Calculus.ag b/Language/LOL/Typing/Expr/Calculus.ag new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Expr/Calculus.ag @@ -0,0 +1,156 @@ +-- vim: syntax=haskell +optpragmas { +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} +{-# OPTIONS_GHC -fno-warn-unused-matches #-} +} +module {Language.LOL.Typing.Expr.Calculus} {} { +import Data.Function (($)) +import Data.Eq (Eq(..)) +import Data.Maybe (Maybe(..), fromMaybe) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Prelude (Num(..), error) +import Data.Tuple (fst, snd) +import qualified Data.Foldable as Foldable + + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Expr.Common +import Language.LOL.Typing.Expr.Grammar +-- import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build +import qualified Language.LOL.Calculus as Calc +import Data.Monoid ((<>)) +import Text.Show (show) +-- import Debug.Trace +} + +include "./Grammar.ag" + +attr Expr Decl + -- | top-down + inh env :: {Calc.Env} + inh monoconsts :: Monoconsts + -- ^ The 'Monoconst's + -- bound at the current node. + inh monotys :: Substitution_Fixpoint + -- ^ The inferred 'Monotype's. + inh polytys :: Polysub + -- ^ The inferred 'Polytype's. + inh quantifiers :: {Map Monovar [Monotype]} + -- ^ The 'Monotype's (fully inferred) + -- which have been introduced when a 'Polytype' + -- has been instanciated to a 'Monovar', + -- and thus must be passed to the 'Expr_Var' derived from it. + inh renames :: {Map Name Name} + -- ^ Used to accumulate 'Name's + -- bound at the current node + -- but conflicting with 'monoconsts_Inh_Expr', + -- and thus requiring a rename + -- at their corresponding 'Expr_Var' nodes; + -- this rename is important because 'quantifiers_Inh_Expr' + -- may introduce 'Monoconst's of 'monoconsts_Inh_Expr'. + + -- | bottom-up + syn monovar :: Monovar + syn term :: {Calc.Term TeTy_Var} + + -- | both + chn freshvar :: Freshvar + +sem Expr + | Annot + | Var + lhs.monovar = @loc.monovar + loc.monovar = @lhs.freshvar + lhs.freshvar = @lhs.freshvar + 1 + loc.name = Map.findWithDefault @name @name @lhs.renames + lhs.term = {- + let ty = @lhs.monotys `substitute` Monotype_Var @loc.monovar in + let fv = subvars ty in + trace ("trace: Var m"<>show @loc.monovar<> + " name="<>show @loc.name<> + " : "<>Build.string ty<> + " ~> "<>show (Build.list <$> Map.lookup @loc.monovar @lhs.quantifiers)) $ + -} + Foldable.foldl + (\acc mty -> Calc.TeTy_App acc + (calc_type mty)) + (Calc.TeTy_Var (TeTy_Var_Name @loc.name)) + (Map.findWithDefault [] @loc.monovar @lhs.quantifiers) + {-case Map.lookup @loc.monovar @lhs.quantifiers of + Nothing -> Calc.TeTy_Var (TeTy_Var_Name @name) + Just quants -> + Foldable.foldl + (\acc quant -> Calc.TeTy_App acc + (calc_type $ @lhs.monotys `substitute` Monotype_Var quant)) + (Calc.TeTy_Var (TeTy_Var_Name @name)) + quants-} + | Abst + lhs.monovar = @loc.monovar + loc.monovar = @lhs.freshvar + loc.arg_monovar = @lhs.freshvar + 1 + body.freshvar = @lhs.freshvar + 2 + loc.consts_name = const_freshify @lhs.monoconsts @name + body.monoconsts = fst @loc.consts_name + body.renames = if @name == snd @loc.consts_name + then @lhs.renames + else Map.insert @name (snd @loc.consts_name) @lhs.renames + loc.term = Calc.Term_Abst (Calc.Suggest $ snd @loc.consts_name) + (calc_type $ @lhs.monotys `substitute` + Monotype_Var @loc.arg_monovar) $ -- TODO: cache calc_type + (\v -> case v of + TeTy_Var_Name n | n == snd @loc.consts_name -> Just (Calc.Suggest n) + _ -> Nothing) `Calc.abstract` @body.term + | App + lhs.monovar = @loc.monovar + loc.monovar = @lhs.freshvar + abst.freshvar = @lhs.freshvar + 1 + lhs.term = Calc.TeTy_App @abst.term @arg.term + | Let + lhs.monovar = @loc.monovar + loc.monovar = @lhs.freshvar + loc.decl_polyvar = @lhs.freshvar + 1 + decl.freshvar = @lhs.freshvar + 2 + loc.consts_name = const_freshify @lhs.monoconsts @name + body.renames = if @name == snd @loc.consts_name + then @lhs.renames + else Map.insert @name (snd @loc.consts_name) @lhs.renames + loc.decl_polyty = fromMaybe (error $ "Oops, Polytype missing " <> show @loc.decl_polyvar <> " in " <> show @lhs.polytys) $ + Map.lookup @loc.decl_polyvar @lhs.polytys + loc.decl_quants = quantifiers_freshify @lhs.monoconsts + (quantifier_hintnames @loc.decl_polyty) + (quantifiers @loc.decl_polyty) + decl.monoconsts = fst @loc.decl_quants + body.monoconsts = fst @loc.consts_name + lhs.term = Calc.TeTy_App + (Calc.Term_Abst + (Calc.Suggest $ snd @loc.consts_name) + (Foldable.foldr + (\(quant, qname) ty -> + let nam = Calc.Suggest qname in + Calc.Type_Abst nam + (Calc.Type_Sort Calc.sort_star_mono) + ((\v -> case v of + TeTy_Var_Monovar m | m == quant -> Just nam + _ -> Nothing) `Calc.abstract` ty)) + (calc_type (quantified @loc.decl_polyty)) + (snd @loc.decl_quants)) + ((\v -> case v of + TeTy_Var_Name n | n == snd @loc.consts_name -> Just (Calc.Suggest n) + _ -> Nothing) `Calc.abstract` @body.term)) + (Foldable.foldr + (\(quant, qname) te -> + let nam = Calc.Suggest qname in + Calc.Term_Abst nam + (Calc.Type_Sort Calc.sort_star_mono) + ((\v -> case v of + TeTy_Var_Monovar m | m == quant -> Just nam + _ -> Nothing) `Calc.abstract` te)) + @decl.term + (snd @loc.decl_quants)) +sem Decl + | Let + -- loc.monovar = @lhs.freshvar + -- loc.decl_polyvar = @lhs.freshvar + 1 + decl.freshvar = @lhs.freshvar + 1 diff --git a/Language/LOL/Typing/Expr/Common.hs b/Language/LOL/Typing/Expr/Common.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Expr/Common.hs @@ -0,0 +1,124 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} +module Language.LOL.Typing.Expr.Common where + +import qualified Data.Foldable as Foldable +import Data.Eq (Eq(..)) +import Data.Text (Text) +import qualified Data.Text as Text +import Data.Function (const) +import Data.Functor ((<$>)) +import Data.Maybe (Maybe(..)) +import Data.Text.Buildable (Buildable(..)) + +import qualified Language.LOL.Calculus as Calc +import Language.LOL.Typing.Type +import Text.Show + +type Name = Text + +data TeTy_Var + = TeTy_Var_Name Calc.Var_Name + | TeTy_Var_Monovar Monovar + deriving (Eq, Show) +instance Buildable TeTy_Var where + build x = + case x of + TeTy_Var_Name n -> build n + TeTy_Var_Monovar v -> build (Monotype_Var v) + +class Calc_Type a where + calc_type :: a -> Calc.Type TeTy_Var +instance Calc_Type Monotype where + calc_type ty = + case app_spine_left ty of + Monotype_Var v `App_Spine` [] -> Calc.TeTy_Var (TeTy_Var_Monovar v) + Monotype_Const c `App_Spine` [] -> Calc.TeTy_Var (TeTy_Var_Name c) + Monotype_Const "->" `App_Spine` [t1, t2] -> + Calc.Type_Abst (Calc.Suggest "") + (calc_type t1) + (const Nothing `Calc.abstract` calc_type t2) + t `App_Spine` tys -> + Calc.term_apps + (calc_type t) + (calc_type <$> tys) +calc_of_polytype + :: Monoconsts + -> Polytype + -> (Monoconsts, Calc.Type TeTy_Var) +calc_of_polytype consts_used Quantification + { quantifiers + , quantifier_hintnames + , quantified } = + Foldable.foldr + (\(quant, qname) ty -> + let nam = Calc.Suggest qname in + Calc.Type_Abst nam + (Calc.Type_Sort Calc.sort_star_mono) + ((\x -> case x of + TeTy_Var_Monovar v | v == quant-> Just nam + _ -> Nothing) `Calc.abstract` ty) + ) (calc_type quantified) <$> + quantifiers_freshify consts_used quantifier_hintnames quantifiers +calc_abst_term_of_polytype + :: Monoconsts + -> Polytype + -> Calc.Term TeTy_Var + -> (Monoconsts, Calc.Type TeTy_Var) +calc_abst_term_of_polytype consts_used Quantification + { quantifiers + , quantifier_hintnames } term = + Foldable.foldr + (\(quant, qname) ty -> + let nam = Calc.Suggest qname in + Calc.Term_Abst nam + (Calc.Type_Sort Calc.sort_star_mono) + ((\x -> case x of + TeTy_Var_Monovar v | v == quant -> Just nam + _ -> Nothing) `Calc.abstract` ty) + ) term <$> + quantifiers_freshify consts_used quantifier_hintnames quantifiers +{- +instance (Show a, Substitutable a, Buildable (Quantification_Build_Options, a), Calc_Type a) + => Calc_Type ([Monoconst], Forall a) where + calc_type (consts_used, f@Quantification + { quantifiers + , quantifier_hintnames + , quantified }) = + let (_consts_used, quants) = quantifiers_freshify consts_used quantifier_hintnames quantifiers in + let qty = calc_type quantified in + Foldable.foldr + (\(quant, qname) ty -> + Calc.Type_Abst (Calc.Suggest qname) + (Calc.Type_Sort Calc.sort_star_mono) + ((\x -> + case x of + TeTy_Var_Name _ -> Nothing + TeTy_Var_Monovar v -> + if v == quant + then Just (Calc.Suggest qname) + else Nothing) `Calc.abstract` ty) + ) qty $ + trace ("quants: " <> Build.string (Build.list $ (\(x, y) -> Build.tuple [build x, build y]) <$> quants)) + trace ("forall: " <> Build.string (def::Quantification_Build_Options,f)) + trace ("forall: " <> show f) + trace ("quantified: " <> show quantified) + quants +-} +instance (Calc_Type a) => Calc_Type (Qualification [Class_Qualifier] a) where + calc_type Qualification + { qualifiers + , qualified } = + Foldable.foldr + (\(Class_Qualifier qname qty) ty -> + Calc.Term_Abst (Calc.Suggest qname) + (calc_type qty) + ((\x -> case x of + TeTy_Var_Name n | Text.toLower n == qname -> Just (Calc.Suggest qname) + _ -> Nothing) `Calc.abstract` ty) + ) (calc_type qualified) qualifiers + diff --git a/Language/LOL/Typing/Expr/Grammar.ag b/Language/LOL/Typing/Expr/Grammar.ag new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Expr/Grammar.ag @@ -0,0 +1,43 @@ +-- vim: syntax=haskell +optpragmas { +{-# LANGUAGE OverloadedStrings #-} +} +module {Language.LOL.Typing.Expr.Grammar} {} { +import Data.Maybe (Maybe(..)) +import Text.Show (Show) + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Expr.Common +} + +data Expr + | Var + name :: Name + | Abst -- ^ Monomorphic bind + sig :: {Maybe Monotype} + name :: Name + body :: Expr + | App + abst :: Expr + arg :: Expr + | Annot + body :: Expr + sig :: Polytype + | Let -- ^ Polymorphic bind + sig :: {Maybe Polytype} + name :: Name + decl :: Expr + body :: Expr + | Where + sig :: {Maybe Polytype} + name :: Name + decl :: Expr + body :: Expr +deriving Expr : Show + +data Decl + | Let + sig :: {Maybe Monotype} + name :: Name + decl :: Expr +deriving Decl : Show diff --git a/Language/LOL/Typing/Expr/Test.hs b/Language/LOL/Typing/Expr/Test.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Expr/Test.hs @@ -0,0 +1,195 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +module Expr.Test where + +import Control.Monad (Monad(..), when) +import Data.Bool +import Data.Functor.Identity (Identity(..)) +import Data.Either (Either(..)) +import Data.Function (($), (.)) +import Data.Functor ((<$>)) +import Data.Traversable (Traversable(..)) +import Data.Maybe (Maybe(..)) +import Data.Eq (Eq(..)) +-- import Data.Tuple (fst, snd) +import qualified Data.Foldable as Foldable +import qualified Data.List as List +-- import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Monoid (Monoid(..), (<>)) +import Test.Tasty +import Test.Tasty.HUnit +-- import Test.HUnit hiding (test) +import System.IO (IO) +-- import Data.Sequence (Seq) +import Data.Text (Text) +-- import Control.Monad.Trans.Class (lift) +-- import qualified Data.Text as Text +import qualified Data.Text.IO as Text +import Text.Show (Show(..)) +import Prelude (error) +-- import Debug.Trace + +import qualified Language.LOL.Calculus as Calc +import qualified Language.LOL.Calculus.Read as Calc +import Language.LOL.Typing +-- import qualified Language.LOL.Typing.Collect.Grammar as Collect +import Language.LOL.Typing.Expr.Calculus +import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build +import Solver.Test (polytys_env, infer) +-- import Solver.Test (write_log, Collect_Constraints(..), Infer_Polytype(..)) + +tests :: TestTree +tests = testGroup "Expr" + [ tests_Calculus + ] + +type Test_Solver + = Solver_Greedy_Finite Collect_Infos IO + +class Calcify a where + calcify + :: Bool -> a + -> IO (Either (Collect_Error (Info Test_Solver) + (Error Test_Solver)) + (Calc.Term TeTy_Var)) +instance Calcify Expr where + calcify logging expr = do + ty <- infer logging expr + case ty of + Left err -> return $ Left err + Right Solver_Result + { solver_result_monotypes = monosub + , solver_result_polytypes = polysub + , solver_result_quantifiers = quants + } -> do + let monoty = monosub `substitute` Monotype_Var 0 + let foralls = subvars monoty + let consts = Map.unions + ( (Map.fromList $ (, ()) <$> List.take (List.length foralls) const_pool) + : ((\(name, polyty) -> Map.insert name () $ monoconsts polyty) <$> polytys_env) ) + let Syn_Expr + { term_Syn_Expr = term + } = wrap_Expr (sem_Expr expr) Inh_Expr + { env_Inh_Expr = mempty + , freshvar_Inh_Expr = 0 + , monoconsts_Inh_Expr = consts + , monotys_Inh_Expr = monosub + , polytys_Inh_Expr = (monosub `substitute`) <$> polysub + , quantifiers_Inh_Expr = (monosub `substitute`) . (Monotype_Var <$>) <$> quants + , renames_Inh_Expr = mempty + } + return $ Right $ + Foldable.foldr + (\(quant, const) -> + Calc.Term_Abst (Calc.Suggest const) + (Calc.Type_Sort Calc.sort_star_mono) . + ((\v -> case v of + TeTy_Var_Monovar m | m == quant -> Just (Calc.Suggest const) + _ -> Nothing) `Calc.abstract`)) + term + (List.zip foralls const_pool) +instance Calcify Decl where + calcify logging decl = do + ty <- infer logging decl + case ty of + Left err -> return $ Left err + Right Solver_Result + { solver_result_monotypes = monosub + , solver_result_polytypes = polysub + , solver_result_quantifiers = quants + } -> do + let monoty = monosub `substitute` Monotype_Var 1 -- NOTE: decl.freshvar + let foralls = subvars monoty + let consts = Map.unions + ( (Map.fromList $ (, ()) <$> List.take (List.length foralls) const_pool) + : ((\(name, polyty) -> Map.insert name () $ monoconsts polyty) <$> polytys_env) ) + let Syn_Decl + { term_Syn_Decl = term + } = wrap_Decl (sem_Decl decl) Inh_Decl + { env_Inh_Decl = mempty + , freshvar_Inh_Decl = 0 + , monoconsts_Inh_Decl = consts + , monotys_Inh_Decl = monosub + , polytys_Inh_Decl = (monosub `substitute`) <$> polysub + , quantifiers_Inh_Decl = (monosub `substitute`) . (Monotype_Var <$>) <$> quants + , renames_Inh_Decl = mempty + } + return $ Right $ + Foldable.foldr + (\(quant, const) -> + Calc.Term_Abst (Calc.Suggest const) + (Calc.Type_Sort Calc.sort_star_mono) . + ((\v -> case v of + TeTy_Var_Monovar m | m == quant -> Just (Calc.Suggest const) + _ -> Nothing) `Calc.abstract`)) + term + (List.zip foralls const_pool) + +calc_monovar_close :: Calc.Term TeTy_Var -> Either Monovar (Calc.Term Calc.Var_Name) +calc_monovar_close te = + traverse go te + where + go (TeTy_Var_Monovar v) = Left v + go (TeTy_Var_Name n) = Right n + +tests_Calculus :: TestTree +tests_Calculus = testGroup "Calculus" $ + let test logging input (expected::Text) = do + when logging $ + Text.putStrLn ("expr: " <> Build.text input) + let expect_term = + case runIdentity $ Calc.read Calc.parse_term expected of + Left err -> error $ show err + Right x -> x + got_either_term <- calcify logging input + case got_either_term of + got@(Left _) -> got @?= Right (TeTy_Var_Name <$> expect_term) + Right got_term -> + case calc_monovar_close got_term of + Left m -> Left ("Monovar remains in term: " <> show m) @?= Right expect_term + got -> do + when logging $ do + Text.putStrLn ("exp: " <> Build.text expect_term) + case got of + Right ex -> Text.putStrLn ("got: " <> Build.text ex) + _ -> return () + got @?= Right expect_term in + let (==>) = test False in + -- let (==>>) = test True in + [ testGroup "Expr" $ + [ testCase "id" $ ("x".-> "x") + ==> "λ(a:*) (x:a) -> x" + , testCase "id_Int" $ (("x","Int")..-> "x") + ==> "λ(x:Int) -> x" + , testCase "id_Int" $ ("x".-> ("x".:("Int"::Monotype))) + ==> "λ(x:Int) -> x" + , testCase "twice" $ ("f".-> "x".-> "f"!("f"!"x")) + ==> "λ(a:*) (f:a -> a) (x:a) -> f (f x)" + , testCase "const" $ ("x".-> "y".-> "x") + ==> "λ(a:*) (b:*) (x:a) (y:b) -> x" + , testCase "compose" $ ("f".-> "g".-> "x".-> "f"!("g"!"x")) + ==> "λ(a:*) (b:*) (c:*) (f:a -> b) (g:c -> a) (x:c) -> f (g x)" + , testCase "equal" $ ("x".-> "f".= "x" $ "f") + ==> "λ(a:*) (x:a) -> (λ(f:a) -> f) x" + , testCase "equal" $ ("x".-> "f".= ("y".->"x") $ "pair"!("f"!"True")!("f"!"one") ) + ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> pair a a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)" + {- + , testCase "equal" $ ("x".-> "f".= ("y".->"x") $ "equal"!("f"!"True")!("f"!"one") ) + ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> equal a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)" + -} + ] + , testGroup "Decl" $ + [ testCase "equal" $ Decl_Let Nothing "test" + ("x".-> "f".= ("y".-> "x") $ "equal"!("f"!"True")!("f"!"one") ) + ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> equal a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)" + -- , testCase "Abst rename" $ Decl_Let Nothing "test" ("Bool".-> "f".= ("y".-> "Bool") $ "equal"!("f"!"True")!("f"!"one") ) + -- ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> equal a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)" + -- , testCase "Let rename" $ Decl_Let Nothing "test" ("x".-> "Int".= ("y".-> "x") $ "equal"!("Int"!"True")!("Int"!"one") ) + -- ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> equal a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)" + -- , testCase "equal" $ Decl_Let Nothing "test" ("x".-> "f".= ("y".-> "g".= ("z".->"y") $ "g"!"x") $ "equal"!("f"!"True")!("f"!"True") ) + -- ==>> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> b) -> equal Bool (f Bool True) (f Bool True)) (λ(b:*) (y:b) -> (λ(g:∀(c:*) -> c -> b) -> g a x) (λ(c:*) (z:c) -> y))" + ] + ] diff --git a/Language/LOL/Typing/Expr/Utils.hs b/Language/LOL/Typing/Expr/Utils.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Expr/Utils.hs @@ -0,0 +1,43 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Language.LOL.Typing.Expr.Utils where + +import Data.Function (($), (.)) +import Data.Maybe (Maybe(..)) +import Data.String (IsString(..)) + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Expr.Common +import Language.LOL.Typing.Expr.Grammar + +-- Convenient instances + +instance IsString Expr where + fromString = Expr_Var . fromString + +-- * Convenient 'Expr' constructors + +(.->) :: Name -> Expr -> Expr +(.->) = Expr_Abst Nothing +infixr 0 .-> +(..->) :: (Name, Monotype) -> Expr -> Expr +(..->) (name, sig) = Expr_Abst (Just sig) name +infixr 0 ..-> + +(.:) :: Polytypeable sig => Expr -> sig -> Expr +(.:) e = Expr_Annot e . polytype +infixr 0 .: + +(.=) :: Name -> Expr -> Expr -> Expr +(.=) = Expr_Let Nothing +infixr 2 .= +(..=) :: Polytypeable sig => (Name, sig) -> Expr -> Expr -> Expr +(..=) (name, sig) = Expr_Let (Just $ polytype sig) name +infixr 2 ..= + +(!) :: Expr -> Expr -> Expr +(!) = Expr_App +infixl 5 ! + +(.$) :: Expr -> Expr -> Expr +(.$) = Expr_App +infixr 3 .$ diff --git a/Language/LOL/Typing/Expr/Write.hs b/Language/LOL/Typing/Expr/Write.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Expr/Write.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Language.LOL.Typing.Expr.Write where + +import Data.Maybe (Maybe(..)) +import Data.Monoid ((<>)) +import Data.Text.Buildable (Buildable(..)) + +import Language.LOL.Typing.Expr.Grammar + +instance Buildable Expr where + build expr = + case expr of + Expr_Var nam -> build nam + Expr_App f x -> + "(" <> build f <> " " <> build x <> ")" + Expr_Annot e sig -> + "(" <> build e <> " : " <> build sig <> ")" + Expr_Let sig nam decl e -> + "let " <> n <> " = " <> build decl <> " in " <> build e + where n = + case sig of + Just s -> "("<>build nam<>":"<>build s<>")" + Nothing -> build nam + Expr_Where sig nam decl e -> + build e <> " where " <> n <> " = " <> build decl + where n = + case sig of + Just s -> "("<>build nam<>":"<>build s<>")" + Nothing -> build nam + Expr_Abst sig nam e -> + "(" <> "\\" <> n <> " -> " <> build e <> ")" + where n = + case sig of + Just s -> "("<>build nam<>":"<>build s<>")" + Nothing -> build nam +instance Buildable Decl where + build decl = + case decl of + Decl_Let sig nam expr -> + n <> " = " <> build expr + where n = + case sig of + Just s -> "("<>build nam<>":"<>build s<>")" + Nothing -> build nam diff --git a/Language/LOL/Typing/Lib/Control/Monad/Classes/EffectsFix.hs b/Language/LOL/Typing/Lib/Control/Monad/Classes/EffectsFix.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Lib/Control/Monad/Classes/EffectsFix.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE KindSignatures #-} +module Language.LOL.Typing.Lib.Control.Monad.Classes.EffectsFix where +-- | Effects whose state is parameterized by the 'Monad' stack. + +-- * Types of effects + +-- | Writer effect +data EffWriterFix (w :: {-m-}(* -> *) -> *) + +-- | Reader effect +data EffReaderFix (e :: {-m-}(* -> *) -> *) + +-- | Local state change effect +data EffLocalFix (e :: {-m-}(* -> *) -> *) + +-- | State effect +data EffStateFix (s :: {-m-}(* -> *) -> *) diff --git a/Language/LOL/Typing/Lib/Control/Monad/Classes/Instance.hs b/Language/LOL/Typing/Lib/Control/Monad/Classes/Instance.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Lib/Control/Monad/Classes/Instance.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE TypeFamilies #-} +module Language.LOL.Typing.Lib.Control.Monad.Classes.Instance where +import Data.Bool (Bool(..)) +import GHC.Prim (Constraint) + +-- | A data type to existentially wrap a value of type @ty@, +-- when it is an instance of the type class @cl@. +data Instance (cl:: * -> Constraint) + = forall ty. cl ty => Instance ty + +-- | An open type family to know (at the type level) whether a type @ty@ +-- has an instance of the type class @cl@. +-- +-- NOTE: currently, users have to manually define type family instances of 'Class' +-- to indicate to the compiler which type support which type class. +-- It is definitively redundant to have to define +-- both a type class instance and a type family instance, +-- but I cannot find a way to automatically synchronize +-- the compiler's knowledge between these two levels. +type family Class (cl:: * -> Constraint) (ty:: *) :: Bool diff --git a/Language/LOL/Typing/Lib/Control/Monad/Classes/StateFix.hs b/Language/LOL/Typing/Lib/Control/Monad/Classes/StateFix.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Lib/Control/Monad/Classes/StateFix.hs @@ -0,0 +1,134 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} + +-- | 'MonadState' whose state is parameterized by the 'Monad' stack. +module Language.LOL.Typing.Lib.Control.Monad.Classes.StateFix where + +import Control.Applicative (Applicative(..)) +import Control.Monad +import Control.Monad.Classes +import Control.Monad.Trans.Class +import qualified Control.Monad.Trans.State.Lazy as SL +-- import qualified Control.Monad.Trans.State.Strict as SS -- TODO: when needed :) +import Data.Bool (Bool(..)) +import Data.Function ((.), const) +import Data.Functor.Identity (Identity) +import GHC.Prim (Proxy#, proxy#) +import Prelude (seq) + +import Language.LOL.Typing.Lib.Control.Monad.Classes.EffectsFix + +-- * Type 'StateLazyFixT' + +data StateLazyFixT + (st::{-StateLazyFixT st m-}(* -> *) -> *) + (m::{-a-}* -> *) + (a:: *) + = StateLazyFixT + { unStateLazyFixT :: SL.StateT (st (StateLazyFixT st m)) m a } + deriving (Functor) +instance Monad m => Applicative (StateLazyFixT st m) where + pure = return + (<*>) = ap +instance Monad m => Monad (StateLazyFixT st m) where + return = StateLazyFixT . return + m >>= f = StateLazyFixT (unStateLazyFixT m >>= unStateLazyFixT . f) +instance MonadTrans (StateLazyFixT st) where + lift = StateLazyFixT . lift + +-- ** Type 'StateLazyFix' +type StateLazyFix st + = StateLazyFixT st Identity + +-- * Type family 'StateFixCanDo' + +type instance CanDo (StateLazyFixT s m) eff + = StateFixCanDo s eff + +type family StateFixCanDo s eff where + StateFixCanDo s (EffStateFix s) = 'True + StateFixCanDo s (EffReaderFix s) = 'True + StateFixCanDo s (EffLocalFix s) = 'True + StateFixCanDo s (EffWriterFix s) = 'True + StateFixCanDo s eff = 'False + +-- * Class 'MonadStateFixN' + +class Monad m => MonadStateFixN (n :: Peano) s m where + stateFixN :: Proxy# n -> (s m -> (a, s m)) -> m a + +-- | Warning: only work when 'StateLazyFixT' +-- is the outermost 'Monad' (i.e. when @n@ @~@ 'Zero'), +-- because the state is paramaterized by this 'Monad'. +instance Monad m => MonadStateFixN 'Zero s (StateLazyFixT s m) where + stateFixN _ = StateLazyFixT . SL.state + +-- ** Type 'MonadStateFixN' + +-- | The @'MonadStateFix' s m@ constraint asserts that @m@ is a 'Monad' stack +-- that supports state operations on type @s@ +type MonadStateFix (s::(* -> *) -> *) m + = MonadStateFixN (Find (EffStateFix s) m) s m + +-- | Construct a state 'Monad' computation from a function +stateFix + :: forall s m a. (MonadStateFix s m) + => (s m -> (a, s m)) -> m a +stateFix = stateFixN (proxy# :: Proxy# (Find (EffStateFix s) m)) + +-- | @'put' s@ sets the state within the 'Monad' to @s@ +putFix :: MonadStateFix s m => s m -> m () +putFix s = stateFix (const ((), s)) + +-- | Fetch the current value of the state within the 'Monad' +getFix :: MonadStateFix s m => m (s m) +getFix = stateFix (\s -> (s, s)) + +-- | Gets specific component of the state, +-- using a projection function supplied. +getsFix :: MonadStateFix s m => (s m -> a) -> m a +getsFix f = do + s <- getFix + return (f s) + +-- | Maps an old state to a new state inside a state 'Monad' layer +modifyFix :: MonadStateFix s m => (s m -> s m) -> m () +modifyFix f = stateFix (\s -> ((), f s)) + +-- | A variant of 'modify' in which the computation +-- is strict in the new state. +modifyFix' :: MonadStateFix s m => (s m -> s m) -> m () +modifyFix' f = stateFix (\s -> let s' = f s in s' `seq` ((), s')) + +-- Return the 'Monad' parameter and the state. +runStateLazyFix + :: st (StateLazyFixT st m) + -> StateLazyFixT st m a + -> m (a, st (StateLazyFixT st m)) +runStateLazyFix s m = SL.runStateT (unStateLazyFixT m) s + +-- Return the 'Monad' parameter. +evalStateLazyFix + :: Monad m + => st (StateLazyFixT st m) + -> StateLazyFixT st m a + -> m a +evalStateLazyFix s m = SL.evalStateT (unStateLazyFixT m) s + +-- Return the state. +execStateLazyFix + :: Monad m + => st (StateLazyFixT st m) + -> StateLazyFixT st m a + -> m (st (StateLazyFixT st m)) +execStateLazyFix s m = SL.execStateT (unStateLazyFixT m) s diff --git a/Language/LOL/Typing/Lib/Control/Monad/Classes/StateInstance.hs b/Language/LOL/Typing/Lib/Control/Monad/Classes/StateInstance.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Lib/Control/Monad/Classes/StateInstance.hs @@ -0,0 +1,109 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} -- NOTE: for CansMonadStateInstance +{-# OPTIONS_GHC -fno-warn-tabs #-} + +-- | Collect in a 'Monad' stack, the states of 'MC.MonadState' 'Monad' +-- which are instances of a given type class. +module Language.LOL.Typing.Lib.Control.Monad.Classes.StateInstance where + +import Control.Monad +import qualified Control.Monad.Classes as MC +import Control.Monad.Trans.Class +import qualified Control.Monad.Trans.State.Lazy as SL +import qualified Control.Monad.Trans.State.Strict as SS +import Data.Bool (Bool(..)) +import GHC.Prim (Proxy#, proxy#, Constraint) + +import Language.LOL.Typing.Lib.Control.Monad.Classes.Instance +import Language.LOL.Typing.Lib.Control.Monad.Classes.StateFix + +-- * Class 'MonadStateInstance' + +-- ** Type family 'CanMonadStateInstance' + +-- | A close type family to know whether a 'Monad' @m@ +-- support an effect 'eff' whose state is an instance of the type class @cl@. +-- +-- NOTE: the closeness enables to define 'Class' instances +-- only for the states of the 'Monad's in a 'Monad' stack +-- which support the effects 'MC.EffState'. +type family CanMonadStateInstance (cl:: * -> Constraint) (m:: * -> *) (eff:: k) :: Bool where + CanMonadStateInstance cl (SL.StateT s m) (MC.EffState _s) = Class cl s + CanMonadStateInstance cl (SS.StateT s m) (MC.EffState _s) = Class cl s + -- CanMonadStateInstance cl (SL.StateT s m) (MC.EffReader _s) = Class cl s + -- CanMonadStateInstance cl (SS.StateT s m) (MC.EffReader _s) = Class cl s + CanMonadStateInstance cl (StateLazyFixT s m) (MC.EffState _s) = Class cl (s m) + CanMonadStateInstance cl s eff = 'False + +-- ** Type family 'CansMonadStateInstance' + +-- | A close type family to know which 'Monad's in a 'Monad' stack @stack@ +-- support an effect 'eff' whose state is an instance of the type class @cl@. +type family CansMonadStateInstance (cl:: * -> Constraint) (eff :: k) (stack :: * -> *) :: [Bool] where + CansMonadStateInstance cl eff (t m) = CanMonadStateInstance cl (t m) eff ': CansMonadStateInstance cl eff m + CansMonadStateInstance cl eff m = CanMonadStateInstance cl m eff ': '[] + +-- | A type synonym to constrain a 'Monad' @m@ +-- to support an 'MC.EffState' whose state is an instance of the type class @cl@. +type MonadStateInstance cl m + = MonadStateInstanceN cl (CansMonadStateInstance cl (MC.EffState ()) m) m + +getInstance :: forall cl m. MonadStateInstance cl m => m [Instance cl] +getInstance = getInstanceN (proxy# :: Proxy# (CansMonadStateInstance cl (MC.EffState ()) m)) + +-- ** Class 'MonadStateInstanceN' + +-- | A type class to recurse over the 'Monad' stack +-- to collect the states which are instance of the type class @cl@. +class Monad m => MonadStateInstanceN cl (cans::[Bool]) m where + getInstanceN :: Proxy# cans -> m [Instance cl] + +-- | Collect the lazy 'SL.StateT', and recurse. +instance (cl s, Monad m, MonadStateInstanceN cl cans m) + => MonadStateInstanceN cl ('True ': cans) (SL.StateT s m) where + getInstanceN _ = do + s <- SL.get + ss <- lift (getInstanceN (proxy# :: Proxy# cans)) + return (Instance s : ss) + +-- | Collect the strict 'SS.StateT', and recurse. +instance (cl s, Monad m, MonadStateInstanceN cl cans m) + => MonadStateInstanceN cl ('True ': cans) (SS.StateT s m) where + getInstanceN _ = do + s <- SS.get + ss <- lift (getInstanceN (proxy# :: Proxy# cans)) + return (Instance s : ss) + +-- | Collect the 'StateLazyFixT', and recurse. +instance (cl (s (StateLazyFixT s m)), Monad m, MonadStateInstanceN cl cans m) + => MonadStateInstanceN cl ('True ': cans) (StateLazyFixT s m) where + getInstanceN _ = do + s <- StateLazyFixT SL.get + ss <- lift (getInstanceN (proxy# :: Proxy# cans)) + return (Instance s : ss) + +-- | Recurse the 'Monad' stack, passing over 'Monad' @t m@ +-- such that 'CanMonadStateInstance' @cl@ @t m@ @MC.EffState ()@ @~@ 'False'. +instance + ( Monad m + , Monad (t m) + , MonadTrans t + , MonadStateInstanceN cl (can ': cans) m + ) => MonadStateInstanceN cl ('False ': (can ': cans)) (t m) where + getInstanceN _ = lift (getInstanceN (proxy# :: Proxy# (can ': cans))) + +-- | Terminating instance, when the deepest 'Monad' on the stack +-- is such that 'CanMonadStateInstance' @cl@ @t m@ @MC.EffState ()@ @~@ 'False': +-- then there is no need to recurse, +-- and thus no 'MonadStateInstanceN' @cl@ @[]@ @m@ constraint to impose. +instance Monad m => MonadStateInstanceN cl ('False ': '[]) m where + getInstanceN _ = return [] diff --git a/Language/LOL/Typing/Lib/Data/Default.hs b/Language/LOL/Typing/Lib/Data/Default.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Lib/Data/Default.hs @@ -0,0 +1,6 @@ +module Language.LOL.Typing.Lib.Data.Default where + +-- * Class 'Default' + +class Default a where + def :: a diff --git a/Language/LOL/Typing/Lib/Data/Empty.hs b/Language/LOL/Typing/Lib/Data/Empty.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Lib/Data/Empty.hs @@ -0,0 +1,17 @@ +module Language.LOL.Typing.Lib.Data.Empty where + +import Data.Maybe (Maybe(..)) + +-- * Class 'Empty' + +class Empty a where + empty :: a + +instance Empty () where + empty = () +instance (Empty a, Empty b) => Empty (a, b) where + empty = (empty, empty) +instance Empty [a] where + empty = [] +instance Empty (Maybe a) where + empty = Nothing diff --git a/Language/LOL/Typing/Lib/Data/Text/Buildable.hs b/Language/LOL/Typing/Lib/Data/Text/Buildable.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Lib/Data/Text/Buildable.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Language.LOL.Typing.Lib.Data.Text.Buildable where + +import Data.Function (($), (.)) +import Data.Functor ((<$>)) +import Data.Foldable (Foldable(..)) +import Data.Monoid (Monoid(..), (<>)) +import qualified Data.List as List +import Data.String (String) +import Data.Text (Text) +import Data.Text.Buildable (Buildable(..)) +import qualified Data.Text.Lazy as TL +import qualified Data.Text.Lazy.Builder as Build +import Data.Text.Lazy.Builder (Builder) + +string :: Buildable a => a -> String +string = TL.unpack . Build.toLazyText . build + +text :: Buildable a => a -> Text +text = TL.toStrict . Build.toLazyText . build + +tuple :: (Foldable f, Buildable a) => f a -> Builder +tuple f = "(" <> mconcat (List.intersperse ", " $ foldr ((:). build) [] f) <> ")" + +list :: (Foldable f, Buildable a) => f a -> Builder +list f = "[" <> mconcat (List.intersperse ", " $ foldr ((:). build) [] f) <> "]" + +unlines :: (Foldable f, Buildable a) => f a -> Builder +unlines = mconcat . List.intersperse "\n" . foldr ((:). build) [] + +indent :: Buildable a => Builder -> a -> Builder +indent prefix = + mconcat . List.intersperse "\n" . + ((prefix <>) . build <$>) . TL.lines . + Build.toLazyText . build + +parens :: Buildable a => a -> Builder +parens a = "(" <> build a <> ")" + +{- +instance Buildable a => Buildable [a] where + build = list +-} diff --git a/Language/LOL/Typing/Solver.hs b/Language/LOL/Typing/Solver.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Solver.hs @@ -0,0 +1,18 @@ +-- | All submodules, in a topological order. +module Language.LOL.Typing.Solver + ( module Language.LOL.Typing.Solver.Common + , module Language.LOL.Typing.Solver.Constraint + , module Language.LOL.Typing.Solver.Monotype + , module Language.LOL.Typing.Solver.Polytype + , module Language.LOL.Typing.Solver.Class + , module Language.LOL.Typing.Solver.Monad + , module Language.LOL.Typing.Solver.Greedy + ) where + +import Language.LOL.Typing.Solver.Common +import Language.LOL.Typing.Solver.Constraint +import Language.LOL.Typing.Solver.Monotype +import Language.LOL.Typing.Solver.Polytype +import Language.LOL.Typing.Solver.Class +import Language.LOL.Typing.Solver.Monad +import Language.LOL.Typing.Solver.Greedy diff --git a/Language/LOL/Typing/Solver/Class.hs b/Language/LOL/Typing/Solver/Class.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Solver/Class.hs @@ -0,0 +1,478 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +-- | Type inference for /type class polymorphism/ +-- (aka. /parametric overloading/). +module Language.LOL.Typing.Solver.Class where + +import Control.Monad (Monad(..), forM, forM_, mapM) +import qualified Control.Monad.Classes as MC +import Data.Bool +import Data.Eq (Eq(..)) +import qualified Data.Foldable as Foldable +import Data.Function (($), (.)) +import Data.Functor ((<$>)) +import qualified Data.List as List +import qualified Data.Map.Strict as Map +import Data.Maybe (Maybe(..), isJust) +import Data.Monoid (Monoid(..), (<>)) +import Data.Text (Text) +import Data.Text.Buildable (Buildable(..)) +import Data.Tuple (fst) +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Solver.Common +import Language.LOL.Typing.Solver.Constraint +import Language.LOL.Typing.Solver.Monotype +import Language.LOL.Typing.Solver.Polytype +import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.Instance as MC +import Language.LOL.Typing.Lib.Data.Empty (Empty(..)) +import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build + +-- * Type 'State_Class' + +data State_Class info + = State_Class + { state_class_directives :: [Class_Directive info] + -- ^ 'Class_Directive's for 'state_class_qualifiers'. + , state_class_env :: Class_Env + -- ^ Known 'Class'es and 'Class_Instance's. + , state_class_qualifiers :: State_Class_Qualifiers info + -- ^ 'Class' assertions. + } deriving (Show) + +-- | Make 'State_Class' collectable as a 'State' instance +-- out of a 'Monad' stack. +type instance MC.Class State (State_Class info) = 'True + +instance Empty (State_Class info) where + empty = State_Class + { state_class_directives = mempty + , state_class_env = mempty + , state_class_qualifiers = empty + } +instance Buildable info => State (State_Class info) where + state_name _ = "State_Class" + state_show = Build.text +instance Buildable info => Buildable (State_Class info) where + build State_Class + { state_class_directives + , state_class_env + , state_class_qualifiers + } = + mconcat $ List.intersperse "\n" + [ "class directives: " <> Build.list state_class_directives + , "class environment: " <> Build.list (Map.keys state_class_env) + , "class qualifiers: " + , Build.indent " " state_class_qualifiers + ] + +-- ** Type 'State_Class_Qualifiers' + +data State_Class_Qualifiers info + = State_Class_Qualifiers + { state_class_qualifiers_assumed :: [Infoed info Class_Qualifier] + , state_class_qualifiers_generalized :: [Infoed info Class_Qualifier] + , state_class_qualifiers_toprove :: [Infoed info Class_Qualifier] + -- ^ Once the constraints have been solved, this list should be empty. + } deriving (Show) + +instance Empty (State_Class_Qualifiers info) where + empty = + State_Class_Qualifiers + { state_class_qualifiers_assumed = [] + , state_class_qualifiers_generalized = [] + , state_class_qualifiers_toprove = [] + } +instance Buildable info => Buildable (State_Class_Qualifiers info) where + build State_Class_Qualifiers + { state_class_qualifiers_assumed + , state_class_qualifiers_generalized + , state_class_qualifiers_toprove + } = + Build.unlines + [ "assumed: " <> Build.list state_class_qualifiers_assumed + , "generalized: " <> Build.list state_class_qualifiers_generalized + , "toprove: " <> Build.list state_class_qualifiers_toprove + ] +instance Substitutable (State_Class_Qualifiers info) where + subvars (State_Class_Qualifiers qs gs as) = subvars (infoed <$> (qs <> gs <> as)) + sub `substitute` State_Class_Qualifiers + { state_class_qualifiers_toprove = ps + , state_class_qualifiers_generalized = gs + , state_class_qualifiers_assumed = as + } = + State_Class_Qualifiers + { state_class_qualifiers_toprove = ((sub `substitute`) <$>) <$> ps + , state_class_qualifiers_generalized = ((sub `substitute`) <$>) <$> gs + , state_class_qualifiers_assumed = ((sub `substitute`) <$>) <$> as + } + +-- * Class 'Solver_Class' + +class + ( Solver_Constraint m + , Solver_Monotype m + , Solver_Polytype m + , MC.MonadState (State_Class (Info m)) m + , Infoable (Info_Class (Info m)) (Info m) + , Solver_Logable Log_Class m + ) => Solver_Class m where + error_class :: Error_Class -> Error m + + class_qualifiers :: m (State_Class_Qualifiers (Info m)) + class_qualifiers = + MC.gets $ \(s::State_Class (Info m)) -> + state_class_qualifiers s + class_qualifiers_modify + :: (State_Class_Qualifiers (Info m) -> State_Class_Qualifiers (Info m)) + -> m () + class_qualifiers_modify f = + MC.modify $ \(s::State_Class (Info m)) -> + s{ state_class_qualifiers = + f (state_class_qualifiers s) } + class_qualifier_toprove + :: Info m -> Class_Qualifier -> m () + class_qualifier_toprove info q = do + log $ Log_Class_Qualifier_ToProve q + class_qualifiers_modify $ \quals -> + quals{ state_class_qualifiers_toprove = + Infoed info q : state_class_qualifiers_toprove quals } + class_qualifier_assume + :: Info m -> Class_Qualifier -> m () + class_qualifier_assume info q = do + log $ Log_Class_Qualifier_Assume q + class_qualifiers_modify $ \quals -> + quals{ state_class_qualifiers_assumed = + Infoed info q : state_class_qualifiers_assumed quals } + class_qualifiers_map + :: (Class_Qualifier -> m Class_Qualifier) -> m () + class_qualifiers_map f = do + let g = mapM $ \(Infoed info q) -> + f q >>= \new -> return (Infoed info new) + state_class_qualifiers_toprove <- + (>>= g) $ + MC.gets $ \(s::(State_Class (Info m))) -> + state_class_qualifiers_toprove $ + state_class_qualifiers s + state_class_qualifiers_generalized <- + (>>= g) $ + MC.gets $ \(s::(State_Class (Info m))) -> + state_class_qualifiers_generalized $ + state_class_qualifiers s + state_class_qualifiers_assumed <- + (>>= g) $ + MC.gets $ \(s::(State_Class (Info m))) -> + state_class_qualifiers_assumed $ + state_class_qualifiers s + class_qualifiers_modify $ \quals -> + quals + { state_class_qualifiers_toprove + , state_class_qualifiers_generalized + , state_class_qualifiers_assumed + } + + class_qualifiers_reduced :: m [Class_Qualifier] + class_qualifiers_reduced = do + synotys <- synotype_substitution + clenv <- class_env + quals <- class_qualifiers + return $ fst $ + class_context_reduction + synotys clenv $ infoed <$> ( + state_class_qualifiers_toprove quals <> + state_class_qualifiers_generalized quals <> + state_class_qualifiers_assumed quals + ) + + -- | Generalize a 'Monotype', preserving given 'Rigtype's, + -- and such that the resulting 'Polytype' + -- has all the 'Class_Qualifier's from 'state_class_qualifiers_toprove', + -- when they apply at least on one of the 'quantifiers' of this 'Polytype'. + class_polytype_forall + :: [Rigtype] -> Monotype -> m Polytype + class_polytype_forall rigtys monoty = do + State_Class_Qualifiers + { state_class_qualifiers_toprove = quals_toprove + , state_class_qualifiers_generalized = quals_generalized + } <- class_qualifiers + let rigvas = subvars rigtys + let polyvars = subvars monoty List.\\ rigvas + let has_polyvars = Foldable.any (`List.elem` polyvars) . subvars . infoed + let ( quals_toprove_poly + , quals_toprove_mono + ) = List.partition has_polyvars quals_toprove + let quals_generalized_poly = List.filter has_polyvars quals_generalized + class_qualifiers_modify $ \quals -> + quals + { state_class_qualifiers_toprove = quals_toprove_mono + , state_class_qualifiers_generalized = quals_toprove_poly <> state_class_qualifiers_generalized quals + } + return $ + forall_but rigvas $ + Qualification + (infoed <$> (quals_toprove_poly <> quals_generalized_poly)) + monoty + + class_improve + :: Bool -> m [(Info m, Monotype, Monotype)] + class_improve normal = + if normal + then class_improve_normal + else class_improve_final + class_improve_normal + :: m [(Info m, Monotype, Monotype)] + class_improve_normal = + return [] + class_improve_final + :: m [(Info m, Monotype, Monotype)] + class_improve_final = + return [] + + class_simplify :: m () + class_simplify = do + State_Class_Qualifiers + { state_class_qualifiers_toprove + , state_class_qualifiers_assumed + } <- class_qualifiers + synotys <- synotype_substitution + clenv <- class_env + cldirs <- MC.gets state_class_directives + clquals <- simplify synotys clenv cldirs + state_class_qualifiers_toprove + class_qualifiers_modify $ \quals -> + quals{state_class_qualifiers_toprove = + List.filter (not . class_entails synotys clenv + (infoed <$> state_class_qualifiers_assumed) . infoed) clquals } + where + simplify :: + ( Solver_Constraint m + , Solver_Polytype m + ) => Synotype_Substitution + -> Class_Env + -> [Class_Directive (Info m)] + -> [Infoed (Info m) Class_Qualifier] + -> m [Infoed (Info m) Class_Qualifier] + simplify synotys clenv cldirs clquals = do + hnf' <- go_insts clquals + are_disjoints (go_super_class [] hnf') + where + go_insts + :: [Infoed (Info m) Class_Qualifier] + -> m [Infoed (Info m) Class_Qualifier] + go_insts ts = + (List.concat <$>) <$> + forM ts $ + \q@(Infoed info clqual@(Class_Qualifier clname _)) -> + if is_class_qualifier_normalized clqual + then return [q] + else case class_env_instance_context synotys clenv clqual of + Just inst_context -> + go_insts $ + Infoed (info_insert + (Info_Class_Qualifier_Parent clqual::Info_Class (Info m)) + info) <$> + inst_context + Nothing -> do + constraint_error_insert + (error_class Error_Class_Qualifier_Unresolved) $ + (case cldirs_never of + clql:_ -> info_insert $ Info_Class_Directive_Never clql + [] -> case infos_cldirs_close of + [i] -> info_insert (Info_Class_Directive_Close (Infoed i clname)::Info_Class (Info m)) + _ -> info_insert (Info_Class_Qualifier_Unresolved clqual::Info_Class (Info m))) + info + return [] + where + cldirs_never = + [ Infoed i clql + | Class_Directive_Never clql i <- cldirs + , isJust $ class_qualifier_unification synotys clqual clql + ] + infos_cldirs_close = + [ i + | Class_Directive_Close n i <- cldirs + , n == clname ] + + go_super_class + :: [Infoed (Info m) Class_Qualifier] + -> [Infoed (Info m) Class_Qualifier] + -> [Infoed (Info m) Class_Qualifier] + go_super_class rs [] = rs + go_super_class rs (x:xs) + | class_entails_super_class clenv + (infoed <$> (rs <> xs)) (infoed x) = go_super_class rs xs + | otherwise = go_super_class (x:rs) xs + + are_disjoints + :: [Infoed (Info m) Class_Qualifier] + -> m [Infoed (Info m) Class_Qualifier] + are_disjoints [] = return [] + are_disjoints (t@(Infoed info (Class_Qualifier className ty)):ts) = do + let f t'@(Infoed info' (Class_Qualifier className' ty')) = + case + [ i + | ty == ty' + , Class_Directive_Disjoint ss i <- cldirs + , className `List.elem` ss + , className' `List.elem` ss + ] of + [] -> return ([t'], True) + info_directive : _ -> do + constraint_error_insert + (error_class Error_Class_Qualifier_Disjoint) $ + info_insert + (Info_Class_Directive_Disjoint + (Infoed info className) + (Infoed info' className')) + info_directive + return ([], False) + result <- mapM f ts + let (list, bs) = List.unzip result + rest <- are_disjoints (List.concat list) + return $ if Foldable.and bs then t : rest else rest + + class_ambiguous :: m () + class_ambiguous = do + State_Class_Qualifiers + { state_class_qualifiers_toprove + } <- class_qualifiers + rigvars_rigtypes <- polytype_rigids + forM_ state_class_qualifiers_toprove $ \q_toprove -> + case q_toprove of + Infoed _ Class_Qualifier{class_qualifier_type=Monotype_Var v} -> + case + [ info + | Infoed info (rigvas, _) <- rigvars_rigtypes + , v `List.elem` rigvas + ] of + info:_ -> err_missing q_toprove info + _ -> err_ambiguous q_toprove + _ -> err_ambiguous q_toprove + where + err_ambiguous (Infoed info p) = + constraint_error_insert + (error_class Error_Class_Qualifier_Ambiguous) $ + info_insert + (Info_Class_Qualifier_Ambiguous p::Info_Class (Info m)) info + err_missing q_toprove info = + constraint_error_insert + (error_class Error_Class_Qualifier_Missing) $ + info_insert + (Info_Class_Qualifier_Arising_from q_toprove) info + + class_env :: m Class_Env + class_env = + MC.gets $ \(s::State_Class (Info m)) -> + state_class_env s + class_env_set :: Class_Env -> m () + class_env_set state_class_env = + MC.modify $ \(s::State_Class (Info m)) -> + s{ state_class_env } + +-- | When all 'state_constraint_constraints' have been handled, +-- takes all the remaining 'state_class_qualifiers_toprove', +-- and report them as ambiguities. +class_ambiguities :: + ( Solver_Constraint m + , Solver_Monotype m + , Solver_Polytype m + , Solver_Class m + ) => m () +class_ambiguities = do + class_reduction + class_improve_fix False + class_ambiguous + +-- | Perform context reduction on the 'state_class_qualifiers_toprove', +-- and removes the 'Class_Qualifier's +-- which are entailed by 'state_class_qualifiers_assumed'. +class_reduction :: + ( Solver_Constraint m + , Solver_Monotype m + , Solver_Polytype m + , Solver_Class m + ) => m () +class_reduction = do + monotype_substitution_consistentify + class_qualifiers_map monotype_substitute + class_improve_fix True + class_simplify + +class_improve_fix :: + ( Solver_Constraint m + , Solver_Monotype m + , Solver_Polytype m + , Solver_Class m + ) => Bool -> m () +class_improve_fix normal = do + improvements <- class_improve normal + case improvements of + [] -> return () + _ -> do + forM_ improvements + (\(info, t1, t2) -> monotype_unify info t1 t2) + monotype_substitution_consistentify + class_improve_fix normal + +-- * Class 'Info_Class' + +data Info_Class info + = Info_Class_Qualifier_Ambiguous Class_Qualifier + | Info_Class_Qualifier_Arising_from (Infoed info Class_Qualifier) + | Info_Class_Qualifier_Parent Class_Qualifier + | Info_Class_Qualifier_Unresolved Class_Qualifier + | Info_Class_Directive_Close (Infoed info Text) + | Info_Class_Directive_Disjoint (Infoed info Text) (Infoed info Text) + | Info_Class_Directive_Never (Infoed info Class_Qualifier) + deriving (Eq, Show) + +instance Buildable info => Buildable (Info_Class info) where + build x = + case x of + Info_Class_Qualifier_Ambiguous q -> + "Info_Class_Qualifier_Ambiguous " <> build q + Info_Class_Qualifier_Arising_from q -> + "Info_Class_Qualifier_Arising_from " <> build q + Info_Class_Qualifier_Parent q -> + "Info_Class_Qualifier_Parent " <> build q + Info_Class_Qualifier_Unresolved q -> + "Info_Class_Qualifier_Unresolved " <> build q + Info_Class_Directive_Close n -> + "Info_Class_Directive_Close " <> build n + Info_Class_Directive_Disjoint n1 n2 -> + "Info_Class_Directive_Disjoint " <> build n1 <> " " <> build n2 + Info_Class_Directive_Never q -> + "Info_Class_Directive_Never " <> build q + +-- * Type 'Error_Class' + +data Error_Class + = Error_Class_Qualifier_Ambiguous + -- ^ Example: @forall a. Eq a => Int -> Int@ + | Error_Class_Qualifier_Disjoint + | Error_Class_Qualifier_Missing + | Error_Class_Qualifier_Unresolved + -- ^ A 'Monotype' is missing a required 'Class_Qualifier'. + deriving (Eq, Show) + +-- ** Type 'Log_Class' + +data Log_Class + = Log_Class_Qualifier_Assume Class_Qualifier + | Log_Class_Qualifier_ToProve Class_Qualifier + deriving (Show) +instance Buildable Log_Class where + build x = + case x of + Log_Class_Qualifier_Assume q -> "class_qualifier_assume : " <> build q + Log_Class_Qualifier_ToProve q -> "class_qualifier_toprove : " <> build q diff --git a/Language/LOL/Typing/Solver/Common.hs b/Language/LOL/Typing/Solver/Common.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Solver/Common.hs @@ -0,0 +1,116 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +module Language.LOL.Typing.Solver.Common where + +import Control.Monad (Monad(..)) +import Data.Bool +import Data.Eq (Eq(..)) +import Data.Functor (Functor(..)) +import Data.Monoid ((<>)) +import Data.Text (Text) +import qualified Data.Text as Text +import Data.Text.Buildable (Buildable(..)) +import Text.Show (Show(..)) + +-- * Class 'Information' + +-- | An associated type constructor +-- to attach informations to a 'Constraint' +-- about why it exists. +-- +-- NOTE: an 'Information' should be enough to construct +-- an error message if the 'Constraint' it is associated with +-- leads to an inconsistency. +class (Monad m, Buildable (Info m)) => Information m where + type Info m + +-- ** Class 'Infoable' +class Infoable a info where + info_insert :: a -> info -> info + +-- | A data type constructor to gather informations +-- from the 'Monad' stack of a solver. +-- data family Info (m :: * -> *) + +-- ** Type 'Infoed' + +-- | A data type to associate some @info@ to a value. +data Infoed info a + = Infoed + { information :: info + , infoed :: a + } deriving (Eq, Functor, Show) +instance (Buildable info, Buildable a) => Buildable (Infoed info a) where + build Infoed { information, infoed } = + build infoed <> " {- " <> build information <> " -}" + +-- * Type 'Error' + +-- | A data type constructor to gather errors +-- from the 'Monad' stack of a solver. +data family Error (m :: * -> *) + +-- * Type 'Solver_Logable' + +class Solver_Logable a m where + log :: a -> m () + +-- * Class 'State' + +class State st where + state_name :: st -> Text + state_options :: st -> [Text] + state_collect :: st -> [(Text, Text)] + state_show :: st -> Text + + -- state_show = Text.pack . show + state_options _ = [] + state_collect st = [(state_name st, state_show st)] + +-- * Type 'Option' + +data Option a + = Option + { option_current :: a + , option_default :: a + , option_description :: Text + } + +instance (Show a, Eq a) => Show (Option a) where + show a = + Text.unpack (option_description a) + <> ": " + <> show (option_current a) + <> show_default + where + show_default | option_current a == option_default a = " (default)" + | otherwise = "" +instance (Buildable a, Eq a) => Buildable (Option a) where + build a = + build (option_description a) + <> ": " + <> build (option_current a) + <> build_default + where + build_default | option_current a == option_default a = " (default)" + | otherwise = "" +instance Functor Option where + fmap f a = + a{ option_default = f (option_default a) + , option_current = f (option_current a) } + +option :: a -> Text -> Option a +option a s = + Option + { option_default = a + , option_current = a + , option_description = s + } diff --git a/Language/LOL/Typing/Solver/Constraint.hs b/Language/LOL/Typing/Solver/Constraint.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Solver/Constraint.hs @@ -0,0 +1,256 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +module Language.LOL.Typing.Solver.Constraint where + +import Control.Monad (Monad(..), filterM, forM_, mapM, unless, when) +import Data.Bool +import qualified Data.Foldable as Foldable +import Data.Function (($), (.)) +import Data.Functor (Functor(..), (<$>)) +import qualified Data.List as List +import Data.Maybe (Maybe(..)) +import Data.Monoid (Monoid(..), (<>)) +import Data.Sequence (Seq, (<|)) +import qualified Data.Sequence as Seq +import Data.String (String) +import qualified Data.Text as Text +import Data.Text.Buildable (Buildable(..)) +import Data.Tuple (fst, snd) +import Prelude (error) +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Solver.Common +import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.Instance as MC +import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.StateFix as MC +import Language.LOL.Typing.Lib.Data.Empty (Empty(..)) +import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build + +-- * Type 'Constraint' + +data Constraint m = + forall c. (Show c, Buildable c, Substitutable c) + => Constraint c + (c -> m ()) -- solving strategy + (c -> m Bool) -- semantic check + +instance Show (Constraint m) where + show (Constraint c _ _) = show c +instance Buildable (Constraint m) where + build (Constraint c _ _) = build c +instance Substitutable (Constraint m) where + subvars (Constraint c _ _) = subvars c + sub `substitute` (Constraint c f g) = + Constraint (sub `substitute` c) f g +instance Monad m => Solvable (Constraint m) m where + constraint_solver (Constraint c f _) = f c + constraint_checker (Constraint c _ f) = f c + +-- | Return a 'Constraint' from a 'Solvable' instance. +constraint :: Solvable c m => c -> Constraint m +constraint c = Constraint c constraint_solver constraint_checker + +constraints :: (Solvable c m, Functor f) => f c -> f (Constraint m) +constraints = (constraint <$>) + +constraint_map :: (forall a. m1 a -> m2 a) -> Constraint m1 -> Constraint m2 +constraint_map t (Constraint c f g) = Constraint c (t . f) (t . g) + +-- ** Class 'Solvable' + +-- | A type class for 'Constraint's solvable within a 'Monad'. +class (Show c, Buildable c, Substitutable c, Monad m) => Solvable c m where + constraint_solver :: c -> m () + constraint_checker :: c -> m Bool + constraint_checker _ = return True + +-- * Type 'State_Constraint' + +-- | A 'State_Constraint' is parameterized over the 'Monad' +-- in which the 'Constraint's can be solved. +data State_Constraint m + = State_Constraint + { state_constraint_constraints :: Seq (Constraint m) + -- ^ A stack of 'Constraint's to solve. + , state_constraint_checks :: [(m Bool, String)] + -- ^ Conditions to check (for the solved 'Constraint's). + , state_constraint_errors :: [(Info m, Error m)] + -- ^ The detected errors. + , state_constraint_option_stop :: Option Bool + -- ^ Whether to discard all remaining 'Constraint's after the first error. + , state_constraint_option_check :: Option Bool + -- ^ Whether to check constraint satisfaction afterwards. + } + +-- | Make 'State_Constraint' collectable as a 'State' instance +-- out of a 'Monad' stack. +type instance MC.Class State (State_Constraint m) = 'True + +instance Show (State_Constraint m) where + show = Build.string +instance Buildable (State_Constraint m) where + build State_Constraint + { state_constraint_constraints + , state_constraint_errors + , state_constraint_checks } = + Build.unlines $ + [ "constraints: " <> Build.tuple + [ show (List.length state_constraint_constraints) <> " constraints" + , show (List.length state_constraint_errors) <> " errors" + , show (List.length state_constraint_checks) <> " checks" + ] + ] <> ((" " <>) . build <$> + Foldable.toList state_constraint_constraints) +instance State (State_Constraint m) where + state_name _ = "State_Constraint" + state_show = Build.text + state_options s = + [ Text.pack $ show $ state_constraint_option_stop s + , Text.pack $ show $ state_constraint_option_check s + ] +instance Empty (State_Constraint m) where + empty = State_Constraint + { state_constraint_constraints = mempty + , state_constraint_errors = mempty + , state_constraint_checks = mempty + , state_constraint_option_stop = option False "Stop solving at first error" + , state_constraint_option_check = option False "Check the solution" + } + +-- * Class 'Solver_Constraint' + +class + ( MC.MonadStateFix State_Constraint m + , Information m + , Solver_Logable Log_Constraint m + ) => Solver_Constraint m where + constraint_push :: Constraint m -> m () + constraint_push c = do + log $ Log_Constraint_Push c + MC.modifyFix $ \(s::State_Constraint m) -> + s{ state_constraint_constraints = + c <| state_constraint_constraints s } + + constraint_push_many :: Seq (Constraint m) -> m () + constraint_push_many cs = do + forM_ cs $ log . Log_Constraint_Push + MC.modifyFix $ \(s::State_Constraint m) -> + s{ state_constraint_constraints = + cs <> state_constraint_constraints s } + + constraint_pop :: m (Maybe (Constraint m)) + constraint_pop = do + cs <- MC.getsFix $ \(s::State_Constraint m) -> + state_constraint_constraints s + case Seq.viewl cs of + Seq.EmptyL -> return Nothing + (c Seq.:< state_constraint_constraints) -> do + log $ Log_Constraint_Pop c + MC.modifyFix (\(s::State_Constraint m) -> + s{ state_constraint_constraints }) + return (Just c) + + constraint_discard :: m () + constraint_discard = + MC.modifyFix $ \(s::State_Constraint m) -> + s{ state_constraint_constraints = mempty } + + constraint_error_insert :: Error m -> Info m -> m () + constraint_error_insert err info = do + MC.modifyFix (\(s::State_Constraint m) -> + s{ state_constraint_errors = + (info, err) : state_constraint_errors s }) + stop <- constraint_option_stop + when (option_current stop) + constraint_discard + + constraint_errors :: m [(Info m, Error m)] + constraint_errors = + MC.getsFix $ \(s::State_Constraint m) -> + state_constraint_errors s + + constraint_error_info_update + :: (Info m -> m (Info m)) -> m () + constraint_error_info_update f = do + errs <- constraint_errors + state_constraint_errors <- do + let g (info, err) = do + info' <- f info + return (info', err) + g `mapM` errs + MC.modifyFix $ \(s::State_Constraint m) -> + s{ state_constraint_errors } + + -- | Add sanity checks for the solved 'Constraint's, + -- performed when all 'Constraint's have been solved. + -- + -- The first argument of 'constraint_check_insert' is + -- a message, which is reported + -- when the second argument evaluates + -- to 'False' (in the 'Monad' @m@). + constraint_check_insert :: String -> m Bool -> m () + constraint_check_insert text check = + MC.modifyFix $ \(s::State_Constraint m) -> + s{ state_constraint_checks = + (check, text) : state_constraint_checks s} + + constraint_check_get :: m [(m Bool, String)] + constraint_check_get = + MC.getsFix $ \(s::State_Constraint m) -> + state_constraint_checks s + + constraint_option_stop :: m (Option Bool) + constraint_option_stop = + MC.getsFix $ \(s::State_Constraint m) -> + state_constraint_option_stop s + + constraint_option_check :: m (Option Bool) + constraint_option_check = + MC.getsFix (\(s::State_Constraint m) -> + state_constraint_option_check s) + + constraint_solve :: m () + constraint_solve = do + mc <- constraint_pop + case mc of + Just c -> do + constraint_solver c + constraint_check_insert (show c) (constraint_checker c) + constraint_solve + Nothing -> do + check <- option_current <$> constraint_option_check + errs <- fmap fst <$> constraint_errors + when (check && List.null errs) + constraint_check + + constraint_check :: m () + constraint_check = do + ms <- constraint_check_get + bs <- filterM ((not <$>) . fst) ms + unless (List.null bs) $ + let err = + "\n\n Constraints violated:\n" + <> List.unlines (fmap ((" - " <>) . snd) bs) in + error $ "constraint_check: " <> err + +-- ** Type 'Log_Constraint' + +data Log_Constraint + = forall c. (Show c, Buildable c) => Log_Constraint_Pop c + | forall c. (Show c, Buildable c) => Log_Constraint_Push c +deriving instance Show Log_Constraint +instance Buildable Log_Constraint where + build x = + case x of + Log_Constraint_Pop c -> "constraint_pop : " <> build c + Log_Constraint_Push c -> "constraint_push: " <> build c diff --git a/Language/LOL/Typing/Solver/Greedy.hs b/Language/LOL/Typing/Solver/Greedy.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Solver/Greedy.hs @@ -0,0 +1,67 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} + +-- | The point at which point inconsistency is detected. +-- depends on the ordering of the 'Constraint's +-- and on the 'Solver's used. +-- +-- Because choosing an ordering for the 'Constraint's +-- closely relates to the order in which types are unified (with 'mgu_with_synonyms'), +-- a /greedy 'Constraint' solver/, beeing highly sensitive +-- to the order in which it solves 'Constraint_Monotype_Unification's, +-- will report different 'Constraint's for different orders. +module Language.LOL.Typing.Solver.Greedy where + +import Control.Monad (Monad) +import qualified Control.Monad.Classes as MC +import Data.Bool (Bool(..)) +import Data.Sequence (Seq) +import Data.Text.Buildable (Buildable(..)) + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Solver.Common +import Language.LOL.Typing.Solver.Constraint +import Language.LOL.Typing.Solver.Monotype +import Language.LOL.Typing.Solver.Polytype +import Language.LOL.Typing.Solver.Class +import Language.LOL.Typing.Solver.Monad +import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.StateInstance as MC + +-- * Type 'Solver_Greedy_Finite' + +type Solver_Greedy_Finite info m + = Solver info m Substitution_Finite + +solver_greedy_finite :: + ( sol ~ Solver_Greedy_Finite info m + , res ~ Solver_Result (Info sol) (Error sol) + , Monad m + , Solvable constraint sol + , MC.CansMonadStateInstance State (MC.EffState ()) m ~ '[ 'False ] + , Buildable info + , Infoable Info_Monotype info + , Infoable Info_Polytype info + , Infoable (Info_Class info) info + ) => Solver_Config -> Seq constraint -> sol res +solver_greedy_finite = solver + +-- * Type 'Solver_Greedy_Fixpoint' + +type Solver_Greedy_Fixpoint info m + = Solver info m Substitution_Fixpoint + +solver_greedy_fixpoint :: + ( sol ~ Solver_Greedy_Fixpoint info m + , res ~ Solver_Result (Info sol) (Error sol) + , Monad m + , Solvable constraint sol + , MC.CansMonadStateInstance State (MC.EffState ()) m ~ '[ 'False ] + , Buildable info + , Infoable Info_Monotype info + , Infoable Info_Polytype info + , Infoable (Info_Class info) info + ) => Solver_Config -> Seq constraint -> sol res +solver_greedy_fixpoint = solver diff --git a/Language/LOL/Typing/Solver/Monad.hs b/Language/LOL/Typing/Solver/Monad.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Solver/Monad.hs @@ -0,0 +1,304 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +module Language.LOL.Typing.Solver.Monad where + +import Control.Applicative (Applicative(..)) +import Control.Monad (Monad(..)) +import qualified Control.Monad.Classes as MC +import qualified Control.Monad.Classes.Run as MC +import qualified Control.Monad.Trans.State.Lazy as SL +import Data.Bool +import Data.Eq (Eq(..)) +import Data.Function (($), (.)) +import Data.Functor ((<$>)) +import qualified Data.List as List +import Data.Map.Strict (Map) +import Data.Monoid (Monoid(..), (<>)) +import Data.Ord (Ord(..), max) +import Data.Sequence (Seq) +import Data.Text.Buildable (Buildable(..)) +import Prelude (Num(..)) +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Solver.Common +import Language.LOL.Typing.Solver.Constraint +import Language.LOL.Typing.Solver.Monotype +import Language.LOL.Typing.Solver.Polytype +import Language.LOL.Typing.Solver.Class +import Language.LOL.Typing.Lib.Data.Empty (Empty(..)) +import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.Instance as MC +import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.StateFix as MC +import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.StateInstance as MC +import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build + +-- * Type 'Solver' + +-- | A 'Monad' stack gathering all the @Solver_*@. +-- +-- * @m@ is a base 'Monad' +-- (for instance within which 'Solver_Log's +-- can be handled during the solving). +-- * @info@ is a polymorphic type to hold informations +-- about the origin of the 'Constraint's. +-- * @monotype_substitution@ is a for accumulating known 'Monotype's +-- (for example it can be: 'Substitution_Finite' or 'Substitution_Fixpoint'). +type Solver info m monotype_substitution = + MC.StateLazyFixT State_Constraint + (SL.StateT (State_Monotype monotype_substitution) + (SL.StateT (State_Polytype info) + (SL.StateT (State_Class info) + (WriterT Solver_Log + m)))) + +-- * Type 'Solver_Log' + +data Solver_Log + = Solver_Log_States [MC.Instance State] + -- ^ Logs summarizing the 'State's. + | Solver_Log_Constraint Log_Constraint + -- ^ Log of 'Constraint' handling. + | Solver_Log_Class Log_Class + -- ^ Log of 'Class' handling. + | Solver_Log_Polytype Log_Polytype + -- ^ Log of 'Polytype' handling. + +instance Monad m + => Solver_Logable Log_Constraint (Solver info m sub) where + log = MC.tell . Solver_Log_Constraint +instance Monad m + => Solver_Logable Log_Class (Solver info m sub) where + log = MC.tell . Solver_Log_Class +instance Monad m + => Solver_Logable Log_Polytype (Solver info m sub) where + log = MC.tell . Solver_Log_Polytype + +log_states + :: forall m. + ( MC.MonadWriter Solver_Log m + , MC.MonadStateInstance State m + , Solver_Constraint m + ) => m () +log_states = do + (states::[MC.Instance State]) <- MC.getInstance + MC.tell $ Solver_Log_States states + +-- | Type synonym to 'MC.CustomWriterT', +-- /eta-reduced/ to fit in 'Solver'. +type WriterT w m = MC.CustomWriterT' w m m + +-- * Type 'Solver_Info' + +data Solver_Info info + = Solver_Info_Class (Info_Class info) + | Solver_Info_Monotype Info_Monotype + | Solver_Info_Polytype Info_Polytype + deriving (Eq, Show) +instance Buildable info => Buildable (Solver_Info info) where + build x = + case x of + Solver_Info_Class i -> build i + Solver_Info_Monotype i -> build i + Solver_Info_Polytype i -> build i +instance Buildable info => Buildable [Solver_Info info] where + build = Build.list + +instance + ( Monad m + , Buildable info + ) => Information (Solver info m sub) where + type Info (Solver info m sub) = info + +data instance Error (Solver info m sub) + = Solver_Error_Class Error_Class + | Solver_Error_Monotype Error_Monotype + | Solver_Error_Polytype Error_Polytype + deriving (Eq, Show) + +instance + ( Monad m + , Buildable info + ) => Solver_Constraint (Solver info m sub) +instance + ( Monad m + , Buildable info + , Solver_Monotype_Substitution sub + , Infoable Info_Monotype info + ) => Solver_Monotype (Solver info m sub) where + type Solver_Monotype_Sub (Solver info m sub) = sub + error_monotype = Solver_Error_Monotype +instance + ( Monad m + , Buildable info + , info ~ Info (Solver info m sub) + , Infoable Info_Polytype info + ) => Solver_Polytype (Solver info m sub) where + error_polytype = Solver_Error_Polytype +instance + ( Monad m + , Buildable info + , info ~ Info (Solver info m sub) + , Infoable Info_Monotype info + , Infoable Info_Polytype info + , Infoable (Info_Class info) info + , Solver_Monotype_Substitution sub + ) => Solver_Class (Solver info m sub) where + error_class = Solver_Error_Class + +-- | Return within base 'Monad' @m@. +-- the 'Solver_Result' produced +-- by evaluating the given 'Solver', +-- while using the given 'Solver_Log' handler. +solve :: + ( sol ~ Solver info m sub + , res ~ Solver_Result (Info sol) (Error sol) + , Monad m + , Empty sub + ) => (Solver_Log -> m ()) + -> sol res -> m res +solve writer_log = + MC.evalWriterWith writer_log . + MC.evalStateLazy empty . + MC.evalStateLazy empty . + MC.evalStateLazy empty . + MC.evalStateLazyFix empty + +-- | Return the 'Solver' produced +-- by the given 'Solver_Config' and 'Contraint's. +solver :: + ( sol ~ Solver info m sub + , res ~ Solver_Result (Info sol) (Error sol) + , Monad m + , Solver_Monotype_Substitution sub + , Solvable constraint sol + , MC.CansMonadStateInstance State (MC.EffState ()) m ~ '[ 'False ] + -- NOTE: require that the inner 'Monad' does not have 'State' instances. + , Buildable info + , Infoable Info_Monotype info + , Infoable Info_Polytype info + , Infoable (Info_Class info) info + ) => Solver_Config -> Seq constraint -> sol res +solver cfg cs = do + solver_init cs cfg + solver_run cs + solver_result + +-- | Run the solvers of a 'Monad' over the given 'Constraint's. +solver_run :: + ( Solvable constraint m + , Solver_Constraint m + , Solver_Monotype m + , Solver_Polytype m + , Solver_Class m + , MC.MonadWriter Solver_Log m + , MC.MonadStateInstance State m + ) => Seq constraint -> m () +solver_run cs = do + constraint_push_many $ constraints cs + log_states + constraint_solve + monotype_substitution_consistentify + polytype_rigids_check + class_ambiguities + log_states + +-- ** Type 'Solver_Config' + +data Solver_Config + = Solver_Config + { solver_config_class_env :: Class_Env + , solver_config_freshvar :: Freshvar + , solver_config_synotypes :: Synotype_Substitution + , solver_config_check :: Bool + , solver_config_stop :: Bool + } + +-- | Return a 'Solver_Config'. +solver_config :: Solver_Config +solver_config = + Solver_Config + { solver_config_class_env = class_env_default + , solver_config_freshvar = -1 + , solver_config_synotypes = empty + , solver_config_check = option_current $ state_constraint_option_check empty + , solver_config_stop = option_current $ state_constraint_option_stop empty + } + +-- | Initialize a solver 'Monad' with given 'Solver_Config'. +solver_init :: + forall m constraints. + ( Substitutable constraints + , Solver_Constraint m + , Solver_Polytype m + , Solver_Class m + ) => constraints -> Solver_Config -> m () +solver_init cs cfg = do + polytype_freshvar_set freshvar + synotype_substitution_set $ + solver_config_synotypes cfg + class_env_set $ + solver_config_class_env cfg + MC.modifyFix $ \(s::State_Constraint m) -> + s{ state_constraint_option_check = + (state_constraint_option_check s) + { option_current = solver_config_check cfg } + , state_constraint_option_stop = + (state_constraint_option_stop s) + { option_current = solver_config_stop cfg } + } + where + freshvar + | solver_config_freshvar cfg < 0 = 1 + List.maximum (-1 : subvars cs) + | otherwise = solver_config_freshvar cfg + +-- ** Type 'Solver_Result' + +data Solver_Result info err + = Solver_Result + { solver_result_freshvar :: Freshvar + , solver_result_monotypes :: Substitution_Fixpoint + , solver_result_polytypes :: Polysub + , solver_result_quantifiers :: Map Monovar [Quantifier] + , solver_result_qualifiers :: [Class_Qualifier] + -- ^ 'Class_Qualifier's assumed to hold. + , solver_result_errors :: [(info, err)] + } + +instance Empty (Solver_Result info err) where + empty = mempty +instance Monoid (Solver_Result info err) where + mempty = Solver_Result 0 mempty mempty mempty mempty mempty + mappend + (Solver_Result fr1 ms1 ps1 qts1 qls1 es1) + (Solver_Result fr2 ms2 ps2 qts2 qls2 es2) = + Solver_Result + (fr1 `max` fr2) + (ms1 <> ms2) + (ps1 <> ps2) + (qts1 <> qts2) + (qls1 <> qls2) + (es1 <> es2) + +-- | Return a 'Solver_Result' from a solver 'Monad'. +solver_result :: + ( Solver_Constraint m + , Solver_Monotype m + , Solver_Polytype m + , Solver_Class m + ) => m (Solver_Result (Info m) (Error m)) +solver_result = + Solver_Result + <$> polytype_freshvar + <*> monotype_substitution + <*> polytype_substitution + <*> polytype_quantifiers + <*> class_qualifiers_reduced + <*> constraint_errors diff --git a/Language/LOL/Typing/Solver/Monotype.hs b/Language/LOL/Typing/Solver/Monotype.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Solver/Monotype.hs @@ -0,0 +1,265 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +-- | Type inference for /monomorphic types/. +module Language.LOL.Typing.Solver.Monotype where + +import Control.Monad (Monad(..), mapM) +import qualified Control.Monad.Classes as MC +import Data.Bool +import Data.Either (Either(..)) +import Data.Eq (Eq(..)) +import Data.Function (($), (.), id) +import Data.Int (Int) +import qualified Data.List as List +import qualified Data.Map.Strict as Map +import Data.Maybe (Maybe(..), fromMaybe) +import Data.Monoid (Monoid(..), (<>)) +import Data.Text (Text) +import Data.Text.Buildable (Buildable(..)) +import Data.Tuple (uncurry) +import Prelude (error) +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Solver.Common +import Language.LOL.Typing.Solver.Constraint +import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.Instance as MC +import Language.LOL.Typing.Lib.Data.Empty (Empty(..)) +import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build + +-- * Type 'State_Monotype' + +data State_Monotype sub + = State_Monotype + { state_monotype_substitution :: sub + -- ^ Known 'Monovar's. + , state_monotype_synotypes :: Synotype_Substitution + -- ^ Known 'Synotype's. + } deriving (Show) + +-- | Make 'State_Monotype' collectable as a 'State' instance +-- out of a 'Monad' stack. +type instance MC.Class State (State_Monotype sub) = 'True + +instance Buildable sub => Buildable (State_Monotype sub) where + build State_Monotype + { state_monotype_substitution = sub + , state_monotype_synotypes = synotys + } = + Build.unlines + [ "monotypes: " + , Build.indent " " sub + , "synotypes: " <> build synotys + ] +instance Buildable sub => State (State_Monotype sub) where + state_name _ = "State_Monotype" + state_show = Build.text +instance Empty sub => Empty (State_Monotype sub) where + empty = State_Monotype + { state_monotype_substitution = empty + , state_monotype_synotypes = empty + } + +-- * Class 'Solver_Monotype' + +-- | A type class for 'Monad's containing a 'Substitution', +-- that may be in an inconsistent state. +class + ( Solver_Constraint m + , Monad m + , MC.MonadState (State_Monotype (Solver_Monotype_Sub m)) m + , Solver_Monotype_Substitution (Solver_Monotype_Sub m) + , Infoable Info_Monotype (Info m) + ) => Solver_Monotype (m :: * -> *) where + error_monotype :: Error_Monotype -> Error m + type Solver_Monotype_Sub m + + monotype_substitution :: m Substitution_Fixpoint + monotype_substitution = MC.gets $ + \(s::State_Monotype (Solver_Monotype_Sub m)) -> + monotype_substitution_fixpoint $ + state_monotype_substitution s + + -- | Lookup the value of a 'Monotype_Var' in the substitution. + monotype_lookup :: Monovar -> m Monotype + monotype_lookup v = MC.gets $ + \(s::State_Monotype (Solver_Monotype_Sub m)) -> + fromMaybe (Monotype_Var v) $ + substitution_lookup v $ + state_monotype_substitution s + + -- | Apply the 'Substitution' to any instance of 'Substitutable'. + monotype_substitute :: Substitutable a => a -> m a + monotype_substitute a = do + let subvars_a = subvars a + monotys <- monotype_lookup `mapM` subvars_a + let sub = substitution_finite (List.zip subvars_a monotys) + return (sub `substitute` a) + + -- | Unify two 'Monotype's. + -- + -- NOTE: In the end, the two 'Monotype's should be equivalent + -- under 'monotype_substitution'. However, unifying two 'Monotype's + -- may bring the substitution into an /inconsistent state/. + monotype_unify :: Info m -> Monotype -> Monotype -> m () + monotype_unify info ty1 ty2 = do + synotys <- synotype_substitution + subty1 <- monotype_substitute ty1 + subty2 <- monotype_substitute ty2 + case monotype_substitution_unify + synotys (ty1, subty1) (ty2, subty2) of + Left err -> + constraint_error_insert + (error_monotype $ Error_Monotype_Unification err) + info + Right (_log, uni) -> -- do + -- constraint_log "monotype_unify" log + MC.modify $ \(s::State_Monotype (Solver_Monotype_Sub m)) -> + s{state_monotype_substitution = + uni $ state_monotype_substitution s } + -- | Make 'state_monotype_substitution' consistent. + -- + -- NOTE: Only relevant for 'Substitution' states + -- that can be inconsistent + -- (eg. the /type graph/ substitution state). + monotype_substitution_consistentify :: m () + monotype_substitution_consistentify = return () + + synotype_substitution :: m Synotype_Substitution + synotype_substitution = MC.gets $ + \(s::State_Monotype (Solver_Monotype_Sub m)) -> + state_monotype_synotypes s + synotype_substitution_set :: Synotype_Substitution -> m () + synotype_substitution_set state_monotype_synotypes = + MC.modify $ \(s::State_Monotype (Solver_Monotype_Sub m)) -> + s{ state_monotype_synotypes } + +-- ** Class 'Solver_Monotype_Substitution' + +class + ( Buildable sub + , Show sub + , Monoid sub + , Substitution sub + ) => Solver_Monotype_Substitution sub where + monotype_substitution_fixpoint :: sub -> Substitution_Fixpoint + monotype_substitution_unify + :: Synotype_Substitution + -> (Monotype, Monotype) + -> (Monotype, Monotype) + -> Either Unification_Error (Text, sub -> sub) + +instance Solver_Monotype_Substitution Substitution_Finite where + monotype_substitution_fixpoint = Substitution_Fixpoint + monotype_substitution_unify synotys (_origty1, ty1) (_origty2, ty2) = + case mgu_with_synotypes synotys ty1 ty2 of + Left err -> Left err + Right (_, uni) -> Right $ (Build.text uni,) $ substitution_finite_union uni +instance Solver_Monotype_Substitution Substitution_Fixpoint where + monotype_substitution_fixpoint = id + monotype_substitution_unify synotys (origty1, ty1) (origty2, ty2) = + case mgu_with_synotypes synotys ty1 ty2 of + Left err -> Left err + Right (was_synexpanded, uni) -> + Right $ (Build.text uni,) $ + (if was_synexpanded then subexpand else id) . + subunion uni + where + subunion x (Substitution_Fixpoint y) = + Substitution_Fixpoint $ + (`Map.union` y) $ + Map.fromList + [ (v, fromMaybe (Monotype_Var v) $ substitution_lookup v x) + | v <- substitution_domain x + ] + subexpand = + substitution_fixpoint_synexpand synotys origty2 unity . + substitution_fixpoint_synexpand synotys origty1 unity + unity = + fromMaybe (error "monotype_substitution_unify: types not unifiable") $ + mgt_with_synotypes synotys + (uni `substitute` ty1) + (uni `substitute` ty2) + +-- TODO: understand and test this code better… + +-- NOTE: Top: The key idea is as follows: +-- try to minimize the number of expansions by 'Synotype's. +-- If a type is expanded, then this should be recorded in the substitution. +-- Invariant of this function should be that "atp" (the first type) can be +-- made equal to "utp" (the second type) with a number of 'Synotype' expansions +substitution_fixpoint_synexpand + :: Synotype_Substitution + -> Monotype + -> Monotype + -> Substitution_Fixpoint + -> Substitution_Fixpoint +substitution_fixpoint_synexpand syns = + go + where + go :: Monotype -> Monotype -> Substitution_Fixpoint -> Substitution_Fixpoint + go atp utp original = + case (app_spine_left atp, app_spine_left utp) of + (App_Spine (Monotype_Var i) [], _) -> writeIntType i utp original + ( App_Spine (Monotype_Const s) as + , App_Spine (Monotype_Const t) bs + ) | s == t && not (is_panthom_synotype syns s) -> + List.foldr (uncurry go) original (List.zip as bs) + (App_Spine (Monotype_Const _) _, _) -> + case synexpand_top_step (synotypes syns) atp of + Just atp' -> go atp' utp original + Nothing -> error $ "substitution_fixpoint_synexpand: inconsistent types(1)" <> show (atp, utp) + _ -> error $ "substitution_fixpoint_synexpand: inconsistent types(2)" <> show (atp, utp) + + writeIntType :: Int -> Monotype -> Substitution_Fixpoint -> Substitution_Fixpoint + writeIntType i utp original@(Substitution_Fixpoint fm) = + case Map.lookup i fm of + Nothing -> + case utp of + Monotype_Var j | i == j -> original + _ -> Substitution_Fixpoint (Map.insert i utp fm) + Just atp -> + case (app_spine_left atp, app_spine_left utp) of + (App_Spine (Monotype_Var j) [], _) -> writeIntType j utp original + ( App_Spine (Monotype_Const s) as + , App_Spine (Monotype_Const t) bs + ) | s == t -> + List.foldr (uncurry go) original (List.zip as bs) + (App_Spine (Monotype_Const _) _, _) -> + case synexpand_top_step (synotypes syns) atp of + Just atp' -> writeIntType i utp (Substitution_Fixpoint (Map.insert i atp' fm)) + Nothing -> + -- NOTE: Top: FIX!!! HERSCHRIJVEN! + -- de volgende situatie trad op: + -- utp=Categorie, atp = [Char] + -- met type Categorie = String + case synexpand_top_step (synotypes syns) utp of + Just utp' -> writeIntType i atp (Substitution_Fixpoint (Map.insert i utp' fm)) + Nothing -> error $ "substitution_fixpoint_synexpand: inconsistent types(1)" <> show (i, utp, atp) + _ -> error "substitution_fixpoint_synexpand: inconsistent types(2)" + +-- ** Class 'Info_Monotype' + +data Info_Monotype + = Info_Monotype_Unification Monotype Monotype + deriving (Eq, Show) + +instance Buildable Info_Monotype where + build x = + case x of + Info_Monotype_Unification m1 m2 -> + "Info_Monotype_Unification " <> Build.tuple [m1, m2] + +-- ** Type 'Error_Monotype' + +data Error_Monotype + = Error_Monotype_Unification Unification_Error + deriving (Eq, Show) diff --git a/Language/LOL/Typing/Solver/Polytype.hs b/Language/LOL/Typing/Solver/Polytype.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Solver/Polytype.hs @@ -0,0 +1,352 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +-- | Type inference for /parametric polymorphism/. +module Language.LOL.Typing.Solver.Polytype where + +import Control.Monad (Monad(..), mapM, forM_, foldM, sequence) +import qualified Control.Monad.Classes as MC +import Data.Bool +import Data.Eq (Eq(..)) +import Data.Function (($), flip) +import Data.Functor ((<$>)) +import qualified Data.List as List +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Maybe (Maybe(..)) +import Data.Monoid (Monoid(..), (<>)) +import Data.Text.Buildable (Buildable(..)) +import Data.Tuple (snd) +import Prelude (Num(..), error) +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Solver.Common +import Language.LOL.Typing.Solver.Constraint +import Language.LOL.Typing.Solver.Monotype +import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.Instance as MC +import Language.LOL.Typing.Lib.Data.Default (Default(..)) +import Language.LOL.Typing.Lib.Data.Empty (Empty(..)) +import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build + +-- * Type 'State_Polytype' + +data State_Polytype info + = State_Polytype + { state_polytype_freshvar :: Freshvar + -- ^ An incrementing counter + -- for fresh 'Monovar's, fresh 'Rigvar's, or 'Polyvar's. + , state_polytype_substitution :: Polysub + -- ^ Known 'Polytype's. + , state_polytype_rigids :: [Infoed info ([Rigvar], [Rigtype])] + -- ^ The 'Rigvar's introduced as 'Freshvar's by 'polytype_rigvarify' + -- with the 'Rigtype's from the /typing context/ + -- (used by 'polytype_rigids_check'). + , state_polytype_quantifiers :: Map Monovar [Quantifier] + -- ^ Map every 'Monovar' unified with an instance of a 'Polytype' + -- to the 'Freshvar's allocated to instantiate + -- the 'quantifiers' of this 'Polytype'. + } deriving (Show) + +-- | Make 'State_Polytype' collectable as a 'State' instance +-- out of a 'Monad' stack. +type instance MC.Class State (State_Polytype info) = 'True + +instance Buildable info => Buildable (State_Polytype info) where + build State_Polytype + { state_polytype_freshvar = freshvar + , state_polytype_substitution = polytys + , state_polytype_rigids = rigids + , state_polytype_quantifiers = instances + } = + Build.unlines $ + [ "freshvar: " <> build freshvar + , "rigids: " ] <> + ((" " <>) <$> + List.foldr (\(Infoed info (rigvas, monotys)) -> + ((Build.tuple + [ Build.list rigvas + , Build.list monotys + ] <> " {- " <> build info <> " -}") :) + ) [] rigids) <> + [ "polytypes: " ] <> + Map.foldrWithKey (\v ty -> + ((" p" <> build v <> " == " <> + build (def::Quantification_Build_Options, ty)) :) + ) [] polytys <> + [ "instances: " ] <> + Map.foldrWithKey (\v vs -> + ((" " <> build (Monotype_Var v) <> " -> " <> + Build.list (Monotype_Var <$> vs)) :) + ) [] instances +instance Buildable info => State (State_Polytype info) where + state_name _ = "State_Polytype" + state_show = Build.text +instance Empty (State_Polytype m) where + empty = + State_Polytype + { state_polytype_freshvar = 0 + , state_polytype_substitution = mempty + , state_polytype_rigids = mempty + , state_polytype_quantifiers = mempty + } + +-- * Class 'Solver_Polytype' + +class + ( Solver_Constraint m + , MC.MonadState (State_Polytype (Info m)) m + , Infoable Info_Polytype (Info m) + , Solver_Logable Log_Polytype m + ) => Solver_Polytype m where + error_polytype :: Error_Polytype -> Error m + + polytype_freshvar :: m Freshvar + polytype_freshvar = + MC.gets $ \(s::State_Polytype (Info m)) -> + state_polytype_freshvar s + polytype_freshvar_set :: Freshvar -> m () + polytype_freshvar_set state_polytype_freshvar = + MC.modify $ \(s::State_Polytype (Info m)) -> + s{ state_polytype_freshvar } + + polytype_substitution :: m Polysub + polytype_substitution = + MC.gets $ \(s::State_Polytype (Info m)) -> + state_polytype_substitution s + polytype_insert :: Polyvar -> Polytype -> m () + polytype_insert var polyty = do + log $ Log_Polytype_Insert var polyty + MC.modify $ \(s::State_Polytype (Info m)) -> + s{ state_polytype_substitution = + Map.insert var polyty $ + state_polytype_substitution s + } + polytype_lookup + :: Polytyref -> m Polytype + polytype_lookup polyref = + case polyref of + Polytyref polyty -> return polyty + Polytyref_Var v -> + Map.findWithDefault + (error "polytype_lookup: Polytyref_Var not found in polytype_substitution") + v <$> polytype_substitution + + -- | 'Rigvar' variables + -- + -- NOTE: used by 'polytype_rigids_check'. + polytype_rigids :: m [Infoed (Info m) ([Rigvar], [Rigtype])] + polytype_rigids = + MC.gets $ \(s::State_Polytype (Info m)) -> + state_polytype_rigids s + polytype_rigids_set :: [Infoed (Info m) ([Rigvar], [Rigtype])] -> m () + polytype_rigids_set state_polytype_rigids = + MC.modify $ \(s::State_Polytype (Info m)) -> + s{ state_polytype_rigids } + polytype_rigids_push + :: Infoed (Info m) ([Rigvar], [Rigtype]) -> m () + polytype_rigids_push rig{-@(Infoed info (vs, ms))-} = do + --constraint_log "polytype_rigids_push" + -- (Infoed info (Build.tuple [Build.list vs, Build.list ms])) + rigs <- polytype_rigids + polytype_rigids_set (rig:rigs) + + -- | Return the 'quantified' of the given 'Forall' + -- with the 'quantifiers' 'substitute'd with 'Freshvar's. + -- Also, if the given 'Monotype' is a 'Monotype_Var', + -- and at least one 'Freshvar' has been allocated, + -- record them in the 'State_Polytype'. + polytype_instantiate + :: Substitutable a => Monotype -> Forall a -> m a + polytype_instantiate monoty quant = do + freshvar <- polytype_freshvar + let Unquantification freshvar' a = unquantify_forall freshvar quant + polytype_freshvar_set freshvar' + case monoty of + Monotype_Var monovar -> + case [freshvar..freshvar'-1] of + [] -> return () + fs -> + MC.modify $ \(s::State_Polytype (Info m)) -> + s{ state_polytype_quantifiers = + Map.insert monovar fs $ + state_polytype_quantifiers s + } + _ -> return () + return a + polytype_quantifiers :: m (Map Monovar [Quantifier]) + polytype_quantifiers = + MC.gets $ \(s::State_Polytype (Info m)) -> + state_polytype_quantifiers s + + -- | Like 'rigvarify', but 'unquantify' + -- by using fresh 'Monovar's ('Freshvar') instead of fresh 'Const's ('Rigvar's). + -- + -- NOTE: useful for the 'quantifiers' of a 'Polytype', + -- maintaining a list of 'Rigvar's in 'state_polytype_rigids'. + polytype_rigvarify + :: Substitutable a + => Info m -> [Rigtype] -> Forall a -> m a + polytype_rigvarify info rigtys forall_a = do + freshvar <- polytype_freshvar + let Unquantification freshvar' a = + unquantify_forall freshvar forall_a + polytype_freshvar_set freshvar' + polytype_rigids_push $ + Infoed info ([freshvar .. freshvar'-1], rigtys) + return a + +polytype_rigids_check + :: forall m. + ( Solver_Constraint m + , Solver_Monotype m + , Solver_Polytype m + ) => m () +polytype_rigids_check = + polytype_rigids >>= + rigvars_substitution >>= + check_rigvars_are_mapped_to_vars >>= + check_rigvars_are_mapped_to_different_vars >>= + check_monotys_have_no_rigvar >>= + rigvars_substituted >>= + polytype_rigids_set + -- NOTE: restore the 'Rigvar's + -- which are consistent with the current 'monotype_substitution'. + where + -- | Return the 'Monotype's toward which 'monotype_substitution' + -- maps the given 'Rigvar's. + rigvars_substitution + :: [Infoed (Info m) ([Rigvar] , [Rigtype])] + -> m [Infoed (Info m) ([(Rigvar, Monotype)], [Rigtype])] + rigvars_substitution = + mapM $ \(Infoed info (rigvas, rigtys)) -> do + subtys <- monotype_lookup `mapM` rigvas + return $ Infoed info + ( List.zip rigvas subtys + , rigtys ) + -- | Return the 'Monovar's of the given 'Monotype's which are 'Monotype_Var's. + check_rigvars_are_mapped_to_vars + :: [Infoed (Info m) ([(Rigvar, Monotype)], [Rigtype])] + -> m [Infoed (Info m) ([(Rigvar, Monovar)], [Rigtype])] + check_rigvars_are_mapped_to_vars tochecks = do + let (goods, bads) = + List.foldr + (\i@(Infoed info (rigvars_monotys, rigtys)) (gs, bs) -> + let (rigvars_subvars::Maybe [(Rigvar, Monovar)]) = + sequence $ (\(rig, ty) -> + case ty of + Monotype_Var v -> Just (rig, v) + _ -> Nothing + ) <$> rigvars_monotys in + case rigvars_subvars of + Just x -> (Infoed info (x, rigtys):gs, bs) + Nothing -> (gs, i:bs) + ) + ([], []) + tochecks + forM_ bads $ \(Infoed info (rigvars_monotys, _monotys)) -> + constraint_error_insert + (error_polytype $ Error_Polytype_Rigid_type_mismatch rigvars_monotys) + info + return goods + -- | Return the 'Rigvar's which are injectively mapped to the given 'Monovar's. + check_rigvars_are_mapped_to_different_vars + :: [Infoed (Info m) ([(Rigvar, Monovar)], [Rigtype])] + -> m [Infoed (Info m) ([(Rigvar, Monovar)], [Rigtype])] + check_rigvars_are_mapped_to_different_vars tochecks = do + let (subvars_rigvars::Map Monovar [Rigvar]) = + Map.fromListWith (flip (<>)) + [ (subvar, [rigvar]) + | Infoed _ (rigvars_subvars, _) <- tochecks + , (rigvar, subvar) <- rigvars_subvars + ] + let subvars_colliding_rigvars = + Map.filter + (\l -> case l of { [] -> False; [_] -> False; _ -> True }) + subvars_rigvars + let (goods, bads) = + List.partition + (\(Infoed _ (rigvars_subvars, _)) -> + List.null $ (subvars_colliding `List.intersect`) $ + snd <$> rigvars_subvars) + tochecks + where subvars_colliding = Map.keys subvars_colliding_rigvars + forM_ bads $ \(Infoed info (rigvars_subvars, _)) -> + constraint_error_insert + (error_polytype $ Error_Polytype_Rigid_injectivity_lost $ + Map.fromList + [ (subvar, rigvas) + | (_rigvar, subvar) <- rigvars_subvars + , Just rigvas <- [Map.lookup subvar subvars_colliding_rigvars] + ]) + info + return goods + check_monotys_have_no_rigvar + :: [Infoed (Info m) ([(Rigvar, Monovar)], [Rigtype])] + -> m [Infoed (Info m) ([(Rigvar, Monovar)], [Rigtype])] + check_monotys_have_no_rigvar = + foldM (\goods this@(Infoed info (rigvars_subvars, rigtys)) -> do + rigtys' <- monotype_substitute rigtys + case subvars rigtys' `List.intersect` (snd <$> rigvars_subvars) of + [] -> return (this:goods) + rigvars_escaping -> do + constraint_error_insert + (error_polytype $ Error_Polytype_Rigid_escaping rigvars_escaping) + info + return goods + ) [] + rigvars_substituted + :: [Infoed (Info m) ([(Rigvar, Monovar)], [Rigtype])] + -> m [Infoed (Info m) ([Rigvar], [Rigtype])] + rigvars_substituted checkeds = + return + [ Infoed info (snd <$> rigvars_subvars, rigtys) + | Infoed info ( rigvars_subvars, rigtys) <- checkeds + ] + +-- * Class 'Info_Polytype' + +data Info_Polytype + = Info_Polytype_Instantiated Polytype + | Info_Polytype_Rigidified [Rigtype] Polytype + deriving (Eq, Show) + +instance Buildable Info_Polytype where + build x = + case x of + Info_Polytype_Instantiated p -> + "Info_Polytype_Instantiated " <> build p + Info_Polytype_Rigidified rs p -> + "Info_Polytype_Rigidified " <> Build.list rs <> " " <> build p + +-- * Type 'Error_Polytype' + +data Error_Polytype + = Error_Polytype_Rigid_type_mismatch [(Rigvar, Monotype)] + -- ^ A 'Rigvar' is mapped by the current 'monotype_substitution' + -- to a 'Monotype' which is not a 'Monotype_Var'. + | Error_Polytype_Rigid_injectivity_lost (Map Monovar [Rigvar]) + -- ^ 'Map' of 'Monovar's reached by at least two distincts 'Rigvar's. + | Error_Polytype_Rigid_escaping [Rigvar] + -- ^ Some 'Rigvar's escape via a 'Rigtype'. + deriving (Eq, Show) + +-- ** Type 'Log_Polytype' + +data Log_Polytype + = Log_Polytype_Insert Polyvar Polytype + deriving (Show) +instance Buildable Log_Polytype where + build x = + case x of + Log_Polytype_Insert var polyty -> + "polytype_insert : " <> + build (Polytyref_Var var) <> " == " <> build polyty diff --git a/Language/LOL/Typing/Solver/Test.hs b/Language/LOL/Typing/Solver/Test.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Solver/Test.hs @@ -0,0 +1,510 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Solver.Test where + +import Control.Arrow (second) +import Control.Monad (Monad(..)) +import Data.Bool +import Data.Either (Either(..)) +import Data.Function (($), (.)) +import Data.Functor ((<$>)) +-- import Data.Functor.Identity (Identity(..)) +import Data.Int (Int) +import qualified Data.List as List +import qualified Data.Map.Strict as Map +import Data.Maybe ({-Maybe(..),-} fromMaybe) +import Data.Monoid ((<>)) +import Data.Sequence (Seq) +import Data.String (IsString(..)) +-- import Data.Text (Text) +import qualified Data.Text as Text +import Data.Text.Buildable (Buildable(..)) +-- import qualified Data.Text.IO as Text +import qualified Data.Text.Lazy.Builder as Build +import qualified Data.Text.Lazy.IO as TL +-- import Data.Tuple (fst) +import Prelude (Num(..), error) +import System.IO (IO) +-- import Test.HUnit hiding (test) +import Test.Tasty +import Test.Tasty.HUnit +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type +import Language.LOL.Typing.Expr +import Language.LOL.Typing.Solver +import Language.LOL.Typing.Collect.Constraint +-- import Language.LOL.Typing.Collect.Grammar +import qualified Language.LOL.Typing.Collect.Grammar as Collect +import Language.LOL.Typing.Lib.Data.Default (Default(..)) +import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.Instance as MC +import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build + +-- Convenient instances +instance IsString Polytype where + fromString = polytype . Monotype_Const . fromString +instance Num Monotype where + (+) = Monotype_App + (*) = Monotype_App + abs x = x + signum _ = 0 + negate x = x + fromInteger = Monotype_Var . fromInteger + +type Test_Solver + = Solver_Greedy_Finite Collect_Infos IO + +{- +polytype_of_expr + :: Expr + -> Either (Collect_Error (Info Test_Solver) + (Error Test_Solver)) + Text +polytype_of_expr ex = do + -- Text.putStrLn (Text.pack $ show ex) + let Syn_Expr + { constraints_Syn_Expr = cs + , freshvar_Syn_Expr = freshvar + , monoty_Syn_Expr = monotype + , errors_Syn_Expr = errors + } = wrap_Expr (sem_Expr ex) Inh_Expr + { polytys_Inh_Expr = -- Map.fromList + [ ("eq", polytyref + (Quantification [1] [(1, "a")] $ + [Class_Qualifier "Eq" 1] + .=>. (1.->.1.->."Bool") + :: Polytype)) + ] + , freshvar_Inh_Expr = 0 + } + case errors of + (_:_) -> Left $ Collect_Error_Grammar errors + [] -> + let cs' = {-hussel-} cs in + let cfg = solver_config + { solver_config_freshvar = freshvar + , solver_config_check = True + } in + let (result :: Solver_Result (Info Test_Solver) (Error Test_Solver)) = + runIdentity $ + solve (\_ -> return ()) $ + solver_greedy_finite cfg cs' in + case solver_result_errors result of + [] -> Right $ Build.text $ + (def::Quantification_Build_Options,) $ + for_all $ solver_result_monotypes result `substitute` monotype + errs -> Left $ Collect_Error_Solver errs + +-- | Like 'polytype_of_expr', but more verbose; +-- mainly for debugging. +debug_expr :: Expr -> IO Text +debug_expr ex = do + Text.putStrLn (Text.pack $ Build.string ex) + let Syn_Expr + { constraints_Syn_Expr = cs + , freshvar_Syn_Expr = freshvar + , monoty_Syn_Expr = monotype + , errors_Syn_Expr = errors + } = wrap_Expr (sem_Expr ex) Inh_Expr + { polytys_Inh_Expr = mempty + , freshvar_Inh_Expr = 0 + } + case errors of + (_:_) -> return $ Build.text $ + show (Collect_Error_Grammar errors::Collect_Error Collect_Info (Error Test_Solver)) + [] -> do + let cs' = {-hussel-} cs + let cfg = solver_config + { solver_config_freshvar = freshvar + , solver_config_check = True + } + (result :: Solver_Result (Info (Solver_Greedy_Finite Collect_Infos IO)) + (Error (Solver_Greedy_Finite Collect_Infos IO))) <- + solve write_log $ + solver_greedy_finite cfg cs' + -- (\_ -> return ()) + return $ + case solver_result_errors result of + [] -> Build.text $ + (def::Quantification_Build_Options,) $ + for_all $ solver_result_monotypes result `substitute` monotype + errs -> Build.text $ show $ Collect_Error_Solver errs +-} + +write_log :: Solver_Log -> IO () +write_log l = + case l of + Solver_Log_Constraint x -> + TL.putStrLn $ Build.toLazyText $ "- " <> build x + Solver_Log_Class x -> + TL.putStrLn $ Build.toLazyText $ "- " <> build x + Solver_Log_Polytype x -> + TL.putStrLn $ Build.toLazyText $ "- " <> build x + Solver_Log_States states -> + TL.putStrLn $ Build.toLazyText $ + Build.unlines $ + [ hline ] <> + List.zipWith + (\i (MC.Instance s) -> + build i <> ". " <> build (state_name s) <> "\n" <> + Build.indent " " (Build.unlines $ + (build <$> state_options s) <> + [build $ state_show s])) + [1::Int ..] + states <> + [ hline ] + where + hline :: Build.Builder = build $ Text.replicate 80 "-" + +polytys_env :: [(Name, Polytype)] +polytys_env = + [ ("equal", polytype + (Quantification [1] [(1, "a")] $ + [Class_Qualifier "Eq" 1] + .=>. (1.->.1.->."Bool") + :: Polytype)) + , ("compare", polytype + (Quantification [1] [(1, "a")] $ + [Class_Qualifier "Ord" 1] + .=>. (1.->.1.->."Ordering") + :: Polytype)) + , ("True", polytype + (Quantification [] [] $ + [] .=>. "Bool" + :: Polytype)) + , ("one", polytype + (Quantification [] [] $ + [] .=>. "Int" + :: Polytype)) + , ("pair", polytype + (Quantification [1,2] [] $ + [] .=>. (1.->.2.->.type_Tuple [1,2]) + :: Polytype)) + ] + + +class Collect_Constraints a where + collect_constraints + :: a -> Either (Collect_Error (Info Test_Solver) (Error Test_Solver)) + (Freshvar, Seq Collect_Constraint) +instance Collect_Constraints Expr where + collect_constraints expr = + let Collect.Syn_Expr + { Collect.freshvar_Syn_Expr = freshvar + , Collect.constraints_Syn_Expr = constrs + , Collect.errors_Syn_Expr = errors + } = Collect.wrap_Expr (Collect.sem_Expr expr) + Collect.Inh_Expr + { Collect.polytys_Inh_Expr = (polytyref `second`) <$> polytys_env + , Collect.freshvar_Inh_Expr = 0 + } in + case errors of + errs@(_:_) -> Left $ Collect_Error_Grammar errs + [] -> Right (freshvar, constrs) +instance Collect_Constraints Decl where + collect_constraints decl = + let Collect.Syn_Decl + { Collect.freshvar_Syn_Decl = freshvar + , Collect.constraints_Syn_Decl = constrs + , Collect.errors_Syn_Decl = errors + } = Collect.wrap_Decl (Collect.sem_Decl decl) + Collect.Inh_Decl + { Collect.polytys_Inh_Decl = (polytyref `second`) <$> polytys_env + , Collect.freshvar_Inh_Decl = 0 + } in + case errors of + errs@(_:_) -> Left $ Collect_Error_Grammar errs + [] -> Right (freshvar, constrs) + +infer :: Collect_Constraints a + => Bool -> a + -> IO (Either (Collect_Error (Info Test_Solver) (Error Test_Solver)) + (Solver_Result (Info Test_Solver) (Error Test_Solver))) +infer logging x = + case collect_constraints x of + Left err -> return $ Left err + Right (solver_config_freshvar, constrs) -> do + let cfg = solver_config + { solver_config_freshvar + , solver_config_check = True + } + let wlog = if logging then write_log else (\_ -> return ()) + res <- solve wlog $ solver_greedy_finite cfg constrs + return $ + case solver_result_errors res of + [] -> Right res + errs -> Left $ Collect_Error_Solver errs + +class Collect_Constraints a => Infer_Polytype a where + infer_polytype + :: Bool -> a + -> IO (Either (Collect_Error (Info Test_Solver) (Error Test_Solver)) + Polytype) +instance Infer_Polytype Expr where + infer_polytype logging ex = do + res <- infer logging ex + case res of + Left err -> return $ Left err + Right Solver_Result + { solver_result_monotypes = monosub + , solver_result_qualifiers = quals + } -> return $ Right $ + for_all $ (quals .=>.) $ + (monosub `substitute`) $ + Monotype_Var 0 +instance Infer_Polytype Decl where + infer_polytype logging ex = do + res <- infer logging ex + case res of + Left err -> return $ Left err + Right Solver_Result + { solver_result_monotypes = monosub + , solver_result_polytypes = polysub + } -> return $ Right $ + (monosub `substitute`) $ + fromMaybe (error $ "Oops, Polytype missing" <> show polysub) $ + Map.lookup 0 polysub + + +tests :: TestTree +tests = testGroup "Solver" + [ testGroup "Expr" $ + let test logging input expected = do + p <- infer_polytype logging input + let got = (Build.text . (def::Quantification_Build_Options,)) <$> p + got @?= expected in + let (==>) = test False in + -- let (==>>) = test True in + [ testGroup "SKI" $ + -- DOC: https://en.wikipedia.org/wiki/SKI_combinator_calculus + -- DOC: https://en.wikipedia.org/wiki/B,_C,_K,_W_system + let i = "x".-> "x" in + let k = "x".-> "y".-> "x" in + let s = "x".-> "y".-> "z".-> ("x"!"z") ! ("y"!"z") in + let c = "f".-> "x".-> "y".-> "f"!"y"!"x" in + let b = "f".-> "g".-> "x".-> "f"!("g"!"x") in + let w = "x".-> "y".-> "x"!"y"!"y" in + let t = k in -- True + let f = s ! k in -- False + let no = f ! t in -- not + [ testCase "I" $ i + ==> Right "forall a. a -> a" + , testCase "K" $ k + ==> Right "forall a b. a -> b -> a" + , testCase "S" $ s + ==> Right "forall a b c. (a -> b -> c) -> (a -> b) -> a -> c" + , testCase "B" $ b + ==> Right "forall a b c. (a -> b) -> (c -> a) -> c -> b" + , testCase "B = S (K S) K" $ + (s ! (k!s) ! k) + ==> Right "forall a b c. (a -> b) -> (c -> a) -> c -> b" + , testCase "C" $ c + ==> Right "forall a b c. (a -> b -> c) -> b -> a -> c" + , testCase "C = S (B B S) (K K)" $ + (s ! (b!b!s) ! (k!k)) + ==> Right "forall a b c. (a -> b -> c) -> b -> a -> c" + , testCase "W" $ w + ==> Right "forall a b. (a -> a -> b) -> a -> b" + , testCase "W = S S (S K)" $ + (s ! s ! (s!k)) + ==> Right "forall a b. (a -> a -> b) -> a -> b" + , testCase "W /= S I I" $ + (s!i!i) + ==> Left (Collect_Error_Solver + [( Collect_Infos + [ Collect_Info_Solver (Solver_Info_Monotype $ Info_Monotype_Unification 1 (18 .->. 0)) + , Collect_Info_Grammar (Collect_Info_Grammar_Expr "App") ] + , Solver_Error_Monotype $ + Error_Monotype_Unification $ + Unification_Error_Infinite_type 12 + )]) + , testCase "W W /= W W" $ + (w ! w) + ==> Left (Collect_Error_Solver + [( Collect_Infos + [ Collect_Info_Solver (Solver_Info_Monotype $ Info_Monotype_Unification 1 (10 .->. 0)) + , Collect_Info_Grammar (Collect_Info_Grammar_Expr "App") ] + , Solver_Error_Monotype $ + Error_Monotype_Unification $ + Unification_Error_Infinite_type 13 + )]) + , testCase "S = B (B W) (B B C)" $ + (b ! (b!w) ! (b!b!c)) + ==> Right "forall a b c. (a -> b -> c) -> (a -> b) -> a -> c" + , testCase "I = S K K" $ + (s!k!k) + ==> Right "forall a. a -> a" + , testCase "I = W K" $ + (w ! k) + ==> Right "forall a. a -> a" + , testCase "not" $ no + ==> Right "forall a. a -> a" + ] + , testGroup "Abst" $ + let o = "f".-> "g".-> "x".-> "f"!("g"!"x") in + [ testCase "(x:Int) -> x" $ + (("x", "Int"::Monotype)..-> "x") + ==> Right "Int -> Int" + , testCase "(x:Int) -> (x:Bool)" $ + (("x", "Int"::Monotype)..-> ("x".:("Bool"::Monotype))) + ==> Left (Collect_Error_Solver + [ ( Collect_Infos + [ Collect_Info_Solver (Solver_Info_Monotype (Info_Monotype_Unification 2 "Bool")) + , Collect_Info_Solver (Solver_Info_Polytype (Info_Polytype_Rigidified [1] "Bool")) + , Collect_Info_Grammar (Collect_Info_Grammar_Expr "Annot Bool") ] + , Solver_Error_Monotype (Error_Monotype_Unification (Unification_Error_Constant_clash "Int" "Bool"))) + ]) + , testCase "(x:Int -> Int) -> x" $ + (("x", "Int".->."Int")..-> "x") + ==> Right "(Int -> Int) -> Int -> Int" + , testCase "x -> y" $ + ("x".-> "y") + ==> Left (Collect_Error_Grammar [Collect_Error_Grammar_Variable_not_in_scope "y"]) + , testCase "compose" $ o + ==> Right "forall a b c. (a -> b) -> (c -> a) -> c -> b" + , testCase "twice" $ + ("f".-> "x".-> "f"!("f"!"x")) + ==> Right "forall a. (a -> a) -> a -> a" + , testCase "twice = \\f -> f . f" $ + ("f".-> "c" .= o $ "c"!"f"!"f") + ==> Right "forall a. (a -> a) -> a -> a" + , testCase "(x y) z" $ + ("x".-> "y".-> "z".-> "x"!"y"!"z") + ==> Right "forall a b c. (a -> b -> c) -> a -> b -> c" + , testCase "x (y z)" $ + ("x".-> "y".-> "z".-> "x"!("y"!"z")) + ==> Right "forall a b c. (a -> b) -> (c -> a) -> c -> b" + , testCase "x u v t" $ + ("x".-> "y".-> "z".-> "t".-> + "y" ! ("u".-> ("t" ! (("z"!"u") ! ("v".-> "x"!"u"!"v"!"t"))))) + ==> Right "forall a b c d e f. (a -> b -> (c -> d) -> e) -> ((a -> d) -> f) -> (a -> (b -> e) -> c) -> (c -> d) -> f" + , testCase "x -> x x" $ + ("x".-> "x"!"x") + ==> Left (Collect_Error_Solver + [( Collect_Infos + [ Collect_Info_Solver (Solver_Info_Monotype $ Info_Monotype_Unification 3 (4 .->. 2)) + , Collect_Info_Grammar (Collect_Info_Grammar_Expr "App") ] + , Solver_Error_Monotype $ + Error_Monotype_Unification $ + Unification_Error_Infinite_type 1 + )]) + , testCase "y -> (x -> x) y y" $ + ("y".-> ("x".-> "x")!"y"!"y") + ==> Left (Collect_Error_Solver + [( Collect_Infos + [ Collect_Info_Solver (Solver_Info_Monotype $ Info_Monotype_Unification 3 (8 .->. 2)) + , Collect_Info_Grammar (Collect_Info_Grammar_Expr "App") ] + , Solver_Error_Monotype $ + Error_Monotype_Unification $ + Unification_Error_Infinite_type 1 + )]) + , testCase "x -> (a b c -> a c) (x -> x) (f -> f x x)" $ + ("x".-> ("a".-> "b".-> "c".-> "a"!"c") ! ("x".-> "x") ! ("f".-> "f"!"x"!"x")) + ==> Right "forall a b. a -> b -> b" + ] + , testGroup "Let" + [ testCase "top_example_4_7" $ + ("x".-> + "f".= ("g".= "x" $ "a".-> "g") $ + "h".= "f" $ "h"!"x") + ==> Right "forall a. a -> a" + , testCase "(i:Int) -> let (f:Int) = i in f" $ + (("i", "Int"::Monotype)..-> + (("f", "Int"::Monotype)..= "i") "f") + ==> Right "Int -> Int" + , testCase "i -> let (f:forall a. a -> a) = i in f" $ + ("i".-> (("f", for_all ([] .=>. (1 .->. 1)))..= "i") "f") + ==> Left (Collect_Error_Solver + [( Collect_Infos [ Collect_Info_Grammar (Collect_Info_Grammar_Expr "Let(sig) forall a. a -> a") ] + , Solver_Error_Polytype (Error_Polytype_Rigid_escaping [6]) + )]) + , testCase "(i:Int) -> let (f:Bool) = i in f" $ + (("i", "Int"::Monotype)..-> + (("f", "Bool"::Monotype)..= "i") "f") + ==> Left (Collect_Error_Solver + [( Collect_Infos + [ Collect_Info_Solver (Solver_Info_Monotype (Info_Monotype_Unification 4 (Monotype_Const "Bool"))) + , Collect_Info_Solver (Solver_Info_Polytype (Info_Polytype_Rigidified [1] "Bool")) + , Collect_Info_Grammar (Collect_Info_Grammar_Expr "Let(sig) Bool") ] + , Solver_Error_Monotype $ + Error_Monotype_Unification $ + Unification_Error_Constant_clash "Int" "Bool" + )]) + , testCase "a -> b -> a" $ + ("x".-> "f".= ("y".->"x") $ "f") + ==> Right "forall a b. a -> b -> a" + ] + , testGroup "Annot" $ + let id = "x".-> "x" in + [ testCase "id : a -> a" $ + (id .: for_all ([] .=>. (1 .->. 1))) + ==> Right "forall a. a -> a" + , testCase "id : Int -> Int" $ + (id .: for_all ([] .=>. ("Int" .->. "Int"))) + ==> Right "Int -> Int" + , testCase "id /: a -> Int" $ + (id .: for_all ([] .=>. (1 .->. "Int"))) + ==> Left (Collect_Error_Solver + [( Collect_Infos [ Collect_Info_Grammar (Collect_Info_Grammar_Expr "Annot forall a. a -> Int") ] + , Solver_Error_Polytype $ + Error_Polytype_Rigid_type_mismatch + [(3, Monotype_Const "Int")] ) + ]) + , testCase "id /: a -> b" $ + (id .: for_all ([] .=>. (1 .->. 2))) + ==> Left (Collect_Error_Solver + [( Collect_Infos [ Collect_Info_Grammar (Collect_Info_Grammar_Expr "Annot forall a b. a -> b") ] + , Solver_Error_Polytype $ + Error_Polytype_Rigid_injectivity_lost $ + Map.fromList [(3, [3, 4])] ) + ]) + ] + {- + , testGroup "Class" $ + let (==>) input (expected::Text) = do + got <- ((Build.text . (def::Quantification_Build_Options,)) <$>) + <$> polytype_of_expr input + -- Text.putStrLn ("exp: " <> Build.text term) + got @?= Right expected in + [ testCase "Eq a => a -> Bool" $ + ("x".-> "=="!"x"!"x") + -- ("f".= ("x".-> "=="!"x"!"x") "f") + ==> "forall a. Eq a => a -> Bool" + ] + , testGroup "Class" $ + let test logging input (expected::Text) = do + p <- polytype_of_decl logging input + let got = (Build.text . (def::Quantification_Build_Options,)) <$> p + got @?= Right expected in + let (==>) = test False in + let (==>>) = test True in + [ testCase "Eq a => a -> a -> Bool" $ + Decl_Let Nothing "f" "==" + ==> "forall a. Eq a => a -> a -> Bool" + , testCase "Eq a => a -> Bool" $ + Decl_Let Nothing "f" + ("x".-> "=="!"x"!"x") + ==> "forall a. Eq a => a -> Bool" + , testCase "Eq a => a -> Bool" $ + Decl_Let Nothing "f" + ("x".-> "=="!("=="!"x"!"x")!("=="!"x"!"x")) + ==> "forall a. Eq a => a -> Bool" + , testCase "Ord a => a -> Bool" $ + Decl_Let Nothing "f" ("x".-> + "==" + !("=="!"x"!"x") + !("==" + !("compare"!"x"!"x") + !("compare"!"x"!"x"))) + ==> "forall a. Ord a => a -> Bool" + , testCase "a -> b -> a" $ + Decl_Let Nothing "f" + ("x".-> "g".= ("y".->"x") $ "g") + ==>> "forall a b. a -> b -> a" + ] + -} ] + ] diff --git a/Language/LOL/Typing/Test.hs b/Language/LOL/Typing/Test.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Test.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Test where + +import Data.Function (($)) +import System.IO (IO) +import Test.Tasty + +import qualified Type.Test +-- import qualified Collect.Test +import qualified Solver.Test +import qualified Expr.Test + +main :: IO () +main = + defaultMain $ testGroup "Tests" + [ Type.Test.tests + -- , Collect.Test.tests + , Solver.Test.tests + , Expr.Test.tests + ] diff --git a/Language/LOL/Typing/Type.hs b/Language/LOL/Typing/Type.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Type.hs @@ -0,0 +1,22 @@ +-- | All submodules, in a topological order. +module Language.LOL.Typing.Type + ( module Language.LOL.Typing.Type.Monotype + , module Language.LOL.Typing.Type.Substitution + , module Language.LOL.Typing.Type.Synotype + , module Language.LOL.Typing.Type.Unification + , module Language.LOL.Typing.Type.Quantification + , module Language.LOL.Typing.Type.Qualification + , module Language.LOL.Typing.Type.Class + , module Language.LOL.Typing.Type.Polytype + , module Language.LOL.Typing.Type.Kind + ) where + +import Language.LOL.Typing.Type.Monotype +import Language.LOL.Typing.Type.Substitution +import Language.LOL.Typing.Type.Synotype +import Language.LOL.Typing.Type.Unification +import Language.LOL.Typing.Type.Quantification +import Language.LOL.Typing.Type.Qualification +import Language.LOL.Typing.Type.Class +import Language.LOL.Typing.Type.Polytype +import Language.LOL.Typing.Type.Kind diff --git a/Language/LOL/Typing/Type/Class.hs b/Language/LOL/Typing/Type/Class.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Type/Class.hs @@ -0,0 +1,402 @@ +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +-- | /type class/. +-- +-- __Ressources:__ +-- +-- * /Type classes: exploring the design space/, +-- Simon Peyton Jones, Mark Jones, Erik Meijer, 1997, +-- http://research.microsoft.com/en-us/um/people/simonpj/Papers/type-class-design-space/multi.ps.gz +-- +-- * /Implementing, and Understanding Type Classes/, +-- Oleg Kiselyov, 2014, +-- http://okmij.org/ftp/Computation/typeclass.html +module Language.LOL.Typing.Type.Class where + +import Control.Arrow (first) +import Control.Monad (mapM) +import Data.Bool +import Data.Either (Either(..)) +import Data.Eq (Eq(..)) +import qualified Data.Foldable as Foldable +import Data.Function (($), (.), flip) +import Data.Functor ((<$>)) +import qualified Data.List as List +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Maybe (Maybe(..), maybe) +import Data.Monoid ((<>)) +import Data.Text (Text) +import Data.Text.Buildable (Buildable(..)) +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type.Monotype +import Language.LOL.Typing.Type.Substitution (Substitutable(..)) +import Language.LOL.Typing.Type.Synotype +import Language.LOL.Typing.Type.Unification +import Language.LOL.Typing.Type.Qualification + +-- * Type 'Class' + +data Class + = Class + { class_supers :: [Class_Name] -- ^ /adjacent super classes/ + , class_instances :: [Class_Instance] -- ^ /class instances/ + } deriving (Eq, Show) + +-- ** Type 'Class_Instance' + +data Class_Instance + = Class_Instance + { class_instance_head :: Class_Qualifier + , class_instance_context :: [Class_Qualifier] + } deriving (Eq, Show) + +-- ** Type 'Class_Qualifier' + +data Class_Qualifier + = Class_Qualifier + { class_qualifier_name :: Class_Name + , class_qualifier_type :: Monotype + } deriving (Eq, Show) + +-- | Right associative alias for 'Qualification'. +(.=>.) :: [Class_Qualifier] -> a -> Qualification [Class_Qualifier] a +(.=>.) = Qualification +infixr 2 .=>. + +instance Buildable Class_Qualifier where + build (Class_Qualifier q ty) = + build q <> " " <> build ty +instance Substitutable Class_Qualifier where + subvars = subvars . class_qualifier_type + sub `substitute` p = p{class_qualifier_type = + sub `substitute` class_qualifier_type p} +instance Has_Monoconsts Class_Qualifier where + monoconsts p = monoconsts (class_qualifier_type p) +instance Has_Monotypes Class_Qualifier where + monotypes q = [class_qualifier_type q] + monotypes_map f q = q{class_qualifier_type = f (class_qualifier_type q)} + +-- | Return the 'Unification' (when it exists) +-- of two given 'Class_Qualifier's, +-- using given 'Synotype_Substitution'. +class_qualifier_unification + :: Synotype_Substitution + -> Class_Qualifier + -> Class_Qualifier + -> Maybe Unification +class_qualifier_unification syns + (Class_Qualifier na1 ty1) + (Class_Qualifier na2 ty2) + | na1 == na2 = + case mgu_with_synotypes syns (constify ty1) ty2 of + Left _ -> Nothing + Right (_, uni) -> Just (unconstify <$> uni) + | otherwise = Nothing + +-- ** Type 'Class_Env' + +type Class_Env = Map Class_Name Class +type Class_Name = Text +type Class_Path = [Class_Name] + +class_env_empty :: Class_Env +class_env_empty = Map.empty + +class_env_default :: Class_Env +class_env_default = Map.fromList + [ ("Num",) + Class + { class_supers = ["Eq", "Show"] + , class_instances = + [ Class_Instance (Class_Qualifier "Num" ty) [] + | ty <- [type_Int, type_Float] + ] + } + , ("Enum",) + Class + { class_supers = [] + , class_instances = + [ Class_Instance (Class_Qualifier "Enum" ty) [] + | ty <- [type_Unit, type_Int, type_Float, type_Bool, type_Char] + ] + } + , ("Eq",) + Class + { class_supers = [] + , class_instances = + Class_Instance + { class_instance_head = Class_Qualifier "Eq" "Ordering" + , class_instance_context = [] + } : + instances_Eq_Ord_Show "Eq" + } + , ("Ord",) + Class + { class_supers = ["Eq"] + , class_instances = instances_Eq_Ord_Show "Ord" + } + , ("Show",) + Class + { class_supers = [] + , class_instances = instances_Eq_Ord_Show "Show" + } + ] + where + instances_Eq_Ord_Show name = + Class_Instance -- NOTE: List instance + { class_instance_head = Class_Qualifier name (type_List (Monotype_Var 0)) + , class_instance_context = [Class_Qualifier name (Monotype_Var 0)] + } : + [ Class_Instance + { class_instance_head = Class_Qualifier name ty + , class_instance_context = [] + } + | ty <- [type_Bool, type_Char, type_Float, type_Int] + ] <> + (inst_tuples <$> (0 : [2..10])) + where + inst_tuples i = + Class_Instance + { class_instance_head = + Class_Qualifier name (type_Tuple [ Monotype_Var n | n <- [1..i] ]) + , class_instance_context = + [ Class_Qualifier name (Monotype_Var n) + | n <- [1..i] + ] + } + +-- | Return given 'Class_Env' +-- with given 'Class_Name' +-- mapping to a 'Class' +-- with given 'Class_Instance'. +class_env_insert_instance + :: Class_Name + -> Class_Instance + -> Class_Env -> Class_Env +class_env_insert_instance name inst = + Map.insertWith + (\_new old -> old{class_instances = inst : class_instances old}) + name Class + { class_supers = [] + , class_instances = [inst] + } + +-- | Return whether given 'Class_Env' +-- has a 'Class' with given 'Class_Name'. +class_env_has :: Class_Env -> Class_Name -> Bool +class_env_has = flip Map.member + +-- | Return the 'class_supers' +-- associated to the given 'Class_Name', +-- in given 'Class_Env'. +-- +-- Example: @'class_env_supers' 'class_env_default' \"Ord\" '==' [\"Eq\"]@ +class_env_supers :: Class_Env -> Class_Name -> [Class_Name] +class_env_supers env name = maybe [] class_supers $ Map.lookup name env + +-- | Return the 'Class_Path's +-- between given 'Class_Name's +-- in given 'Class_Env'. +class_env_super_path + :: Class_Env + -> Class_Name -> Class_Name + -> [Class_Path] +class_env_super_path env from to + | from == to = [[to]] + | otherwise = + [ from : path + | super <- class_env_supers env from + , path <- class_env_super_path env super to + ] + +-- | Return the 'Class_Instance's +-- of given 'Class_Name' within given 'Class_Env'. +class_env_instances + :: Class_Env -> Class_Name -> [Class_Instance] +class_env_instances env name = + maybe [] class_instances $ + Map.lookup name env + +-- | Return all the 'Class_Qualifier's +-- of all the 'class_supers' +-- of the given 'Class_Qualifier', +-- within given 'Class_Env'. +class_env_supers_all + :: Class_Env + -> Class_Qualifier + -> [Class_Qualifier] +class_env_supers_all env p@(Class_Qualifier name ty) = + p : List.concat + [ class_env_supers_all env (Class_Qualifier supers ty) + | supers <- class_env_supers env name + ] + +-- | Return the 'class_instance_context' +-- 'substitute'd by the 'class_qualifier_unification' +-- of the first 'class_instance_head' +-- unifying with given 'Class_Qualifier', +-- within given 'Class_Env', +-- and using given 'Synotype_Substitution'. +class_env_instance_context + :: Synotype_Substitution + -> Class_Env + -> Class_Qualifier + -> Maybe [Class_Qualifier] +class_env_instance_context syns env qual@(Class_Qualifier qname _) = + Foldable.msum + [ context inst + | inst <- class_env_instances env qname + ] + where + context :: Class_Instance -> Maybe [Class_Qualifier] + context Class_Instance{class_instance_head, class_instance_context} = do + uni <- class_qualifier_unification syns qual class_instance_head + Just (uni `substitute` class_instance_context) + +-- ** Normalization + +class_qualifier_normalize + :: Synotype_Substitution + -> Class_Env + -> Class_Qualifier + -> Maybe [Class_Qualifier] +class_qualifier_normalize syns env p + | is_class_qualifier_normalized p = Just [p] + | otherwise = do + ctx <- class_env_instance_context syns env p + class_context_normalize syns env ctx + +is_class_qualifier_normalized :: Class_Qualifier -> Bool +is_class_qualifier_normalized (Class_Qualifier _ ty) = go ty + where + go (Monotype_Var _) = True + go (Monotype_Const _) = False + go (Monotype_App t _) = go t + +class_context_normalize + :: Synotype_Substitution + -> Class_Env + -> [Class_Qualifier] + -> Maybe [Class_Qualifier] +class_context_normalize syns env ps = + List.concat <$> + mapM (class_qualifier_normalize syns env) ps + +-- ** Entailment + +class_entails + :: Synotype_Substitution + -> Class_Env + -> [Class_Qualifier] + -> Class_Qualifier + -> Bool +class_entails syns env quals qual = + class_entails_super_class env quals qual || + case class_env_instance_context syns env qual of + Nothing -> False + Just insts -> Foldable.all (class_entails syns env quals) insts + +-- | Return whether a given 'Class' +-- implies another as a 'class_supers'. +class_entails_super_class + :: Class_Env + -> [Class_Qualifier] + -> Class_Qualifier + -> Bool +class_entails_super_class env ps p = + Foldable.any + (p `List.elem`) + (class_env_supers_all env <$> ps) + +class_entails_all + :: Synotype_Substitution + -> Class_Env + -> [Class_Qualifier] + -> [Class_Qualifier] + -> Bool +class_entails_all syns env ps = + Foldable.all (class_entails syns env ps) + +-- ** Type 'Class_Reduction_Error' + +newtype Class_Reduction_Error a + = Class_Reduction_Error a + deriving (Show) + +-- | Reduce a 'Class' context by performing: +-- +-- 1. Simplification using 'Class_Instance's. +-- +-- Example: @Eq (a, b)@ is simplified to @Eq a@ and @Eq b@. +-- +-- Example: @Eq Int@ is removed. +-- +-- Example: @Num Bool@ (whose 'Class_Instance' does not exist) +-- gives a 'Class_Reduction_Error'. +-- +-- 2. Removal of 'Class'es entailed by 'class_supers'. +-- +-- Example: Because @Eq@ is the superclass of @Ord@, @Ord a@ 'class_entails' @Eq a@, +-- which therefore can safely be removed when @Ord a@ is present. +-- +-- 3. Removal of duplicate 'Class'es. +class_context_reduction + :: Synotype_Substitution + -> Class_Env + -> [Class_Qualifier] + -> ( [Class_Qualifier] + , [Class_Reduction_Error Class_Qualifier] + ) +class_context_reduction syns env = + first (go []) . List.foldr fold ([], []) + where + fold qual (quals, errs) = + case class_qualifier_normalize syns env qual of + Just qs -> (qs <> quals, errs) + Nothing -> (quals, Class_Reduction_Error qual : errs) + go rs [] = rs + go rs (q:qs) + | entailed = go rs qs + | otherwise = go (q:rs) qs + where entailed = class_entails_super_class env (rs <> qs) q + +{- +context_reduction_associated + :: Synotype_Substitution + -> Class_Env + -> [(Class_Qualifier, a)] + -> ( [(Class_Qualifier, a)] + , [Class_Reduction_Error (Class_Qualifier, a)] + ) +context_reduction_associated syns env = + first (go []) . List.foldr fold ([], []) + where + fold (qual, a) (reduced, es) = + case class_qualifier_normalize syns env qual of + Just qs -> ([(p, a) | p <- qs] <> reduced, es) + Nothing -> (reduced, Class_Reduction_Error (qual, a) : es) + go rs [] = rs + go rs (q:qs) + | entailed = go rs qs + | otherwise = go (q:rs) qs + where + entailed = class_entails_super_class env + (fst <$> (rs <> qs)) (fst q) +-} + +-- * Type 'Class_Directive' + +data Class_Directive info + = Class_Directive_Never Class_Qualifier info + | Class_Directive_Close Class_Name info + | Class_Directive_Disjoint [Class_Name] info + | Class_Directive_Default Class_Name [Monotype] info + deriving (Eq, Show) + +instance Buildable info => Buildable (Class_Directive info) where + build _ = "Class_Directive" + -- FIXME: write it. diff --git a/Language/LOL/Typing/Type/Kind.hs b/Language/LOL/Typing/Type/Kind.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Type/Kind.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +module Language.LOL.Typing.Type.Kind where + +import Data.Function (($)) +import Data.Int (Int) +import Data.List ((++)) +import qualified Data.List as List +import Data.String (String) +import qualified Data.Text as Text +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type.Monotype +import Language.LOL.Typing.Type.Polytype +import Language.LOL.Typing.Type.Substitution +import Language.LOL.Typing.Type.Quantification + +-- * Type 'Monokind' + +type Monokind = Monotype +type Polykind = Polytype + +-- | The kind of all 'Type's. +star :: Monokind +star = Monotype_Const "*" + +-- | In traditional /kind inference systems/, +-- a kind cannot contain /kind variables/. +-- At some point in the inference process +-- the /kind variables/ are defaulted to 'star'. +monokind_vars_to_star :: Monokind -> Monokind +monokind_vars_to_star ki = sub `substitute` ki + where + sub = substitution_finite + [ (v, star) + | v <- subvars ki + ] + +-- | A function to show kinds. +show_Monokind :: Monokind -> String +show_Monokind ki = show (sub `substitute` ki) + where + sub = substitution_finite + [ (v, Monotype_Const (Text.pack ('k':show v))) + | v <- subvars ki + ] + +show_Polykind :: Polykind -> String +show_Polykind polyki = show (sub `substitute` quantified polyki) + where + sub = substitution_finite $ + [ (v1, Monotype_Const (Text.pack ('k':show v2))) + | (v1, v2) <- List.zip (quantifiers polyki) [1 :: Int ..] + ] ++ + [ (v, Monotype_Const (Text.pack ("_k"++show v))) + | v <- subvars polyki + ] diff --git a/Language/LOL/Typing/Type/Monotype.hs b/Language/LOL/Typing/Type/Monotype.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Type/Monotype.hs @@ -0,0 +1,373 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +module Language.LOL.Typing.Type.Monotype where + +import Data.Bool +import Data.Either (Either(..), either) +import Data.Eq (Eq(..)) +import Data.Function (($), (.), id) +import Data.Functor (Functor(..), (<$>)) +import Data.Int (Int) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Maybe (Maybe(..), maybe, isNothing) +import Data.Monoid (Monoid(..), (<>)) +import Data.Ord (Ord(..)) +import Data.String (IsString(..)) +import Data.Text (Text) +import Data.Text.Buildable (Buildable(..)) +import Prelude (Num(..)) +import Text.Read (read) +import Text.Show (Show(..)) +import qualified Data.Char as Char +import qualified Data.Foldable as Foldable +import qualified Data.List as List +import qualified Data.Text as Text + +import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build + +-- * Type 'Monotype' + +-- | A /monomorphic type/ (aka. /monotype/). +-- +-- NOTE: all 'Monotype's that can be constructed are NOT necessarily well-formed. +-- +-- NOTE: however, a useful typing of this type language +-- is added by separating 'Monotype', 'Polytype' and 'Polytyref' +-- in order to indicate where to expect a 'Polyvar' or a 'Polytyref_Var'. +data Monotype + = Monotype_App Monotype Monotype -- ^ /binary type application/ + | Monotype_Const Monoconst -- ^ /type constant/ + | Monotype_Var Monovar -- ^ /type variable/ + deriving (Eq, Ord, Show) + +instance Buildable Monotype where + build = build . (precedence_Toplevel,) +instance Buildable (Precedence, Monotype) where + build (prec, typ) + | prec >= precedence typ = Build.parens (go typ) + | otherwise = go typ + where + go ty = + case app_spine_left ty of + Monotype_Var v `App_Spine` [] -> "m" <> build v + Monotype_Const c `App_Spine` [] -> build c + Monotype_Const "->" `App_Spine` [t1, t2] -> + build (precedence_Fun, t1) <> + " -> " <> + build (precedence_previous precedence_Fun, t2) + Monotype_Const "[]" `App_Spine` [t1] -> + "[" <> build t1 <> "]" + Monotype_Const (is_Tuple -> True) `App_Spine` tys -> + Build.tuple (build <$> tys) + t `App_Spine` tys -> + mconcat $ List.intersperse " " $ + (build . (precedence_App,)) <$> (t : tys) +instance IsString Monotype where + fromString = Monotype_Const . fromString + +-- * Type 'Precedence' + +-- | A /binding precedence/ for an operator. +newtype Precedence + = Precedence Int + deriving (Eq, Ord, Show) + +-- ** Class 'Has_Precedence' + +class Has_Precedence a where + precedence :: a -> Precedence +instance Has_Precedence Monotype where + precedence ty = + case app_spine_left ty of + Monotype_Const "->" `App_Spine` [_, _] -> precedence_Fun + Monotype_Const "[]" `App_Spine` [_] -> precedence_Atomic + Monotype_Const (is_Tuple -> True) `App_Spine` _ -> precedence_Atomic + _ `App_Spine` [] -> precedence_Atomic + _ -> precedence_App + +precedence_previous :: Precedence -> Precedence +precedence_previous (Precedence p) = Precedence (p - 1) + +-- ** Convenient 'Precedence's +precedence_Toplevel :: Precedence +precedence_Toplevel = Precedence 0 +precedence_Fun :: Precedence +precedence_Fun = Precedence 1 +precedence_App :: Precedence +precedence_App = Precedence 2 +precedence_Atomic :: Precedence +precedence_Atomic = Precedence 3 + +-- ** Type 'Monoconst' + +-- | A /type constant/. +type Monoconst = Text + +-- ** Type 'Monoconsts' + +-- | A context of 'Monoconst's, without duplicates. +type Monoconsts = Map Monoconst () + +-- *** Class 'Has_Monoconsts' + +-- | Return the 'Monoconst's of a 'Monotype', without duplicates. +class Has_Monoconsts a where + monoconsts :: a -> Monoconsts + +instance Has_Monoconsts Monotype where + monoconsts ty = + case ty of + Monotype_Var _ -> Map.empty + Monotype_Const c -> Map.singleton c () + Monotype_App t1 t2 -> monoconsts t1 `Map.union` monoconsts t2 + +{- +-- | Return the 'Monoconst's of a 'Has_Monotypes' instance, without duplicates. +monoconsts_from :: Has_Monotypes a => a -> [Monoconst] +monoconsts_from = + List.nub . List.concatMap go . monotypes + where + go (Monotype_Var _) = [] + go (Monotype_Const c) = [c] + go (Monotype_App t1 t2) = go t1 `List.union` go t2 +-} + +-- | Infinite list of unique 'Monoconst's: +-- @a, b, .., z, a1, b1 .., z1, a2, ..@ +const_pool :: [Monoconst] +const_pool = + [ Text.singleton n + | n <- ['a'..'z'] + ] <> + [ Text.pack (n:show i) + | n <- ['a'..'z'] + , i <- [1 :: Int ..] + ] + +-- | Return given 'Monoconst' renamed a bit to avoid +-- conflicting with any given 'Monoconst's. +const_freshify + :: Monoconsts + -> Monoconst + -> (Monoconsts, Monoconst) +const_freshify consts_used const = + let ints = [1..] :: [Int] in + let fresh_const = + List.head + [ x + | extra <- "" : (show <$> ints) + , x <- [const <> Text.pack extra] + , isNothing (Map.lookup x consts_used) + ] in + ( Map.insert fresh_const () consts_used + , fresh_const ) + +-- | Return given 'Monotype' +-- with all its 'Monotype_Var's +-- turned into 'Monotype_Const's. +-- +-- NOTE: each 'Monovar' being mapped to a 'Monoconst' +-- prefixing by an underscore ('_') +-- the 'show'ed 'Int' of the 'Monovar'. +constify :: Monotype -> Monotype +constify ty = + case ty of + Monotype_Var v -> Monotype_Const $ Text.pack ('_':show v) + Monotype_Const s -> Monotype_Const s + Monotype_App l r -> Monotype_App (constify l) (constify r) + +-- | Return given 'Monotype' +-- with all previously 'constify'ed 'Monovar's +-- turned back into 'Monotype_Var's. +unconstify :: Monotype -> Monotype +unconstify ty = + case ty of + Monotype_Var v -> Monotype_Var v + Monotype_Const (Text.uncons -> Just ('_', c)) + | not (Text.null c) + && Text.all Char.isDigit c -> + Monotype_Var (read $ Text.unpack c) + Monotype_Const c -> Monotype_Const c + Monotype_App l r -> Monotype_App + (unconstify l) + (unconstify r) + +-- *** Useful 'Monoconst's + +type_Bool :: Monotype +type_Bool = Monotype_Const "Bool" +type_Char :: Monotype +type_Char = Monotype_Const "Char" +type_Float :: Monotype +type_Float = Monotype_Const "Float" +type_Int :: Monotype +type_Int = Monotype_Const "Int" +type_String :: Monotype +type_String = Monotype_Const "String" + +-- | Constructs a function 'Monotype' from one 'Monotype' to another. +type_Fun :: Monotype -> Monotype -> Monotype +type_Fun t1 = Monotype_App (Monotype_App (Monotype_Const "->") t1) + +-- | Right associative alias for 'type_Fun'. +(.->.) :: Monotype -> Monotype -> Monotype +(.->.) = type_Fun +infixr 0 .->. + +-- | For instance, @(type_List type_Int)@ represents @[Int]@ +type_List :: Monotype -> Monotype +type_List = Monotype_App (Monotype_Const "[]") + +-- | For instance, @(type_IO type_Bool)@ represents @(IO Bool)@ +type_IO :: Monotype -> Monotype +type_IO = Monotype_App (Monotype_Const "IO") + +-- | A carthesian product of zero or more 'Monotype'. +-- For instance @(type_Tuple [])@ represents @()@, +-- and @(type_Tuple [type_Char, type_String])@ represents @(Char, String)@. +type_Tuple :: [Monotype] -> Monotype +type_Tuple tys = List.foldl Monotype_App (Monotype_Const name) tys + where + name | Foldable.null tys = "()" + | otherwise = Text.pack $ "("<>List.replicate (List.length tys - 1) ','<>")" + +-- | The unit type. A special instance of 'type_Tuple'. +type_Unit :: Monotype +type_Unit = type_Tuple [] + +-- ** Type 'Monovar' + +-- | A /monomorphic type variable/: +-- a place-holder for a 'Monotype' that is not yet known, +-- but that become available at some time during 'Constraint' solving. +type Monovar = Int + +-- | Return the list of 'Monovar's of a 'Monotype', without duplicates. +monovars :: Monotype -> [Monovar] +monovars ty = + case ty of + Monotype_Var v -> [v] + Monotype_Const _ -> [] + Monotype_App t1 t2 -> monovars t1 `List.union` monovars t2 + +-- * Type 'App' + +-- | A /binary 'Monotype' application/. +type App = Monotype -> Monotype -> Monotype + +-- | Left associative alias for 'Monotype_App'. +(.!.) :: Monotype -> Monotype -> Monotype +(.!.) = Monotype_App +infixl 5 .!. + +-- | 'Monotype_App'ly given 'Monotype's to given 'Monotype'. +monoapp :: Monotype -> [Monotype] -> Monotype +monoapp = List.foldl Monotype_App + +-- ** Type 'App_Spine' + +-- | A /application spine/ of a 'Monotype'. +data App_Spine + = App_Spine + { app_spine_end :: Monotype + , app_spine :: [Monotype] + } + +-- | Return the /left 'App_Spine'/ of a 'Monotype_App'. +-- +-- EXAMPLE: if type @t@ is @Either Bool [Int]@, +-- then @app_spine_left t@ is @(Either, [Bool, [Int]])@. +app_spine_left :: Monotype -> App_Spine +app_spine_left = go [] + where + go tys (Monotype_App t1 t2) = go (t2:tys) t1 + go tys ty = App_Spine ty tys + +-- | Return the /right 'App_Spine'/ of a 'Monotype'. +-- +-- EXAMPLE: if type @t@ is @Int -> (Bool -> String)@, +-- then @app_spine_right t@ is @([Int, Bool], String)@. +app_spine_right :: Monotype -> App_Spine +app_spine_right = go [] + where + go tys (Monotype_App (Monotype_App (Monotype_Const "->") t1) t2) = go (t1:tys) t2 + go tys ty = App_Spine ty (List.reverse tys) + +-- | Return the /right 'App_Spine'/ of a 'Monotype' upto a maximal length. +app_spine_right_upto :: Int -> Monotype -> App_Spine +app_spine_right_upto maxlen ty = + let a `App_Spine` as = app_spine_right ty in + let (bs, cs) = List.splitAt maxlen as in + List.foldr (.->.) a cs `App_Spine` bs + +-- ** Type 'Arity' + +-- | The /arity of a 'Monotype'/, +-- i.e. the total number of expected arguments of a 'Monotype'. +type Arity = Int + +-- | Return the 'Arity' of a 'Monotype'. +type_arity :: Monotype -> Arity +type_arity = List.length . app_spine . app_spine_right + +-- * 'Monotype' predicates +is_Var :: Monotype -> Bool +is_Var (Monotype_Var _) = True +is_Var _ = False + +is_Const :: Monotype -> Bool +is_Const (Monotype_Const _) = True +is_Const _ = False + +is_App :: Monotype -> Bool +is_App (Monotype_App _ _) = True +is_App _ = False + +is_Fun :: Monotype -> Bool +is_Fun (Monotype_App (Monotype_App (Monotype_Const "->") _) _) = True +is_Fun _ = False + +is_Tuple :: Monoconst -> Bool +is_Tuple (Text.uncons -> Just ('(', t)) + | Text.null t = False + | otherwise = Text.all (',' ==) (Text.init t) && Text.last t == ')' +is_Tuple _ = False + +is_IO :: Monotype -> Bool +is_IO (Monotype_App (Monotype_Const "IO") _) = True +is_IO _ = False + +-- * Class 'Has_Monotypes' + +class Has_Monotypes a where + monotypes :: a -> [Monotype] + monotypes_map :: (Monotype -> Monotype) -> a -> a + +instance Has_Monotypes Monotype where + monotypes ty = [ty] + monotypes_map = ($) +instance Has_Monotypes a => Has_Monotypes [a] where + monotypes = List.concatMap monotypes + monotypes_map f = (monotypes_map f <$>) +instance Has_Monotypes a => Has_Monotypes (Maybe a) where + monotypes = maybe [] monotypes + monotypes_map = fmap . monotypes_map +instance (Has_Monotypes a, Has_Monotypes b) => Has_Monotypes (Either a b) where + monotypes = either monotypes monotypes + monotypes_map f = either (Left . monotypes_map f) (Right . monotypes_map f) + +-- ** Class 'Monotypeable' + +-- | A type class to convert something into a 'Monotype' +class Monotypeable a where + monotype :: a -> Monotype +instance Monotypeable Monotype where + monotype = id +instance Monotypeable Monovar where + monotype = Monotype_Var +instance Monotypeable Monoconst where + monotype = Monotype_Const diff --git a/Language/LOL/Typing/Type/Polytype.hs b/Language/LOL/Typing/Type/Polytype.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Type/Polytype.hs @@ -0,0 +1,122 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Language.LOL.Typing.Type.Polytype where + +import Data.Bool +import qualified Data.Foldable as Foldable +import Data.Functor ((<$>)) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Function ((.), id) +import qualified Data.List as List +import Data.Monoid ((<>)) +import Data.Text.Buildable (Buildable(..)) +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type.Monotype +import Language.LOL.Typing.Type.Substitution +import Language.LOL.Typing.Type.Quantification +import Language.LOL.Typing.Type.Qualification +import Language.LOL.Typing.Type.Class +import Language.LOL.Typing.Lib.Data.Default (Default(..)) + +-- * Type 'Polytype' + +-- | A /rank-1 polymorphic type/ (aka. /polytype/), with qualifiers. +type Polytype + = Forall (Qualification [Class_Qualifier] Monotype) +instance Buildable Polytype where + build x = build (def::Quantification_Build_Options, x) +instance Has_Monoconsts Polytype where + monoconsts Quantification{quantified = Qualification quals monoty} = + Map.unions (monoconsts monoty : (monoconsts <$> quals)) + +-- | Return a 'Polytype' /generalizing/ the given 'Monotype': +-- +-- * quantifying all its 'Monovar's (which thus become /polymorphic/) +-- except the given 'Monovar's (which thus remain /monomorphic/), +-- * and qualifying them by the given 'Class_Qualifier's +-- which use at least one of them. +polytype_but + :: [Monovar] -> [Class_Qualifier] + -> Monotype -> Polytype +polytype_but vars_mono quals monoty = + forall_in vars_poly Qualification + { qualifiers = List.filter is_quantified quals + , qualified = monoty + } + where + vars_poly = subvars monoty List.\\ vars_mono + is_quantified = Foldable.any (`List.elem` vars_poly) . subvars + +-- | A /type with qualifiers/, constructed from a 'Monotype' +-- and some 'Class_Qualifier's (aka. /class context/). +-- +-- These 'Class_Qualifier's put restrictions on certain 'Monovar's. +type Qualified_Type + = Qualification [Class_Qualifier] Monotype + +-- ** Class 'Polytypeable' + +-- | A type class to convert something into a 'Polytype' +class Polytypeable a where + polytype :: a -> Polytype +instance Polytypeable Monotype where + polytype = quantification . ([] .=>.) +instance Polytypeable (Qualification [Class_Qualifier] Monotype) where + polytype = quantification +instance Polytypeable Polytype where + polytype = id + +-- | Return the 'Arity' of a 'Polytype'. +polytype_arity :: Polytype -> Arity +polytype_arity = type_arity . qualified . quantified + +-- | Return whether the given 'Polytype' contains 'Class_Qualifier's. +is_polytype_qualified :: Polytype -> Bool +is_polytype_qualified = not . Foldable.null . qualifiers . quantified + +-- * Type 'Polysub' + +-- | A /polymorphic type substitution/. +type Polysub = Map Polyvar Polytype + +-- | A /polymorphic type variable/: +-- a place-holder for a 'Polytype' that is not yet known, +-- but that become available at some time during 'Constraint' solving. +-- +-- NOTE: is to 'Polytype', what a 'Monovar' is to a 'Monotype'. +type Polyvar = Quantifier + +-- * Type 'Polytyref' + +data Polytyref + = Polytyref Polytype + | Polytyref_Var Polyvar + deriving (Show) + +instance Buildable Polytyref where + build r = + case r of + Polytyref polyty -> build (def::Quantification_Build_Options, polyty) + Polytyref_Var v -> "p" <> build v +instance Substitutable Polytyref where + subvars (Polytyref polyty) = subvars polyty + subvars (Polytyref_Var _) = [] + + _ `substitute` r@(Polytyref_Var _) = r + sub `substitute` (Polytyref s) = Polytyref (sub `substitute` s) + +-- ** Class 'Polytyrefable' + +class Polytyrefable a where + polytyref :: a -> Polytyref + +instance Polytyrefable Monotype where polytyref = Polytyref . polytype +instance Polytyrefable Polytype where polytyref = Polytyref . polytype +instance Polytyrefable Polytyref where polytyref = id +instance Polytyrefable Polyvar where polytyref = Polytyref_Var +instance Polytyrefable Qualified_Type where polytyref = Polytyref . polytype diff --git a/Language/LOL/Typing/Type/Qualification.hs b/Language/LOL/Typing/Type/Qualification.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Type/Qualification.hs @@ -0,0 +1,84 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +module Language.LOL.Typing.Type.Qualification where + +import Data.Eq (Eq) +import qualified Data.Foldable as Foldable +import Data.Function (($), (.)) +import Data.Functor (Functor(..), (<$>)) +import qualified Data.List as List +import Data.Monoid (Monoid(..), (<>)) +import Text.Show (Show(..)) +import Data.Text.Buildable (Buildable(..)) + +import Language.LOL.Typing.Type.Monotype +import Language.LOL.Typing.Type.Substitution +import Language.LOL.Typing.Type.Quantification + +-- * Type 'Qualification' + +-- | A 'Qualification' introduces constraints on 'Monotype_Var's. +-- +-- Example: the qualified 'Polytype': @forall a. Eq a => [a] -> [a]@ +-- restricts @a@ to the members of the 'Class' @Eq@. +-- +-- Example: @forall a b. (a ~ b) => a -> b@ +-- could be an alternative formulation for the 'Polytype' +-- of the /identity function/. +data Qualification qs a + = Qualification + { qualifiers :: qs + , qualified :: a + } deriving (Eq, Show) + +-- | Qualify the 'subvars' of given 'a' (except those in given @context@) +-- with given @[qualifier]@. +qualify_but :: + ( Substitutable qualifier + , Substitutable a + ) => [Monovar] -> [qualifier] -> a + -> Qualification [qualifier] a +qualify_but vars_mono quals qualified = + Qualification + { qualifiers = List.filter is_quantified quals + , qualified + } + where + vars_poly = subvars qualified List.\\ vars_mono + is_quantified = Foldable.any (`List.elem` vars_poly) . subvars + +instance Functor (Qualification qt) where + fmap f q = q{qualified = f (qualified q)} +instance Buildable q => Buildable + ( Quantification_Build_Options + , Qualification [q] Monotype + ) where + build (_opts, q) = build q + +instance + ( Substitutable q + , Substitutable a + ) => Substitutable (Qualification q a) where + subvars q = subvars (qualifiers q) `List.union` subvars (qualified q) + sub `substitute` q = Qualification + { qualifiers = sub `substitute` qualifiers q + , qualified = sub `substitute` qualified q + } +instance (Has_Monotypes q, Has_Monotypes a) => Has_Monotypes (Qualification q a) where + monotypes = monotypes . qualifiers + monotypes_map f q = Qualification + { qualifiers = monotypes_map f $ qualifiers q + , qualified = monotypes_map f $ qualified q + } +instance (Buildable q, Buildable a) + => Buildable (Qualification [q] a) where + build Qualification{qualifiers, qualified} = + (case qualifiers of + [] -> "" + [q] -> build q <> " => " + _ -> "(" <> mconcat (List.intersperse ", " $ build <$> qualifiers) <> ") => " + ) <> + build qualified diff --git a/Language/LOL/Typing/Type/Quantification.hs b/Language/LOL/Typing/Type/Quantification.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Type/Quantification.hs @@ -0,0 +1,464 @@ +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +module Language.LOL.Typing.Type.Quantification where + +import Data.Bool +import Data.Eq (Eq) +import qualified Data.Foldable as Foldable +import Data.Function (($), (.)) +import Data.Functor (Functor(..), (<$>)) +import Data.Int (Int) +import qualified Data.List as List +import qualified Data.Map.Strict as Map +import Data.Maybe (Maybe(..), fromMaybe, maybeToList, isNothing) +import Data.Monoid (Monoid(..), (<>)) +import Data.Proxy (Proxy(..)) +import Data.Text (Text) +import qualified Data.Text as Text +import Data.Text.Buildable (Buildable(..)) +import Data.Tuple (fst) +import Prelude (Num(..)) +import Text.Read (read) +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type.Monotype +import Language.LOL.Typing.Type.Substitution +import Language.LOL.Typing.Lib.Data.Default (Default(..)) + +-- * Type 'Quantification' + +-- | 'Universal' and 'Existential' /quantification of 'Monotype's/. +-- +-- A 'Quantification' is an abstract interpretation +-- of an expression that can be inlined in many places. +data Quantification quantification_type a + = Quantification + { quantifiers :: [Quantifier] + -- ^ /quantifying type variables/ + , quantifier_hintnames :: [Quantifier_Hinted] + -- ^ original names used for some 'quantifiers' + -- (likely to carry some meaning for a human) + , quantified :: a + -- ^ value upon which the 'Quantification' applies + } deriving (Eq, Show) + +-- | A type synonym indicating a /quantifying type variable/: +-- a /type variable/ bound by a 'Quantification'. +type Quantifier = Monovar + +quantification :: a -> Quantification quantification_type a +quantification = Quantification mempty mempty + +quantify + :: Substitutable a + => [Monovar] -> a + -> Quantification qt a +quantify quantifiers quantified = + Quantification + { quantifiers + , quantifier_hintnames = [] + , quantified + } + +quantify_rigvars + :: Rigvarifiable a + => [Rigvar] -> a + -> Quantification qt a +quantify_rigvars quantifiers a = + Quantification + { quantifiers + , quantifier_hintnames = [] + , quantified = [ (v, Monotype_Var v) | v <- quantifiers ] `rigidvars_substitute` a + } + +instance Functor (Quantification quantification_type) where + fmap f q = q{quantified = f (quantified q)} +instance Substitutable a => Substitutable (Quantification quantification_type a) where + -- | NOTE: the 'subvars' of a 'Quantification' + -- do not include the 'quantifiers'. + subvars q = subvars (quantified q) List.\\ quantifiers q + sub `substitute` q = q{ quantified = + substitution_domain_remove (quantifiers q) sub + `substitute` quantified q } +instance Has_Monotypes a => Has_Monotypes (Quantification quantification_type a) where + monotypes = monotypes . quantified + monotypes_map f q = q{ quantified = monotypes_map f $ quantified q } +{- +instance + ( Buildable (Quantification_Build_Options, a) + , Substitutable a + ) => Buildable (Quantification q a) where + build q = build ((def::Quantification_Build_Options), q) +-} + +-- ** Type 'Quantifier_Freshname' + +-- | A 'Quantifier_Name' for a 'Quantifier', +-- which is unique with respect to some 'Monoconst's. +type Quantifier_Freshname = (Quantifier, Quantifier_Name) +type Quantifier_Name = Monoconst +-- | A 'Quantifier_Name' for a 'Quantifier', +-- to be used as a hint to determine a 'Quantifier_Freshname'. +type Quantifier_Hinted = (Quantifier, Quantifier_Name) +-- | A 'Quantifier' without any hint +-- to determine a 'Quantifier_Freshname'. +type Quantifier_Hintless = Quantifier + +-- | Return 'Quantifier_Freshname's +-- for given 'Quantifier's, +-- without using any of given 'Monoconst's. +quantifiers_freshify + :: Monoconsts -- ^ 'Monoconst's already used. + -> [Quantifier_Hinted] -- ^ Hints to use. + -> [Quantifier] -- ^ 'Quantifier's to freshify. + -> (Monoconsts, [Quantifier_Freshname]) -- ^ Fresh 'Quantifier_Name's, and 'Monoconst's now used. +quantifiers_freshify consts_used hints quants = + quantifiers_hint_freshify consts_used $ + quantifiers_hint_partition hints quants + +-- | Partition between 'Quantifier_Hinted' and 'Quantifier_Hintless'. +quantifiers_hint_partition + :: [Quantifier_Hinted] -- ^ Hints to use. + -> [Quantifier] -- ^ 'Quantifier's to partition. + -> ([Quantifier_Hinted], [Quantifier_Hintless]) +quantifiers_hint_partition hints = + List.foldr (\q (yes, no) -> + case List.lookup q hints of + Nothing -> (yes, q:no) + Just n -> ((q, n):yes, no)) + mempty + +-- | Return 'Quantifier_Freshname's +-- for given hinted and hintless 'Quantifier's, +-- without using any of given 'Monoconst's. +quantifiers_hint_freshify + :: Monoconsts -- ^ 'Monoconst's already used. + -> ([Quantifier_Hinted], [Quantifier_Hintless]) -- ^ 'Quantifier's to freshify. + -> (Monoconsts, [Quantifier_Freshname]) -- ^ 'Monoconst's now used, and Fresh 'Quantifier_Name's. +quantifiers_hint_freshify consts_used (quants_hinted, quants_hintless) = + let (consts_used', quants_hinted_fresh) = + quantifiers_freshify_hinted consts_used quants_hinted in + let (consts_used'', quants_hintless_fresh) = + quantifiers_freshify_hintless consts_used' quants_hintless in + let quants_fresh = quants_hinted_fresh <> quants_hintless_fresh in + (consts_used'', quants_fresh) + +-- | Rename a bit any hinted 'Quantifier_Name' +-- in order to avoid capturing given 'Monoconst's: +-- by appending an increasing integer suffix +-- to any given 'Quantifier_Hinted' colliding. +quantifiers_freshify_hinted + :: Monoconsts -- ^ 'Monoconst's already used. + -> [Quantifier_Hinted] -- ^ 'Quantifier's to freshify. + -> (Monoconsts, [Quantifier_Freshname]) -- ^ 'Monoconst's now used, and Fresh 'Quantifier_Name's. +quantifiers_freshify_hinted monoconsts_used = + List.foldr freshify (monoconsts_used, []) + where + freshify + :: (Quantifier, Quantifier_Name) + -> (Monoconsts, [Quantifier_Hinted]) + -> (Monoconsts, [Quantifier_Freshname]) + freshify (q, name) (consts_used, qnames) = + let ints = [1..] :: [Int] in + let fresh_name = + List.head + [ x + | extra <- "" : (show <$> ints) + , x <- [name <> Text.pack extra] + , isNothing (Map.lookup x consts_used) + ] in + ( Map.insert fresh_name () consts_used + , (q, fresh_name):qnames ) + +quantifiers_freshify_hintless + :: Monoconsts -- ^ 'Monoconst's already used. + -> [Quantifier_Hintless] -- ^ 'Quantifier's to freshify. + -> (Monoconsts, [Quantifier_Freshname]) -- ^ 'Monoconst's now used, and Fresh 'Quantifier_Name's. +quantifiers_freshify_hintless consts_used quants = + let fresh_qnames = List.zip quants (const_pool List.\\ Map.keys consts_used) in + let fresh_consts = Map.fromList $ (\(_, x) -> (x, ())) <$> fresh_qnames in + ( Map.union fresh_consts consts_used + , fresh_qnames ) + +-- ** Type 'Quantification_Build_Options' + +data Quantification_Build_Options + = Quantification_Build_Options + { quantification_build_option_consts_used :: Monoconsts + -- ^ The context of 'Monoconst's not to be captured + -- by the 'quantifiers' to output. + , quantification_build_option_force_var_names :: Bool + -- ^ Output 'quantifiers' like other 'subvars' + -- instead of using 'quantifier_hintnames' and 'const_pool'. + , quantification_build_option_show_toplevel_quantifiers :: Bool + -- ^ Output a declaration for the 'quantifiers', + -- + -- Example: @forall a b.@ + -- + -- Example: @exists a b.@ + , quantification_build_option_use_hints :: Bool + -- ^ Whether to use 'quantifier_hintnames' + -- to output the 'quantifiers'. + , quantification_build_option_var_prefix :: Text + -- ^ A prefix for 'subvars' which are not 'quantifiers'. + } + +instance Default Quantification_Build_Options where + def = + Quantification_Build_Options + { quantification_build_option_consts_used = mempty + , quantification_build_option_force_var_names = False + , quantification_build_option_show_toplevel_quantifiers = True + , quantification_build_option_use_hints = True + , quantification_build_option_var_prefix = "m" + } +instance Buildable (Quantification_Build_Options, Monotype) where + build (_opts, ty) = build ty +instance + ( Buildable (Quantification_Build_Options, a) + , Buildable (Proxy qt) + , Substitutable a + ) => Buildable (Quantification_Build_Options, Quantification qt a) where + build + ( opts@Quantification_Build_Options + { quantification_build_option_consts_used + , quantification_build_option_force_var_names + , quantification_build_option_show_toplevel_quantifiers + , quantification_build_option_use_hints + , quantification_build_option_var_prefix + } + , Quantification + { quantifiers + , quantifier_hintnames + , quantified + } ) = + let subvas = subvars quantified in + let quants = quantifiers `List.intersect` subvas in + -- NOTE: hide unused 'quantifiers'. + let (consts_used, freshnames_quanted) = + if quantification_build_option_force_var_names + then (quantification_build_option_consts_used, []) + else + quantifiers_hint_freshify + quantification_build_option_consts_used $ + if quantification_build_option_use_hints + then quantifiers_hint_partition quantifier_hintnames quants + else ([], quants) in + let freshnames_quantless = + (\v -> -- NOTE: find a name for the non-quantifying substitutable 'Monovar's. + (v, quantification_build_option_var_prefix <> Text.pack (show v)) + ) <$> (subvas List.\\ (fst <$> freshnames_quanted)) in + let freshsub = substitution_finite $ + (Monotype_Const <$>) <$> (freshnames_quanted <> freshnames_quantless) in + (if quantification_build_option_show_toplevel_quantifiers + && not (Foldable.null quants) + then build_declaration $ (freshsub `substitute`) . Monotype_Var <$> quants + else "") <> + build + ( opts + { quantification_build_option_consts_used = consts_used + , quantification_build_option_show_toplevel_quantifiers = True + } + , freshsub `substitute` quantified + ) + where + build_declaration quants = + build (Proxy::Proxy qt) <> " " <> + mconcat (List.intersperse " " $ build <$> quants) <> ". " + +-- ** Type 'Unquantification' + +data Unquantification a + = Unquantification + { unquantification_freshvar :: Freshvar + -- ^ The given 'Freshvar' + -- usable for the next fresh 'Monovar' (or 'Rigvar'), + -- incremented by one for each fresh 'Monovar' (or 'Rigvar's) + -- as needed by 'unquantify'. + , unquantified :: a + -- ^ The given 'quantified' value with the 'quantifiers' + -- replaced by fresh 'Monovar's (or 'Rigvar's). + } + +-- | Type synonym to signify that a 'Monovar' is used as a counter. +type Freshvar = Monovar + +-- | Perform a /type variable unabstraction/ (aka. /type variable instantiation/). +-- +-- Return the 'quantified' value of the given 'Quantification' +-- with its 'quantifiers' 'substitute'd +-- by 'Monovar's counting from given 'Monovar' +-- and applied to given 'Monotype' injection, +-- along with the 'Freshvar' incremented as needed. +unquantify + :: Substitutable a + => (Freshvar -> Monotype) + -> Freshvar + -> Quantification qt a + -> Unquantification a +unquantify monoty freshvar + Quantification{quantifiers, quantified} = + Unquantification + { unquantification_freshvar = freshvar + List.length quantifiers + , unquantified = sub `substitute` quantified + } + where + sub = substitution_finite $ + List.zip quantifiers (monoty <$> [freshvar..]) + +-- ** Type 'Universal' + +data Universal +type Forall = Quantification Universal + +instance Show (Proxy Universal) where + show _ = "Universal" +instance Buildable (Proxy Universal) where + build _ = "forall" + +-- | /Generalize/ a 'Monotype' to a 'Polytype', +-- 'quantify'ing all its 'subvars'. +for_all :: Substitutable a => a -> Forall a +for_all a = quantify (subvars a) a + +-- | /Generalize/ a 'Monotype' to a 'Polytype', +-- 'quantify'ing its 'subvars' which are within given 'Monovar's. +forall_in :: Substitutable a => [Monovar] -> a -> Forall a +forall_in quants a = quantify (quants `List.intersect` subvars a) a + +-- | /Generalize/ a 'Monotype' to a 'Polytype' +-- 'quantify'ing all its 'subvars' +-- except those within given 'Monovar's. +forall_but + :: Substitutable a + => [Monovar] -> a -> Forall a +forall_but vars_mono a = forall_in (subvars a List.\\ vars_mono) a + +-- | 'unquantify' a 'Forall' with fresh 'Monovar's. +unquantify_forall + :: Substitutable a + => Freshvar -> Forall a + -> Unquantification a +unquantify_forall = unquantify Monotype_Var + +-- ** Type 'Existential' + +data Existential +type Exists = Quantification Existential + +instance Show (Proxy Existential) where + show _ = "Existential" +instance Buildable (Proxy Existential) where + build _ = "exists" + +exists :: Rigvarifiable a => a -> Exists a +exists a = quantify_rigvars (rigidvars a) a + +unquantify_exists + :: Substitutable a + => Rigvar -> Exists a + -> Unquantification a +unquantify_exists = unquantify (Monotype_Const . monoconst_from_rigvar) + +reveal + :: Substitutable a + => Freshvar -> Exists a + -> Unquantification a +reveal = unquantify Monotype_Var + +unreveal :: Substitutable a => [Monovar] -> a -> Exists a +unreveal vars a = quantify (vars `List.intersect` subvars a) a + +-- * Type 'Rigvar' + +-- | A /rigid type variable/ (aka. /skolem constant/, named after Thoralf Skolem) +-- is a 'Monovar' bound by a 'Quantification' +-- outside the current /typing context/ +-- (therefore a 'Rigvar' cannot be unified with an other 'Monovar'). +-- +-- Intuitionally, a 'Rigvar' represents a /fixed unknown 'Monotype'/. +type Rigvar = Monovar + +-- | 'Monotype' which must remain monomorphic, +-- used to form the current /typing context/. +type Rigtype = Monotype + +-- | A /rigvarification/ is a special form of 'unquantify'cation +-- in which the 'quantifiers' are replaced by fresh 'Rigvar's: +-- these are 'Monoconst's that do not appear elsewhere. +-- +-- NOTE: 'rigconstify'ing a 'Forall' 'Quantification' +-- is an implementation technique +-- used to ensure that no assumption can be made +-- about certain 'Monovar's. +rigconstify + :: Substitutable a + => Freshvar -> Forall a + -> Unquantification a +rigconstify = unquantify (Monotype_Const . monoconst_from_rigvar) + +unrigconstify :: Rigvarifiable a => a -> Forall a +unrigconstify a = quantify_rigvars (rigidvars a) a + +-- | A prefix to single out 'Rigvar's from other 'Monoconst's. +rigvar_prefix :: Text +rigvar_prefix = "_" + +monoconst_from_rigvar :: Rigvar -> Monoconst +monoconst_from_rigvar = (rigvar_prefix <>) . Text.pack . show + +rigvar_from_monoconst :: Monoconst -> Maybe Rigvar +rigvar_from_monoconst c + | rigvar_prefix `Text.isPrefixOf` c = + Just $ read $ Text.unpack $ + Text.drop (Text.length rigvar_prefix) c + | otherwise = Nothing + +-- | Return the given 'Substitutable' value +-- with its 'subvars' mapped to 'Monotype_Const'. +constify_subvars :: Substitutable a => a -> a +constify_subvars a = sub `substitute` a + where + sub = + substitution_finite + [ (v, Monotype_Const $ monoconst_from_rigvar v) + | v <- subvars a + ] + +-- ** Type 'Rigvar_Substitution' + +type Rigvar_Substitution = [(Rigvar, Monotype)] + +-- ** Class 'Rigvarifiable' + +-- | Like 'Substitutable', but acting on 'Rigvar's. +class Rigvarifiable a where + rigidvars :: a -> [Rigvar] + rigidvars_substitute :: Rigvar_Substitution -> a -> a + +instance Rigvarifiable Monotype where + rigidvars monoty = + case monoty of + Monotype_Var _ -> [] + Monotype_Const c -> maybeToList $ rigvar_from_monoconst c + Monotype_App l r -> rigidvars l `List.union` rigidvars r + + rigidvars_substitute rsub monoty = + case monoty of + Monotype_Var _ -> monoty + Monotype_Const c -> + fromMaybe monoty $ do + rig <- rigvar_from_monoconst c + rig `List.lookup` rsub + Monotype_App l r -> + Monotype_App + (rsub `rigidvars_substitute` l) + (rsub `rigidvars_substitute` r) +instance Rigvarifiable a => Rigvarifiable [a] where + rigidvars = List.foldr (List.union . rigidvars) [] + rigidvars_substitute rsub = ((rsub `rigidvars_substitute`) <$>) diff --git a/Language/LOL/Typing/Type/Substitution.hs b/Language/LOL/Typing/Type/Substitution.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Type/Substitution.hs @@ -0,0 +1,203 @@ +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +module Language.LOL.Typing.Type.Substitution where + +import Data.Bool +import Data.Either (Either(..), either) +import Data.Eq (Eq(..)) +import Data.Function (($), (.)) +import Data.Functor ((<$>)) +import qualified Data.List as List +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Maybe (Maybe(..), fromMaybe, maybe) +import Data.Monoid (Monoid(..), (<>)) +import Data.Sequence (Seq) +import qualified Data.Set as Set +import Data.Text.Buildable (Buildable(..)) +import Prelude (Num(..), error) +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type.Monotype +import Language.LOL.Typing.Lib.Data.Empty (Empty(..)) + +-- * Class 'Substitution' + +-- | A /monomorphic type substitution/. +-- +-- TODO: maybe rename to Monosub? +class Substitution s where + substitution_codomain :: s -> [Monotype] + substitution_domain :: s -> [Monovar] + substitution_domain_remove :: [Monovar] -> s -> s + substitution_domain_restrict :: [Monovar] -> s -> s + substitution_lookup :: Monovar -> s -> Maybe Monotype + +-- ** Type 'Substitution_Finite' + +-- | A 'Substitution' represented by a finite map. +type Substitution_Finite = Map Monovar Monotype + +instance Empty Substitution_Finite where + empty = mempty +instance Buildable Substitution_Finite where + build = + mconcat . List.intersperse "\n" . + Map.foldrWithKey (\var ty -> + ((build (Monotype_Var var) <> " == " <> build ty) :) + ) [] +instance Substitution Substitution_Finite where + substitution_codomain = Map.elems + substitution_domain = Map.keys + substitution_domain_remove vars s = + List.foldr Map.delete s vars + substitution_domain_restrict vars = + Map.filterWithKey (\v _ -> Set.member v vars_kept) + where vars_kept = Set.fromList vars + substitution_lookup = Map.lookup + +substitution_finite_singleton :: Monovar -> Monotype -> Substitution_Finite +substitution_finite_singleton = Map.singleton + +substitution_finite :: [(Monovar, Monotype)] -> Substitution_Finite +substitution_finite = Map.fromList + +-- | Safely unify two 'Substitution_Finite's. +-- +-- NOTE: the union is left-biased: +-- it prefers the first 'Substitution_Finite' +-- when duplicate keys are encountered. +substitution_finite_union :: Substitution_Finite -> Substitution_Finite -> Substitution_Finite +substitution_finite_union x y = x `Map.union` ((x `substitute`) <$> y) + +-- | Unsafely unify two 'Substitution_Finite's. +substitution_finite_union_unsafe :: Substitution_Finite -> Substitution_Finite -> Substitution_Finite +substitution_finite_union_unsafe = Map.union + +-- ** Type 'Substitution_Fixpoint' + +-- | A fixpoint is computed when looking up +-- the target of a 'Monovar' in this 'Substitution'. +-- 'mappend'ing two 'Substitution's is cheap, +-- whereas a 'substitution_lookup' is more expensive +-- than with 'Substitution_Finite'. +newtype Substitution_Fixpoint + = Substitution_Fixpoint (Map Monovar Monotype) + deriving (Show) + +instance Empty Substitution_Fixpoint where + empty = Substitution_Fixpoint Map.empty +instance Buildable Substitution_Fixpoint where + build (Substitution_Fixpoint sub) = build sub +-- | WARNING: only disjoint 'Substitution_Fixpoint's can be 'mappend'ed. +instance Monoid Substitution_Fixpoint where + mempty = empty + mappend = substitution_fixpoint_union +instance Substitution Substitution_Fixpoint where + substitution_codomain (Substitution_Fixpoint s) = Map.elems s + substitution_domain (Substitution_Fixpoint s) = Map.keys s + substitution_domain_remove vars (Substitution_Fixpoint s) = + Substitution_Fixpoint $ + Map.filterWithKey (\v _ -> v `List.notElem` vars) s + substitution_domain_restrict vars (Substitution_Fixpoint s) = + Substitution_Fixpoint $ + Map.filterWithKey (\v _ -> Set.member v vars_kept) s + where vars_kept = Set.fromList vars + -- Map.filterWithKey (\v _ -> v `List.notElem` vars_removed) s + -- where vars_removed = Map.keys s List.\\ vars + substitution_lookup v sub@(Substitution_Fixpoint s) = + case Map.lookup v s of + Nothing -> Nothing + Just ty | ty == Monotype_Var v -> Nothing + | otherwise -> Just $ sub `substitute` ty + +substitution_fixpoint :: [(Monovar, Monotype)] -> Substitution_Fixpoint +substitution_fixpoint = Substitution_Fixpoint . Map.fromList + +-- | WARNING: only valid with disjoint 'Substitution_Fixpoint's +substitution_fixpoint_union + :: Substitution_Fixpoint + -> Substitution_Fixpoint + -> Substitution_Fixpoint +substitution_fixpoint_union + (Substitution_Fixpoint x) + (Substitution_Fixpoint y) = + Substitution_Fixpoint $ + Map.unionWith err x y + where err = error "substitution_fixpoint_union: the two substitutions are not disjoint" + +-- ** Type 'Substitution_Instance' + +data Substitution_Instance + = forall s. Substitution s + => Substitution_Instance + { substitution_instance_substitution :: s + , substitution_instance_codomain :: s -> [Monotype] + , substitution_instance_domain :: s -> [Monovar] + , substitution_instance_remove :: [Monovar] -> s -> s + , substitution_instance_restrict :: [Monovar] -> s -> s + , substitution_instance_lookup :: Monovar -> s -> Maybe Monotype + } + +substitution_instance :: Substitution s => s -> Substitution_Instance +substitution_instance s = + Substitution_Instance s + substitution_codomain + substitution_domain + substitution_domain_remove + substitution_domain_restrict + substitution_lookup + +instance Substitution Substitution_Instance where + substitution_codomain (Substitution_Instance s f _ _ _ _) = f s + substitution_domain (Substitution_Instance s _ f _ _ _) = f s + substitution_domain_remove vs (Substitution_Instance s _ _ f _ _) = substitution_instance (f vs s) + substitution_domain_restrict vs (Substitution_Instance s _ _ _ f _) = substitution_instance (f vs s) + substitution_lookup v (Substitution_Instance s _ _ _ _ f) = f v s + +-- * Class 'Substitutable' + +class Substitutable a where + -- | /substitutable type variables/ (aka. /free type variables/). + subvars :: a -> [Monovar] + -- | /idempotent substitution application/. + substitute :: Substitution s => s -> a -> a + +instance Substitutable Monotype where + subvars ty = + case ty of + Monotype_Var v -> [v] + Monotype_Const _ -> [] + Monotype_App t1 t2 -> subvars t1 `List.union` subvars t2 + sub `substitute` ty = + case ty of + Monotype_Var v -> fromMaybe (Monotype_Var v) $ substitution_lookup v sub + Monotype_Const _ -> ty + Monotype_App t1 t2 -> Monotype_App (sub `substitute` t1) (sub `substitute` t2) +instance Substitutable a => Substitutable [a] where + subvars = List.foldr (List.union . subvars) [] + substitute sub = ((sub `substitute`) <$>) +instance Substitutable a => Substitutable (Seq a) where + subvars = List.foldr (List.union . subvars) mempty + substitute sub = ((sub `substitute`) <$>) +instance Substitutable a => Substitutable (Maybe a) where + subvars = maybe [] subvars + sub `substitute` m = (sub `substitute`) <$> m +instance (Substitutable a, Substitutable b) => Substitutable (Either a b) where + subvars = either subvars subvars + sub `substitute` e = either (Left . (sub `substitute`)) (Right . (sub `substitute`)) e + +-- | Return the next 'Monovar' +-- that is not in the 'subvars' +-- of the given 'Substitutable' value. +-- +-- NOTE: return @0@ when 'subvars' is empty +subvar_next :: Substitutable a => a -> Monovar +subvar_next a = + case subvars a of + [] -> 0 + vs -> 1 + List.maximum vs diff --git a/Language/LOL/Typing/Type/Synotype.hs b/Language/LOL/Typing/Type/Synotype.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Type/Synotype.hs @@ -0,0 +1,238 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +module Language.LOL.Typing.Type.Synotype where + +import Control.Monad (forM) +import Data.Bool +import Data.Eq (Eq(..)) +import qualified Data.Foldable as Foldable +import Data.Function (($), (.), id) +import Data.Functor ((<$>)) +import qualified Data.Graph as Graph (scc, buildG) +import Data.Int (Int) +import qualified Data.List as List +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Maybe (Maybe(..), fromMaybe, maybe) +import Data.Monoid (Monoid(..), (<>)) +import Data.Ord (Ord(..)) +import qualified Data.Text as Text +import Data.Text.Buildable (Buildable(..)) +import qualified Data.Tree as Tree (flatten) +import Data.Tuple (uncurry) +import Prelude (Num(..), error) +import Text.Show (Show(..), showChar, showParen, showString) + +import Language.LOL.Typing.Type.Monotype +import Language.LOL.Typing.Type.Substitution +import Language.LOL.Typing.Lib.Data.Empty (Empty(..)) + +-- * Type 'Synotype' + +-- | An (unordered) collection of /type synonyms/. +data Synotype + = Synotype + { synotype_arity :: Arity + , synotype_monotype :: [Monotype] -> Monotype + } +type Synotypes + = Map Synoname Synotype + +type Synoname = Monoconst + +-- | An ordering of 'Synotypes'. +type Synotype_Ordering + = Map Synoname Synotype_Position + +-- | A position in a 'Synotype_Ordering'. +type Synotype_Position = Int + +-- | 'Synotypes' with a 'Synotype_Ordering'. +data Synotype_Substitution + = Synotype_Substitution + { synotypes_ordering :: Synotype_Ordering + , synotypes :: Synotypes + } +instance Show Synotype_Substitution where + showsPrec d Synotype_Substitution{synotypes_ordering} = + showParen (d > 10) $ + showString "Synotype_Substitution" . + showChar ' ' . + showChar '[' . + showString + (mconcat $ List.intersperse ", " $ + Text.unpack <$> Map.keys synotypes_ordering) . + showChar ']' +instance Buildable Synotype_Substitution where + build Synotype_Substitution{synotypes_ordering} = + "[" <> + mconcat ( + List.intersperse ", " $ + build <$> Map.keys + synotypes_ordering) <> + "]" + +instance Empty Synotype_Substitution where + empty = Synotype_Substitution + { synotypes_ordering = mempty + , synotypes = mempty + } + +-- | A 'type_String' is a 'type_List' of 'type_Char's +synotype_String :: Synotype_Substitution +synotype_String = + Synotype_Substitution + (Map.singleton "String" 0) + (Map.singleton "String" $ Synotype 0 $ \_ -> type_List type_Char) + +-- | Return the 'Synotype_Ordering' of given 'Synotypes' +-- along with the mutually recursive 'Synotypes' that are detected. +synorder + :: Synotypes + -> (Synotype_Ordering, [[Synoname]]) +synorder sys = + let keys = Map.keys sys in + let names = Map.fromList $ List.zip keys [0..] in + let positions = Map.fromList $ List.zip [0..] keys in + + let err = error "synorder: error in lookup table" in + let name_lookup n = fromMaybe err (Map.lookup n names) in + let pos_lookup p = fromMaybe err (Map.lookup p positions) in + + let edges = Map.foldrWithKey go [] sys + where + go s1 (Synotype ari monoty) es = + Map.foldrWithKey add es $ + monoconsts $ monoty (Monotype_Var <$> [0 .. ari - 1]) + where + add s2 _ = + case Map.lookup s2 names of + Just i2 -> (:) (i2, i1) + Nothing -> id + where + i1 = name_lookup s1 + in + + let graph = Graph.buildG (0, Map.size sys - 1) edges in + let list = Tree.flatten <$> Graph.scc graph in + + let (ordering, recursive, _) = + List.foldr go (Map.empty, [], 0) list + where + go ps (os, rs, counter) = + case ps of + [p] | (p, p) `List.notElem` edges -> -- NOTE: correct type synotype + ( Map.insert (pos_lookup p) counter os + , rs + , counter + 1 + ) + _ -> + ( os + , (pos_lookup <$> ps) : rs + , counter + ) + in + (ordering, recursive) + +-- | Return whether given 'Synoname' +-- +is_panthom_synotype :: Synotype_Substitution -> Synoname -> Bool +is_panthom_synotype Synotype_Substitution{synotypes} name = + case Map.lookup name synotypes of + Nothing -> False + Just (Synotype ari monoty) -> + let args = List.take ari [0..] in + let subvars_ty = subvars $ monoty (Monotype_Var <$> args) in + Foldable.any (`List.notElem` subvars_ty) args + +-- | Fully expand a type in a recursive way. +synexpand :: Synotypes -> Monotype -> Monotype +synexpand sys ty = + top_expanded `monoapp` (synexpand sys <$> tail) + where top_expanded `App_Spine` tail = + app_spine_left $ synexpand_tops sys ty + +-- | Fully expand the top-level 'Monotype_Const's. +synexpand_tops :: Synotypes -> Monotype -> Monotype +synexpand_tops sys ty = + maybe ty (synexpand_tops sys) $ + synexpand_top_step sys ty + +{- +-- | Fully expand the top-level 'Monotype_Const'. +synexpand_top :: Synotype_Substitution -> Monotype -> Maybe Monotype +synexpand_top Synotype_Substitution{synotypes} = + (synexpand_tops synotypes <$>) . + synexpand_top_step synotypes +-} + +-- | Try to expand the top-level 'Monotype_Const' one step. +synexpand_top_step :: Synotypes -> Monotype -> Maybe Monotype +synexpand_top_step sys ty = + case app_spine_left ty of + Monotype_Const c `App_Spine` args -> + case Map.lookup c sys of + Just (Synotype ari monoty) + | ari == List.length args -> Just (monoty args) + | otherwise -> err "synotype arity mismatch" + Nothing -> Nothing + _ -> Nothing + where + err s = error $ "synexpand_top_step: " <> s + +-- | Try to expand the top-level 'Monotype_Const' +-- of one of the two paired 'Monotype's. +-- +-- If both top-level 'Monotype_Const' can be expanded one step, +-- then the 'Synotype' which appears first +-- in the 'Synotype_Ordering' is expanded. +synexpand_top_step_ordered + :: Synotype_Substitution + -> (Monotype, Monotype) + -> Maybe (Monotype, Monotype) +synexpand_top_step_ordered + Synotype_Substitution{synotypes_ordering, synotypes} + (ty1, ty2) = + case (position ty1, position ty2) of + (Just p1, Just p2) | p1 <= p2 -> Just (expand_top_step ty1, ty2) + | otherwise -> Just (ty1, expand_top_step ty2) + (Just _ , Nothing) -> Just (expand_top_step ty1, ty2) + (Nothing, Just _ ) -> Just (ty1, expand_top_step ty2) + _ -> Nothing + where + position ty = + case app_spine_left ty of + Monotype_Const c `App_Spine` _ -> Map.lookup c synotypes_ordering + _ -> Nothing + expand_top_step ty = + fromMaybe + (error "synexpand_top_step_ordered: Synotype_Substitution is invalid") + (synexpand_top_step synotypes ty) + +-- | Return the /most general type/ +-- (i.e. with the least number of expansions). +-- of two 'Monotype's which must be equal +-- under given 'Synotype_Substitution'. +mgt_with_synotypes + :: Synotype_Substitution + -> Monotype -> Monotype + -> Maybe Monotype +mgt_with_synotypes syns t1 t2 = + case (app_spine_left t1, app_spine_left t2) of + ( Monotype_Var v `App_Spine` [] + , Monotype_Var _ `App_Spine` [] ) + -> Just $ Monotype_Var v + ( Monotype_Const c1 `App_Spine` tail1 + , Monotype_Const c2 `App_Spine` tail2 ) + | c1 == c2 && not (is_panthom_synotype syns c1) + -> do + mgts <- + forM (List.zip tail1 tail2) $ uncurry $ + mgt_with_synotypes syns + Just (Monotype_Const c1 `monoapp` mgts) + | otherwise -> do + (t1', t2') <- synexpand_top_step_ordered syns (t1, t2) + mgt_with_synotypes syns t1' t2' + _ -> Nothing diff --git a/Language/LOL/Typing/Type/Test.hs b/Language/LOL/Typing/Type/Test.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Type/Test.hs @@ -0,0 +1,38 @@ +{-# LANGUAGE OverloadedStrings #-} +module Type.Test where + +import Data.Function (($)) +import Data.Text.Buildable (Buildable(..)) +import Test.Tasty +import Test.Tasty.HUnit +-- import Test.HUnit hiding (test) + +import Language.LOL.Typing.Type +import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build + +tests :: TestTree +tests = testGroup "Type" + [ tests_Monotype + ] + +tests_Monotype :: TestTree +tests_Monotype = testGroup "Monotype" + [ testGroup "Build" $ + let (==>) x expected = testCase (Build.string expected) $ build x @?= expected in + [ ("a"::Monotype) ==> "a" + , ("a".->."b") ==> "a -> b" + , ("a".->."b".->."c") ==> "a -> b -> c" + , ("a".->."b".->."c".->."d") ==> "a -> b -> c -> d" + , ("a".->."b".->.("c".->."d")) ==> "a -> b -> c -> d" + , (("a".->."b").->."c".->."d") ==> "(a -> b) -> c -> d" + , (("a".->."b").->.("c".->."d")) ==> "(a -> b) -> c -> d" + , ("a".->.("b".->."c").->."d") ==> "a -> (b -> c) -> d" + , ((("a".->."b").->.("c".->."d")).->.(("e".->."f").->.("g".->."h"))) + ==> "((a -> b) -> c -> d) -> (e -> f) -> g -> h" + , ("T".!."a".!."b") ==> "T a b" + , ("T".!."a".!."b".!.("U".!."c".!."d")) ==> "T a b (U c d)" + , ("T".!."a".!."b".->."U".!."c".!."d") ==> "T a b -> U c d" + , ("T".!."a".!."b".->."U".!."c".!."d".->."V".!."e".!."f") ==> "T a b -> U c d -> V e f" + , ("T".!."x".!.(("a".->."b").->.("c".->."d")).!."y") ==> "T x ((a -> b) -> c -> d) y" + ] + ] diff --git a/Language/LOL/Typing/Type/Unification.hs b/Language/LOL/Typing/Type/Unification.hs new file mode 100644 --- /dev/null +++ b/Language/LOL/Typing/Type/Unification.hs @@ -0,0 +1,127 @@ +{-# LANGUAGE NamedFieldPuns #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} +module Language.LOL.Typing.Type.Unification where + +import Data.Bool +import Data.Either (Either(..)) +import Data.Eq (Eq(..)) +import Data.Function (($)) +import Data.Functor ((<$>)) +import qualified Data.List as List +import qualified Data.Map as Map +import Data.Maybe (Maybe(..), fromMaybe) +import Data.Monoid (Monoid(..), (<>)) +import Data.Tuple (snd) +import Prelude (error) +import Text.Show (Show(..)) + +import Language.LOL.Typing.Type.Monotype +import Language.LOL.Typing.Type.Substitution +import Language.LOL.Typing.Type.Synotype +import Language.LOL.Typing.Lib.Data.Empty (Empty(..)) + +-- * Type 'Unification' + +type Unification + = Substitution_Finite + +-- | Like 'mgu_with_synotypes', but with an empty 'Synotype_Substitution'. +mgu :: Monotype -> Monotype -> Either Unification_Error Unification +mgu t1 t2 = snd <$> mgu_with_synotypes empty t1 t2 + +-- | The /most general unification/ ('Substitution') of two 'Monotype's, +-- expanding 'Synotypes' as lazy as possible. +-- +-- Example: +-- +-- @ +-- if String => [Char] +-- then v11 -> [v11] `mgu` String -> [[v14]] +-- should be: +-- [ v11 := [Char] , v14 := Char ] +-- @ +-- +-- NOTE: the boolean indicates whether expansions were necessary. +mgu_with_synotypes + :: Synotype_Substitution + -> Monotype -> Monotype + -> Either Unification_Error (Bool, Unification) +mgu_with_synotypes syns = go mempty + where + err s = error $ "mgu_with_synotypes: " <> s + go sub t1 t2 = + case (app_spine_left t1, app_spine_left t2) of + (App_Spine (Monotype_Var v) [], _) -> go_Var sub v t2 + (_, App_Spine (Monotype_Var v) []) -> go_Var sub v t1 + ( App_Spine (Monotype_Const c1) s1 + , App_Spine (Monotype_Const c2) s2 ) + | c1 == c2 && not (is_panthom_synotype syns c1) -> + go_List sub s1 s2 + | otherwise -> + case synexpand_top_step_ordered syns (t1, t2) of + Nothing -> Left $ Unification_Error_Constant_clash c1 c2 + Just (t1', t2') -> + case go sub t1' t2' of + Left e -> Left e + Right (_, sub') -> Right (True, sub') + _ -> case (t1, t2) of + (Monotype_App l1 r1, Monotype_App l2 r2) -> + go_List sub [l1, r1] [l2, r2] + _ -> err "illegal type" + go_Var sub v ty = + case Map.lookup v sub of + Just t2 -> + case go sub ty t2 of + Right (True, sub') -> + let mgt = + fromMaybe (err "illegal types") $ + mgt_with_synotypes syns + (sub' `substitute` ty) + (sub' `substitute` t2) in + Right + ( True + , substitution_finite_union + (substitution_finite_singleton v mgt) + (substitution_domain_remove [v] sub') + ) + e -> e + Nothing -> + case sub `substitute` ty of + Monotype_Var v' | v == v' -> Right (False, sub) + ty' | v `List.elem` subvars ty' -> Left (Unification_Error_Infinite_type v) + | otherwise -> Right (False, substitution_finite_singleton v ty' `substitution_finite_union` sub) + go_List sub [] [] = Right (False, sub) + go_List sub (s:ss) (t:tt) = + case go sub s t of + Left e -> Left e + Right (b,sub') -> + case go_List sub' ss tt of + Left e -> Left e + Right (b', sub'') -> Right (b || b', sub'') + go_List _ _ _ = err "kinds do not match" + +-- | Given a set of 'Synotype_Substitution', can two types be unified? +unifiable :: Synotype_Substitution -> Monotype -> Monotype -> Bool +unifiable syns t1 t2 = + case mgu_with_synotypes syns t1 t2 of + Left _ -> False + Right _ -> True + +-- | Same as unifiable, but takes as input a list of 'Monotype's +unifiables :: Synotype_Substitution -> [Monotype] -> Bool +unifiables syns (t1:t2:ts) = + case mgu_with_synotypes syns t1 t2 of + Left _ -> False + Right (_, sub) -> unifiables syns (sub `substitute` (t2:ts)) +unifiables _ _ = True + +-- ** Type 'Unification_Error' + +-- | Reasons why two 'Monotype's cannot be unified. +data Unification_Error + = Unification_Error_Constant_clash Monoconst Monoconst + -- ^ Two different 'Monoconst's clash (they should be the same). + | Unification_Error_Infinite_type Monovar + -- ^ A 'Monotype_Var' is unified with a composed 'Monotype' + -- which contains this same 'Monotype_Var'. + deriving (Eq, Show) diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,5 @@ +import Distribution.Simple (defaultMainWithHooks) +import Distribution.Simple.UUAGC (uuagcLibUserHook) +import UU.UUAGC (uuagc) + +main = defaultMainWithHooks (uuagcLibUserHook uuagc) diff --git a/lol-typing.cabal b/lol-typing.cabal new file mode 100644 --- /dev/null +++ b/lol-typing.cabal @@ -0,0 +1,204 @@ +author: Julien Moutinho +-- bug-reports: http://bug.autogeree.net/lol +build-type: Custom +cabal-version: >= 1.24 +category: Language +-- data-dir: . +-- data-files: +description: + WARNING: this is a research program + written as I learn and explore /type inferencing/: + please understand well by yourself whatever you may take from it; + any question or contribution being welcome :-) + . + This package implements /type inferencing/ + by manipulating /type constraints/ + through 3 successive phases: + 1. the 'Collect' phase collects them from some expression, + 2. the 'Order' phase modifies the order in which they will be solved, + 3. the 'Solver' phase solves them according to the logic + of some /type inference rules/. + . + So far, the principles within these phases + are mainly a rewrite of Bastiaan Heeren's + , + using my own code conventions and ideals of simplicity. + The most notable change being the use of Roman Cheplyaka's + + (a little bit augmented): + to handle the 'Monad' stack building a 'Solver' + (instead of a homegrown machinery I could not understand well). + At this point, only a /bottom-up/ 'Collect', a no-op 'Order' + and a 'Greedy' 'Solver' are implemented, supporting: + /monomorphic types/ ('Monotype'), + /parametric polymorphism/ ('Polytype'), + /type class polymorphism/ ('Class'), + and /type synonyms/ ('Synotype'). + The quite understandable thesis of Bastiaan Heeren + explains a lot of this in details: + . + . + The + is used to demonstrate how to collect /type constraints/ from an expression ('Expr'), + and then how to transform this /implicitely typed/ expression into an /explicitely typed/ + expression + . + See also: the compiler. +extra-source-files: + stack.yaml, + uuagc_options, + Language/LOL/Typing/Collect/Grammar.ag, + Language/LOL/Typing/Expr/Calculus.ag, + Language/LOL/Typing/Expr/Grammar.ag +extra-tmp-files: +homepage: http://pad.autogeree.net/informatique/lol/ +license: GPL-3 +license-file: COPYING +maintainer: Julien Moutinho +name: lol-typing +stability: experimental +synopsis: Type inferencer for LOL (λω language) +tested-with: GHC==7.10.3 +version: 1.20160822 + +source-repository head + location: git://git.autogeree.net/lol + type: git + +Flag dev + Default: False + Description: Turn on development settings. + Manual: True + +Flag dump + Default: False + Description: Dump some intermediate files. + Manual: True + +Flag exe + Default: False + Description: Turn on executables. + Manual: True + +Flag prof + Default: False + Description: Turn on profiling settings. + Manual: True + +Flag threaded + Default: True + Description: Enable threads. + Manual: True + +Custom-Setup + setup-depends: + base >= 4.6 && < 5 + , Cabal >= 1.24 + , uuagc >= 0.9 + , uuagc-cabal >= 1.0.6.0 + +Library + default-extensions: NoImplicitPrelude + default-language: Haskell2010 + ghc-options: -Wall -fno-warn-tabs + if flag(dev) + cpp-options: -DDEVELOPMENT + ghc-options: + if flag(dump) + ghc-options: -ddump-simpl -ddump-stg -ddump-to-file + if flag(prof) + cpp-options: -DPROFILING + ghc-options: -fprof-auto + exposed-modules: + Language.LOL.Typing + Language.LOL.Typing.Collect + Language.LOL.Typing.Collect.Constraint + Language.LOL.Typing.Collect.Grammar + Language.LOL.Typing.Constraint + Language.LOL.Typing.Constraint.Either + Language.LOL.Typing.Constraint.Extra + Language.LOL.Typing.Constraint.Monotype + Language.LOL.Typing.Constraint.Polytype + Language.LOL.Typing.Expr + Language.LOL.Typing.Expr.Calculus + Language.LOL.Typing.Expr.Common + Language.LOL.Typing.Expr.Grammar + Language.LOL.Typing.Expr.Utils + Language.LOL.Typing.Expr.Write + Language.LOL.Typing.Lib.Control.Monad.Classes.EffectsFix + Language.LOL.Typing.Lib.Control.Monad.Classes.Instance + Language.LOL.Typing.Lib.Control.Monad.Classes.StateFix + Language.LOL.Typing.Lib.Control.Monad.Classes.StateInstance + Language.LOL.Typing.Lib.Data.Default + Language.LOL.Typing.Lib.Data.Empty + Language.LOL.Typing.Lib.Data.Text.Buildable + Language.LOL.Typing.Solver + Language.LOL.Typing.Solver.Class + Language.LOL.Typing.Solver.Common + Language.LOL.Typing.Solver.Constraint + Language.LOL.Typing.Solver.Greedy + Language.LOL.Typing.Solver.Monad + Language.LOL.Typing.Solver.Monotype + Language.LOL.Typing.Solver.Polytype + Language.LOL.Typing.Type + Language.LOL.Typing.Type.Class + Language.LOL.Typing.Type.Kind + Language.LOL.Typing.Type.Monotype + Language.LOL.Typing.Type.Polytype + Language.LOL.Typing.Type.Qualification + Language.LOL.Typing.Type.Quantification + Language.LOL.Typing.Type.Substitution + Language.LOL.Typing.Type.Synotype + Language.LOL.Typing.Type.Unification + build-depends: + base >= 4.6 && < 5 + , containers >= 0.5 && < 0.6 + , ghc-prim + , lol-calculus + , monad-classes >= 0.3.1.1 + -- , monad-control + , parsec >= 3.1.2 && < 4 + -- , peano + -- , reflection + , text + , text-format + , transformers >= 0.4 && < 0.5 + -- , transformers-base + , uuagc >= 0.9 + , uuagc-cabal >= 1.0.6.0 + + +test-suite lol-typing-test + type: exitcode-stdio-1.0 + default-extensions: NoImplicitPrelude + default-language: Haskell2010 + ghc-options: -Wall -fno-warn-tabs + -main-is Test + hs-source-dirs: Language/LOL/Typing + main-is: Test.hs + other-modules: + Expr.Test + Solver.Test + Type.Test + if flag(threaded) + ghc-options: -threaded -rtsopts -with-rtsopts=-N + if flag(dev) + cpp-options: -DDEVELOPMENT + ghc-options: + if flag(prof) + cpp-options: -DPROFILING + ghc-options: -fprof-auto + build-depends: + base >= 4.6 && < 5 + , containers >= 0.5 && < 0.6 + , directory + , filepath + , ghc-prim + , lol-calculus + , lol-typing + , monad-classes >= 0.3.1.1 + , tasty >= 0.11 + , tasty-hunit + , text + , text-format + , transformers >= 0.4 && < 0.5 diff --git a/stack.yaml b/stack.yaml new file mode 100644 --- /dev/null +++ b/stack.yaml @@ -0,0 +1,15 @@ +flags: {} +extra-package-dbs: [] +packages: +- '.' +- ../calculus +extra-deps: +- Cabal-1.24.0.0 +- monad-classes-0.3.1.1 +- peano-0.1.0.1 +- uuagc-0.9.52.1 +- uuagc-cabal-1.0.6.0 +- uulib-0.9.22 +explicit-setup-deps: + '*': true +resolver: lts-6.12 diff --git a/uuagc_options b/uuagc_options new file mode 100644 --- /dev/null +++ b/uuagc_options @@ -0,0 +1,8 @@ +file : "Language/LOL/Typing/Expr/Grammar.ag" +options : data, haskellsyntax, rename + +file : "Language/LOL/Typing/Expr/Calculus.ag" +options : catas, haskellsyntax, pretty, rename, semfuns, signatures, wrappers + +file : "Language/LOL/Typing/Collect/Grammar.ag" +options : catas, haskellsyntax, pretty, rename, semfuns, signatures, wrappers