static (empty) → 0.1.0.0
raw patch · 13 files changed
+2321/−0 lines, 13 filesdep +basedep +binarydep +bytestringsetup-changed
Dependencies added: base, binary, bytestring, checkers, constraints, doctest, lens, mtl, serialise, singletons, static, tasty, tasty-hunit, tasty-quickcheck, template-haskell, text, transformers
Files
- CHANGELOG.md +5/−0
- LICENSE.GPL-3 +674/−0
- Setup.hs +2/−0
- src/Control/Static.hs +55/−0
- src/Control/Static/Closure.hs +297/−0
- src/Control/Static/Common.hs +300/−0
- src/Control/Static/Serialise.hs +164/−0
- src/Control/Static/Static.hs +167/−0
- src/Control/Static/TH.hs +227/−0
- static.cabal +185/−0
- test/Control/Static/UnitTests.hs +234/−0
- test/DocTests.hs +4/−0
- test/UnitTests.hs +7/−0
+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for static++## 0.1.0.0 -- 2020-05-17++* Initial release.
+ LICENSE.GPL-3 view
@@ -0,0 +1,674 @@+ GNU GENERAL PUBLIC LICENSE+ Version 3, 29 June 2007++ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>+ 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.++ <one line to give the program's name and a brief idea of what it does.>+ Copyright (C) <year> <name of author>++ 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 <http://www.gnu.org/licenses/>.++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:++ <program> Copyright (C) <year> <name of author>+ 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+<http://www.gnu.org/licenses/>.++ 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+<http://www.gnu.org/philosophy/why-not-lgpl.html>.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/Control/Static.hs view
@@ -0,0 +1,55 @@+module Control.Static+ (+ -- * Common definitions+ TCTab(..)+ -- * Static keys and values+ , SKey+ , SKeyed(..)+ , SKeyedExt(..)+ , withSKeyedExt+ , toSKeyedExt+ -- * Static tables and resolving values+ , gwithStatic+ , withStaticCts+ , withSomeStaticCts+ , withStaticCxt+ , withSomeStaticCxt+ -- * Static closures+ , PreClosure(..)+ , Closure(..)+ , PostClosure(..)+ , ClosureApply+ , applyClosure+ , envTabCons+ , envTabNil+ , mkClosureTab+ , RepClosure+ , RepClosure'+ , repClosureTab+ , withEvalClosureCts+ , withEvalSomeClosureCts+ , withEvalClosureCxt+ , withEvalSomeClosureCxt+ , evalClosure+ , evalSomeClosure+ -- * Serialisation+ , RepVal(..)+ , SKeyedError(..)+ , DoubleEncoding(..)+ , DSerialise+ , DBinary+ )+where++import Control.Static.Closure+import Control.Static.Common+import Control.Static.Serialise+import Control.Static.Static++-- Note, the implementation comments in these files make various references to+-- "singletons defunctionalisation symbols", see here for an approachable+-- explanation:+--+-- https://blog.jle.im/entry/introduction-to-singletons-4.html#defunctionalization+--+-- You may want to start from part 1, if you have trouble jumping in the middle.
+ src/Control/Static/Closure.hs view
@@ -0,0 +1,297 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++module Control.Static.Closure where++-- external+import Data.Constraint (Dict (..))+import Data.Functor (($>))+import Data.Kind (Constraint)+import Data.Singletons.Prelude+import Data.Singletons.TH (genDefunSymbols)++-- internal+import Control.Static.Common+import Control.Static.Serialise+import Control.Static.Static+++-- | Closure, internal representation.+--+-- The type parameter @env@ is meant for a bag of functions known statically at+-- compile time, that you don't need to serialise and so don't want the added+-- complexity of dealing with $(mkStatic). For example, if your function takes+-- in extra utility functions, but these are all statically-known. The type+-- parameter @cxt@ are the constraint types, which is effectively similar to+-- @env@ except that Haskell deals with them slightly differently.+type ClosureFunc cxt env arg res = CxtW cxt (env -> arg -> res)++-- | An applied closure, consisting of its static key and an argument.+type ClosureApply g = SKeyedExt g++-- | Create a 'ClosureApply' in its serialisable static form.+applyClosure+ :: RepVal g arg k+ => SKeyed k (CxtW cxt (env -> arg -> res))+ -> arg+ -> ClosureApply g+applyClosure (SKeyed k cl) arg = toSKeyedExt (SKeyed k arg)++envTabCons+ :: SKeyed k (CxtW cxt (env -> arg -> res))+ -> env+ -> TTab kk vv+ -> TTab (k ': kk) (env ': vv)+envTabCons cl env = skeyedCons (cl $> env)++envTabNil :: TTab '[] '[]+envTabNil = TCNil @NullC2Sym0++-- | A pre-closure is a function that takes two statically-known arguments:+-- a constraint, and an explicit argument; and gives a closure.+--+-- Typically, you define a bunch of top-level functions of the form @(ctx =>+-- env -> arg -> res)@, then create a table of pre-closures using the TH+-- function 'Control.Static.TH.mkStaticTab'.+class Closure (Part pcl) => PreClosure pcl where+ type Cxt pcl :: Constraint+ type Env pcl+ type Part pcl+ applyPre :: Cxt pcl => pcl -> Env pcl -> Part pcl++instance PreClosure (CxtW c (e -> v -> r)) where+ type Cxt (CxtW c (e -> v -> r)) = c+ type Env (CxtW c (e -> v -> r)) = e+ type Part (CxtW c (e -> v -> r)) = v -> r+ applyPre (CxtW pcl) = pcl++-- | A closure is a function that takes a runtime argument, and gives a result.+--+-- It is created by applying a constraint and environment to a pre-closure.+-- Typically you do this once on a table of pre-closures, using 'mkClosureTab'.+class Closure cl where+ type Arg cl+ type Res cl+ apply :: cl -> Arg cl -> Res cl++instance Closure (v -> r) where+ type Arg (v -> r) = v+ type Res (v -> r) = r+ apply = ($)++-- | A post-closure is a function that takes a runtime result, and converts all+-- the results of all different closures into the same type.+class PostClosure x f where+ type Pre f+ applyPost :: f -> Pre f -> x++instance PostClosure x (r -> x) where+ type Pre (r -> x) = r+ applyPost = ($)++genDefunSymbols [''Cxt, ''Env, ''Part, ''Arg, ''Res, ''Pre]+++-- | A continuation from the result type to @x@.+type ResCont x = TyContSym1 x .@#@$$$ ResSym0+++-- | Apply a table of pre-closures to its inputs, creating a table of closures.+applyClosureTabPre+ :: forall c1 kk vv+ . ConstrainList (Fmap CxtSym0 vv)+ => TCTab' PreClosure kk vv+ -> TCTab c1 kk (Fmap EnvSym0 vv)+ -> TCTab' Closure kk (Fmap PartSym0 vv)+applyClosureTabPre tab env =+ zipWith3TC @_ @_ @_ @_ @_ @(DictOf CxtSym0) @EnvSym0 @PartSym0 tab cxt env+ $ \_ cl _ Dict _ e -> (applyPre cl e, Dict)+ where cxt = toTCDict @_ @_ @CxtSym0 tab++-- | Apply a table of closures to its inputs, creating a table of results.+applyClosureTab+ :: forall c1 kk vv+ . TCTab' Closure kk vv+ -> TCTab c1 kk (Fmap ArgSym0 vv)+ -> TTab kk (Fmap ResSym0 vv)+applyClosureTab tab arg =+ zipWithTC @_ @_ @_ @_ @ArgSym0 @ResSym0 tab arg $ \_ cl _ a -> (apply cl a, Dict)++-- | Apply a table of results to its post-closures, creating a table of values.+applyClosureTabPost+ :: forall c0 kk rr x+ . TCTab c0 kk rr+ -> TCTab' (PostClosure x) kk (Fmap (TyContSym1 x) rr)+ -> TTab kk (Fmap (ConstSym1 x) rr)+applyClosureTabPost res post =+ zipWithTC @_ @_ @_ @_ @(TyContSym1 x) @(ConstSym1 x) res post+ $ \_ r _ p -> (applyPost p r, Dict)++-- | Apply a table of closures to a table of inputs and post-closures, giving a+-- table of values.+--+-- This method is just a demo, users will want one of the exported functions.+evalClosureTab+ :: forall (kk :: [Symbol]) vv x+ . TCTab' Closure kk vv+ -> TTab kk (Fmap ArgSym0 vv)+ -> TCTab' (PostClosure x) kk (Fmap (ResCont x) vv)+ -> TTab kk (Fmap (ConstSym1 x) vv)+evalClosureTab tab arg post =+ -- we could do this:+ -- let res = applyClosureTab tab arg+ -- in applyClosureTabPost @_ @kk @(Fmap ResSym0 vv) res post+ -- but it does not work as-is; we first have to:+ -- write proofs (no-op functions) to convert+ -- TCTab c kk (Fmap (f .@#@$$$ g) vv)+ -- into+ -- TCTab c kk (Fmap f (Fmap g vv))+ -- in order to call applyClosureTabPost,+ -- as well as proofs to convert+ -- TCTab c kk (Fmap (ConstSym1 x) (Fmap f vv))+ -- into+ -- TCTab c kk (Fmap (ConstSym1 x) vv)+ -- in order to return the result.+ --+ -- OTOH zipWith3TC inlines these proofs for us already, so we use that+ zipWith3TC @_ @_ @_ @_ @_ @ArgSym0 @(ResCont x) @(ConstSym1 x) tab arg post+ $ \_ cl _ a _ p -> (applyPost p (apply cl a), Dict)+++-- | Create a table of closures from a table of pre-closures.+--+-- We apply the relevant constraints and environment arguments,+-- statically-known at compile time.+mkClosureTab+ :: forall c1 kk vv+ . ConstrainList (Fmap CxtSym0 vv)+ => ConstrainList (ZipWith (ConstSym1 (TyCon1 PreClosure)) kk vv)+ => TTab kk vv+ -> TCTab c1 kk (Fmap EnvSym0 vv)+ -> TCTab' Closure kk (Fmap PartSym0 vv)+mkClosureTab = applyClosureTabPre . strengthenTC0++-- | @RepClosure c g k v@ is a constraint comprising:+--+-- * @RepVal g (Arg v) k@+-- * @c k (Res v)@+-- * @Closure v@+--+-- modulo singletons defunctionalisation on @c@.+type RepClosure c g+ = RepExtSym3+ (AndC2 (ConstSym1 (TyCon1 Closure)) (FlipSym2 (.@#@$) ResSym0 .@#@$$$ c))+ g+ ArgSym0++-- | A 'RepClosure' whose result is exactly @r@.+type RepClosure' r g = RepClosure (ConstSym1 (TyCon1 ((~) r))) g++-- | Convert a 'Closure' table into a 'RepClosure' table, deducing constraints.+--+-- This is used to convert the result of 'mkClosureTab' into a form that can be+-- passed to the other functions e.g. 'evalSomeClosure'.+repClosureTab+ :: forall c g (kk :: [Symbol]) vv+ . ConstrainList (ZipWith (FlipSym2 (.@#@$) ResSym0 .@#@$$$ c) kk vv)+ => ConstrainList+ (ZipWith (FlipSym1 (TyCon2 (RepVal g) .@#@$$$ ApplySym1 ArgSym0)) kk vv)+ => TCTab' Closure kk vv+ -> TCTab (RepClosure c g) kk vv+repClosureTab = strengthenTC . strengthenTC++-- | Apply a closure table to a single input and a post-processing table,+-- giving a single result (if the input key was found).+--+-- This is the statically-typed version; for a version that runs for unknown+-- keys see 'withEvalSomeClosureCts'.+withEvalClosureCts+ :: forall c g (k :: Symbol) (kk :: [Symbol]) vv x+ . TCTab (RepClosure c g) kk vv+ -> SKeyed k g+ -> TCTab' (PostClosure x) kk (Fmap (ResCont x) vv)+ -> Either SKeyedError x+withEvalClosureCts tab val post = gwithStatic @_ @_ @(ResCont x) tab val post+ $ \_ cont cl -> applyPost cont . apply cl++-- | Apply a closure table to a single input and a post-processing table,+-- giving a single result (if the input key was found).+--+-- This is the dynamically-typed version; for a version that type-checks for+-- statically-known keys see 'withEvalClosureCts'.+withEvalSomeClosureCts+ :: forall c g (kk :: [Symbol]) vv x+ . TCTab (RepClosure c g) kk vv+ -> ClosureApply g+ -> TCTab' (PostClosure x) kk (Fmap (ResCont x) vv)+ -> Either SKeyedError x+withEvalSomeClosureCts tab ext post =+ withSKeyedExt ext $ \val -> withEvalClosureCts tab val post++-- | Apply a closure table to a single input, and pass the constrained result+-- to a continuation (if the input key was found).+--+-- This is the statically-typed version; for a version that runs for unknown+-- keys see 'withEvalSomeClosureCxt'.+withEvalClosureCxt+ :: forall c f g (k :: Symbol) (kk :: [Symbol]) vv r+ . TCTab (RepClosure c g) kk vv+ -> SKeyed k g+ -> ( forall k' v+ . 'Just '(k', v) ~ LookupKV k kk vv+ => ProofLookupKV f k kk vv+ => (c @@ k' @@ Res v) => Sing k' -> Res v -> r+ )+ -> Either SKeyedError r+withEvalClosureCxt tab val go =+ withStaticCxt @_ @f tab val $ \k' cl a -> go k' (apply cl a)++-- | Apply a closure table to a single input, and pass the constrained result+-- to a continuation (if the input key was found).+--+-- This is the dynamically-typed version; for a version that type-checks for+-- statically-known keys see 'withEvalClosureCxt'.+withEvalSomeClosureCxt+ :: forall c f g (kk :: [Symbol]) vv r+ . TCTab (RepClosure c g) kk vv+ -> ClosureApply g+ -> ( forall k k' v+ . 'Just '(k', v) ~ LookupKV k kk vv+ => ProofLookupKV f k kk vv+ -- keep above constraints; caller can either use or ignore as they wish+ -- without them, caller is prevented from using them at all+ => (c @@ k' @@ Res v) => Sing k' -> Res v -> r+ )+ -> Either SKeyedError r+withEvalSomeClosureCxt tab ext go = withSKeyedExt ext+ $ \(val :: SKeyed k g) -> withEvalClosureCxt @_ @f tab val (go @k)++-- | Evaluate a closure application with statically-known type, against a table+-- of closures, that all have the same result type.+evalClosure+ :: forall g (k :: Symbol) (kk :: [Symbol]) vv r+ . TCTab (RepClosure' r g) kk vv+ -> SKeyed k g+ -> Either SKeyedError r+evalClosure tab val = withEvalClosureCxt tab val $ const id++-- | Evaluate a closure application with statically-unknown type, against a+-- table of closures, that all have the same result type.+evalSomeClosure+ :: forall g (kk :: [Symbol]) vv r+ . TCTab (RepClosure' r g) kk vv+ -> ClosureApply g+ -> Either SKeyedError r+evalSomeClosure tab ext = withSKeyedExt ext $ evalClosure tab
+ src/Control/Static/Common.hs view
@@ -0,0 +1,300 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++module Control.Static.Common where++-- external+import Data.Constraint ((:-) (..), Class (..), Dict (..))+import Data.Kind (Constraint, Type)+import Data.Singletons.Prelude+import Data.Singletons.TH (genDefunSymbols, singletons)+++-- | Type family representing the type of a continuation.+type family TyCont r (a :: Type) where+ TyCont r a = a -> r+genDefunSymbols [''TyCont]++-- | Type family representing the type of a continuation of 2 args.+type family TyCont2 r (a1 :: Type) (a2 :: Type) where+ TyCont2 r a1 a2 = a1 -> a2 -> r+genDefunSymbols [''TyCont2]++-- | Type family representing the type of a continuation of 3 args.+type family TyCont3 r (a1 :: Type) (a2 :: Type) (a3 :: Type) where+ TyCont3 r a1 a2 a3 = a1 -> a2 -> a3 -> r+genDefunSymbols [''TyCont3]++singletons [d|+ -- -| S combinator, not yet in singletons+ -- https://github.com/goldfirere/singletons/issues/455+ ap :: (x -> y -> z) -> (x -> y) -> (x -> z)+ ap f g x = f x (g x)+ |]+++-- | Data type wrapping a constraint, to avoid ImpredicativeTypes GHC error.+newtype CxtW c a = CxtW { unCxtW :: c => a }++-- | Convert a list of constraints into a single constraint+type family ConstrainList (cc :: [Constraint]) :: Constraint where+ ConstrainList '[] = ()+ ConstrainList (c ': cc) = (c, ConstrainList cc)++-- | Null constraint over 1 type param.+type family NullC (t :: k) :: Constraint where+ NullC t = ()+genDefunSymbols [''NullC]++-- | Null constraint over 2 type params.+type family NullC2 (t :: k) (t' :: k') :: Constraint where+ NullC2 t t' = ()+genDefunSymbols [''NullC2]++-- | Combine two constraints+type family AndC c0 c1 :: Constraint where+ AndC c0 c1 = (c0, c1)+genDefunSymbols [''AndC]++-- | Combine two constraint constructors into a single constraint constructor.+--+-- This is analogous to the term-level idiom @ap ((,) . c0) c1@ that combines+-- two functions c0, c1 into a single one.+type AndC1 c0 c1 = ApSym2 (AndCSym0 .@#@$$$ c0) c1++-- | Combine two constraint constructors, each taking 2 type params, into+-- a single constraint constructor taking 2 type params.+--+-- This is analogous to the term-level idiom @ap (ap . ((,) .) . c0) c1@ that+-- combines two functions c0, c1 that each take 2 params, into a single one.+type AndC2 c0 c1 = ApSym2 (ApSym0 .@#@$$$ (.@#@$$) AndCSym0 .@#@$$$ c0) c1++-- | Entailment over 2 type params.+type family Class2 c0 c1 t t' where+ Class2 c0 c1 t t' = Class (c0 @@ t @@ t') (c1 @@ t @@ t')+genDefunSymbols [''Class2]+++singletons [d|+ -- note: subexpressions are lifted out to the top-level due to+ -- https://github.com/goldfirere/singletons/issues/339#issuecomment-612530482++ lookupKV :: Eq k => k -> [k] -> [v] -> Maybe (k, v)+ lookupKV k [] [] = Nothing+ lookupKV k (k':kk) (v':vv) = lookupKV_If k k' kk v' vv (k == k')++ lookupKV_If :: Eq k => k -> k -> [k] -> v -> [v] -> Bool -> Maybe (k, v)+ lookupKV_If k k' _ v' _ True = Just (k', v')+ lookupKV_If k _ kk _ vv False = lookupKV k kk vv+ |]++{-+Proof that fmap f (lookupKV k kk vv) == lookupKV k kk (fmap f vv)++The proof roughly follows the below structure, modulo the fact that we split+out lookupKV into 2 functions due to a singletons / template-haskell issue,+discussed in the link above.++Inducting on kk vv:++Given:+Wf. (Fmap f (LookupKV k kk vv) ~ LookupKV k kk (Fmap f vv))+Sf. Just (f @@ v') ~ Fmap f (Just v')+Tf. f @@ v' ': Fmap f vv ~ Fmap f (v' ': vv)++Deduce:+(Fmap f (LookupKV k (k' ': kk) (v' ': vv)) ~ LookupKV k (k' ': kk) (Fmap f (v' ': vv)))+ by (Tf), ~+ LookupKV k (k' ': kk) (f @@ v' ': Fmap f vv)++if k == k' if k == k'+ then -> Fmap f (Just v') by (Sf) ~ then -> Just (f @@ v')+ else -> Fmap f (LookupKV k kk vv) by (Wf) ~ else -> Lookup k kk (Fmap f vv)++[].++Note that GHC deduces Sf and Tf automatically, so they don't need to appear+explicitly in the code proof below.+-}++class (Fmap (FmapSym1 f) (LookupKV k kk vv) ~+ LookupKV k kk (Fmap f vv))+ => ProofLookupKV f k (kk :: [kt]) vv where+instance -- base case+ ProofLookupKV f k '[] '[]+instance -- implicit (f @@ v' ': Fmap f vv ~ Fmap f (v' ': vv)) =>+ (ProofLookupKV_If f k k' kk v' vv (k == k'))+ => ProofLookupKV f (k :: kt) (k' ': kk) (v' ': vv)++class (Fmap (FmapSym1 f) (LookupKV_If k k' kk v' vv eq) ~+ LookupKV_If k k' kk (f @@ v') (Fmap f vv) eq)+ => ProofLookupKV_If f (k :: kt) k' kk v' vv eq where+instance -- implicit (Just (f @@ v') ~ Fmap f (Just v')) =>+ ProofLookupKV_If f k k' kk v' vv 'True -- Just v+instance+ ProofLookupKV f k kk vv+ => ProofLookupKV_If f k k' kk v' vv 'False -- lookupKV kk vv+++-- | Maybe that carries its type.+data TMaybe (t :: Maybe k) where+ TNothing :: TMaybe 'Nothing+ TJust :: !t -> TMaybe ('Just t)++-- | Heterogeneous constrained table.+data TCTab (c :: kt ~> Type ~> Constraint) (kk :: [kt]) (vv :: [Type]) :: Type where+ TCNil :: TCTab c '[] '[]+ TCCons :: (c @@ k @@ v) => !(Sing (k :: kt)) -> !v -> !(TCTab c kk vv) -> TCTab c (k : kk) (v : vv)++-- | A 'TCTab' with a constraint that applies only to the value, not the key.+type TCTab' c = TCTab (ConstSym1 (TyCon1 c))++-- | Heterogeneous unconstrained table.+--+-- To add or remove constraints, see 'strengthenTC0', 'strengthenTC' and+-- 'weakenTC'.+type TTab = TCTab NullC2Sym0++-- | Result type of 'lookupTC'.+data TCMaybe c (t :: Maybe (kt, Type)) where+ TCNothing :: TCMaybe c 'Nothing+ TCJust :: Dict (c @@ k @@ v) -> !(Sing k) -> !v -> TCMaybe c ('Just '(k, v))++-- | Lookup an element in the table, and generate some proofs about the result+-- that can be used by the caller.+lookupTC+ :: forall kt c f (k :: kt) (kk :: [kt]) vv+ . SEq kt+ => Sing k+ -> TCTab c kk vv+ -> (TCMaybe c (LookupKV k kk vv), Dict (ProofLookupKV f k kk vv))+lookupTC k TCNil = (TCNothing, Dict)+lookupTC k (TCCons k' v tab) = case k %== k' of+ STrue -> (TCJust Dict k' v, Dict)+ SFalse -> case lookupTC @kt @c @f k tab of+ (res, Dict) -> (res, Dict) -- generate new proof from old proof++-- | Lookup two elements in two related tables.+--+-- The types of the outputs are provably related.+lookupTC2+ :: forall kt c0 c1 f (k :: kt) (kk :: [kt]) vv+ . SEq kt+ => Sing k+ -> TCTab c0 kk vv+ -> TCTab c1 kk (Fmap f vv)+ -> ( TCMaybe c0 (LookupKV k kk vv)+ , TCMaybe c1 (Fmap (FmapSym1 f) (LookupKV k kk vv))+ )+lookupTC2 k TCNil TCNil = (TCNothing, TCNothing)+lookupTC2 k (TCCons k' v tab) (TCCons k'' p post) = case k %== k' of+ STrue -> (TCJust Dict k' v, TCJust Dict k'' p)+ SFalse -> lookupTC2 @kt @c0 @c1 @f k tab post++-- | Zip two related tables, giving a third table related to both.+--+-- The types of the outputs are provably related.+zipWithTC+ :: forall kt c0 c1 cr f1 r (kk :: [kt]) vv+ . TCTab c0 kk vv+ -> TCTab c1 kk (Fmap f1 vv)+ -> ( forall k0 k1 v+ . (c0 @@ k0 @@ v)+ => (c1 @@ k1 @@ (f1 @@ v))+ => Sing k0+ -> v+ -> Sing k1+ -> (f1 @@ v)+ -> (r @@ v, Dict (cr @@ k0 @@ (r @@ v)))+ )+ -> TCTab cr kk (Fmap r vv)+zipWithTC TCNil TCNil f = TCNil+zipWithTC (TCCons k0 v t0) (TCCons k1 f1v t1) f = case f k0 v k1 f1v of+ (v', Dict) -> TCCons k0 v' (zipWithTC @kt @c0 @c1 @cr @f1 @r t0 t1 f)++-- | Zip three related tables, giving a fourth table related to both.+--+-- The types of the outputs are provably related.+zipWith3TC+ -- brittany-disable-next-binding+ -- https://github.com/lspitzner/brittany/issues/299+ :: forall kt c0 c1 c2 cr f1 f2 r (kk :: [kt]) vv+ . TCTab c0 kk vv+ -> TCTab c1 kk (Fmap f1 vv)+ -> TCTab c2 kk (Fmap f2 vv)+ -> ( forall k0 k1 k2 v+ . (c0 @@ k0 @@ v)+ => (c1 @@ k1 @@ (f1 @@ v))+ => (c2 @@ k2 @@ (f2 @@ v))+ => Sing k0 -> v+ -> Sing k1 -> f1 @@ v+ -> Sing k2 -> f2 @@ v+ -> (r @@ v, Dict (cr @@ k0 @@ (r @@ v)))+ )+ -> TCTab cr kk (Fmap r vv)+zipWith3TC TCNil TCNil TCNil f = TCNil+zipWith3TC (TCCons k0 v t0) (TCCons k1 f1v t1) (TCCons k2 f2v t2) f =+ case f k0 v k1 f1v k2 f2v of+ (v', Dict) ->+ TCCons k0 v' (zipWith3TC @kt @c0 @c1 @c2 @cr @f1 @f2 @r t0 t1 t2 f)++type DictOf c = TyCon1 Dict .@#@$$$ c++withTCDict+ :: forall kt c0 c (kk :: [kt]) vv r+ . TCTab c0 kk vv+ -> TTab kk (Fmap (DictOf c) vv)+ -> (ConstrainList (Fmap c vv) => r)+ -> r+withTCDict TCNil TCNil f = f+withTCDict (TCCons _ _ tv) (TCCons _ Dict tc) f = withTCDict @_ @_ @c tv tc f++toTCDict+ :: forall kt c0 c (kk :: [kt]) vv+ . ConstrainList (Fmap c vv)+ => TCTab c0 kk vv+ -> TTab kk (Fmap (DictOf c) vv)+toTCDict TCNil = TCNil+toTCDict (TCCons k _ xs) = TCCons k Dict (toTCDict @_ @_ @c xs)++-- | Weaken the constraint on a 'TCTab'.+weakenTC+ :: forall kt c0 c1 (kk :: [kt]) vv+ . ConstrainList (ZipWith (Class2Sym2 c1 c0) kk vv)+ => TCTab c0 kk vv+ -> TCTab c1 kk vv+weakenTC TCNil = TCNil+weakenTC (TCCons (k :: Sing k) (v :: v) tab) =+ case cls @(c1 @@ k @@ v) @(c0 @@ k @@ v) of+ Sub Dict -> TCCons k v (weakenTC tab)++-- | Strengthen the constraint on a 'TCTab'.+strengthenTC+ :: forall kt c0 c1 (kk :: [kt]) vv+ . ConstrainList (ZipWith c1 kk vv)+ => TCTab c0 kk vv+ -> TCTab (AndC2 c0 c1) kk vv+strengthenTC TCNil = TCNil+strengthenTC (TCCons k v xs) = TCCons k v (strengthenTC @_ @_ @c1 xs)++-- | Strengthen the constraint on a 'TTab'.+strengthenTC0+ :: forall kt c1 (kk :: [kt]) vv+ . ConstrainList (ZipWith c1 kk vv)+ => TTab kk vv+ -> TCTab c1 kk vv+strengthenTC0 TCNil = TCNil+strengthenTC0 (TCCons k v xs) = TCCons k v (strengthenTC0 @_ @c1 xs)
+ src/Control/Static/Serialise.hs view
@@ -0,0 +1,164 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}++module Control.Static.Serialise where++-- external+import qualified Codec.Serialise as SR+import qualified Data.Binary as BN+import qualified Data.ByteString.Lazy as LBS++import Codec.Serialise (Serialise)+import Data.Binary (Binary)+import Data.Dynamic (Dynamic, fromDynamic, toDyn)+import Data.Kind (Type)+import Data.Singletons (Sing)+import Data.Singletons.TH (genDefunSymbols)+import GHC.Generics (Generic)+import Type.Reflection ((:~~:) (..), TypeRep, Typeable,+ eqTypeRep, typeRep)+++-- | Serialisable external value, with an associated static-key.+--+-- @g@ is a type that can generically represent all the external interface of+-- your static values. See 'RepVal' and 'DoubleEncoding' for more details.+data SKeyedExt g = SKeyedExt !String !g+ deriving (Read, Show, Generic, Binary, Serialise, Eq, Ord, Functor)++-- | Possible errors when resolving a key in a static table.+data SKeyedError =+ SKeyedNotFound String+ | SKeyedExtDecodeFailure String+ deriving (Read, Show, Generic, Binary, Serialise, Eq, Ord)++-- | A value and its external representation, indexed by some key.+class RepVal g (v :: Type) (k :: kt) where+ -- | Convert an external value into its generic representation.+ toRep :: Sing k -> v -> g+ -- | Convert a generic representation into its external value.+ --+ -- This may fail, since @g@ may have to represent several other @v'@ as well,+ -- which @k@ should help determine.+ fromRep :: Sing k -> g -> Either String v+genDefunSymbols [''RepVal]++castOrFail :: forall s t . (Typeable s, Typeable t) => s -> Either String t+castOrFail s = case reps `eqTypeRep` rept of+ Just HRefl -> Right s+ Nothing ->+ Left+ $ "fromTypeable: type-mismatch, expecting: "+ <> show rept+ <> "; actual: "+ <> show reps+ where+ rept = typeRep :: TypeRep t+ reps = typeRep :: TypeRep s++-- | 'RepVal' instance for 'Dynamic'.+--+-- Note that by nature this is not serialisable, and is only really meant for+-- testing purposes. Neither can it support a generic 'Eq' or 'Ord' instance;+-- if you need that then try 'DSerialise' or 'DBinary'.+instance Typeable v => RepVal Dynamic v k where+ toRep _ = toDyn+ fromRep _ s = case fromDynamic s of+ Nothing -> Left "fromDynamic failed; type-mismatch"+ -- annoyingly, Dynamic doesn't expose the type for us to print it, nor the+ -- value for us to pass it to castOrFail. If you replace this subexpression+ -- with castOrFail this will type-check as it will try to cast the Dynamic+ -- itself, and always fail at runtime.+ Just v -> Right v++-- | Uniform generic wrapper.+--+-- In a type-safe language like Haskell, one needs to know in advance the type+-- of something in order to deserialise it successfully. In many applications+-- however, the point at which data enters the program is separate from the+-- point at which we have enough type information to fully deserialise a+-- statically-keyed value. Between these points, we often want to deserialise+-- the /other/ parts of that data, and perform logic based on its value.+--+-- This wrapper works around that fact by double-encoding the static-value.+-- This is perhaps suboptimal performance-wise, but is simple to implement and+-- use, especially in a compositional manner. When data first enters the+-- program, one can deserialise the whole data using the mechanism represented+-- by @s@, which will then contain @'HalfEncoded' b@ instances of this type+-- inside it. When you finally have enough type information to perform the rest+-- of the deserialise you can call 'fromRep' on these parts, to recovered the+-- typed value corresponding to each part.+--+-- This wrapper also short-circuits the case of calling 'toRep' then 'fromRep'+-- without attempting to serialise the value in between. In this case the+-- original value is simply wrapped in the 'Decoded' constructor, no attempt to+-- serialise based on @s@ is actually made, and no value based on @b@ is ever+-- constructed.+--+-- If you need optimal performance and really must avoid double-serialising,+-- you can instead define your own ADT as a sum-type over all your possible+-- serialisation types, make this serialisable, and implement 'RepVal' for it.+--+-- @s@ is a constraint over serialisable types, e.g 'Serialise' or 'Binary'.+-- @b@ is the concrete serialisation type, e.g. 'LBS.ByteString'.+data DoubleEncoding s b where+ Decoded :: (Typeable t, s t) => !t -> DoubleEncoding s b+ HalfEncoded :: !b -> DoubleEncoding s b++type DSerialise = DoubleEncoding Serialise LBS.ByteString++instance Serialise DSerialise where+ encode (Decoded t) = SR.encode+ (HalfEncoded (SR.serialise t) :: DoubleEncoding Serialise LBS.ByteString)+ encode (HalfEncoded t) = SR.encode t+ decode = HalfEncoded <$> SR.decode++instance (Typeable v, Serialise v) => RepVal DSerialise v k where+ toRep _ = Decoded+ fromRep _ (Decoded v) = castOrFail v+ fromRep _ (HalfEncoded s) = case SR.deserialiseOrFail s of+ Left e -> Left (show e)+ Right v -> Right v++instance Eq DSerialise where+ a == b = SR.serialise a == SR.serialise b++instance Ord DSerialise where+ compare a b = compare (SR.serialise a) (SR.serialise b)++type DBinary = DoubleEncoding Binary LBS.ByteString++decodeFullyOrFail :: Binary a => LBS.ByteString -> Either String a+decodeFullyOrFail s = case BN.decodeOrFail s of+ Left e -> Left ("Data.Binary decode failure: " <> show e)+ Right (bs, o, v) -> if LBS.null bs+ then Right v+ else Left ("Data.Binary decode leftovers: " <> show (bs, o))++instance Binary DBinary where+ put (Decoded t) =+ BN.put (HalfEncoded (BN.encode t) :: DoubleEncoding Binary LBS.ByteString)+ put (HalfEncoded t) = BN.put t+ get = HalfEncoded <$> BN.get++instance (Typeable v, Binary v) => RepVal DBinary v k where+ toRep _ = Decoded+ fromRep _ (Decoded v) = castOrFail v+ fromRep _ (HalfEncoded s) = decodeFullyOrFail s++instance Eq DBinary where+ a == b = BN.encode a == BN.encode b++instance Ord DBinary where+ compare a b = compare (BN.encode a) (BN.encode b)
+ src/Control/Static/Static.hs view
@@ -0,0 +1,167 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++module Control.Static.Static where++-- external+import Data.Constraint (Dict (..))+import Data.Kind (Type)+import Data.Singletons.Prelude+import Data.Singletons.TH (genDefunSymbols)+import Data.Text (pack, unpack)++-- internal+import Control.Static.Common+import Control.Static.Serialise+++-- | Standalone static key with no associated value.+--+-- Users typically don't need this, and should use 'SKeyed' or 'SKeyedExt'+-- as appropriate.+type SKey (k :: Symbol) = Sing k++-- | Internal value, typed-indexed by an associated static-key.+--+-- Generally, @v@ is not expected to be serialisable or otherwise representable+-- outside of the program. For cases where it is, you should define an instance+-- of 'RepVal'. That then enables you to use 'toSKeyedExt' and+-- other utility functions with this constraint.+data SKeyed k v = SKeyed !(SKey k) !v+ deriving Functor++-- | Similar to 'withSomeSing' for a 'SKeyedExt', extract the type from+-- the 'String' key and run a typed function on the typed value.+withSKeyedExt :: SKeyedExt g -> (forall (a :: Symbol) . SKeyed a g -> r) -> r+withSKeyedExt (SKeyedExt s a) f = withSomeSing (pack s) $ \k -> f (SKeyed k a)++-- | Convert an internal value to an external value, depending on the existence+-- of an instance of 'RepVal' to help perform the conversion.+toSKeyedExt :: RepVal g v k => SKeyed k v -> SKeyedExt g+toSKeyedExt (SKeyed k v) = SKeyedExt (unpack (fromSing k)) (toRep k v)++toSKeyedEither+ :: Sing (k :: Symbol) -> Maybe (Either String v) -> Either SKeyedError v+toSKeyedEither k Nothing = Left $ SKeyedNotFound $ unpack $ fromSing k+toSKeyedEither _ (Just (Left e)) = Left $ SKeyedExtDecodeFailure e+toSKeyedEither _ (Just (Right v)) = Right v++-- | Helper function for building 'TCTab's.+skeyedCons+ :: (c @@ k @@ v) => SKeyed k v -> TCTab c kk vv -> TCTab c (k ': kk) (v ': vv)+skeyedCons (SKeyed k v) = TCCons k v++-- | @RepExt c g ext k v@ is a constraint comprising:+--+-- * @RepVal g (ext v) k@+-- * @c k v@+--+-- modulo singletons defunctionalisation on @c@ and @ext@.+type RepExtSym3 c g ext+ = AndC2 c (FlipSym1 (TyCon2 (RepVal g) .@#@$$$ ApplySym1 ext))+{- Implementation note: this is equivalent to:++type family RepExt c g ext k v :: Constraint where+ RepExt c g ext k v = (c @@ k @@ v, RepVal g (ext @@ v) k)+genDefunSymbols [''RepExt]++However it must be of the form @AndC2 x y@ so that we can define 'repClosureTab'+in terms of 'strengthenTC', which uses 'AndC2'.+-}++-- | A continuation from an internal and external value, to a result type @r@.+type family TyContIX r ext (v :: Type) where+ TyContIX r ext v = v -> ext @@ v -> r+genDefunSymbols [''TyContIX]+--type TyContIXSym2 r ext+-- = ApSym2 (TyCon2 (->)) ((FlipSym1 (TyCon2 (->)) @@ r) .@#@$$$ ApplySym1 ext)++-- | Given an 'SKeyed' of an external value @g@, do the following:+--+-- 1. Lookup the corresponding internal value (I) of type @v@.+-- 2. Decode the external value (X) of type @g@, if its type can be decoded+-- into the type @ext v@.+-- 3. Lookup the corresponding continuation (C).+-- 4. Apply (C) to (I) and (X), returning a value of type @r@.+gwithStatic+ :: forall c0 c1 f g ext (k :: Symbol) (kk :: [Symbol]) vv r+ . TCTab (RepExtSym3 c0 g ext) kk vv+ -> SKeyed k g+ -> TCTab c1 kk (Fmap f vv)+ -> ( forall k' v+ . 'Just '(k', v) ~ LookupKV k kk vv+ => 'Just '(k', f @@ v) ~ Fmap (FmapSym1 f) (LookupKV k kk vv)+ => (c0 @@ k' @@ v)+ => (c1 @@ k' @@ (f @@ v))+ => Sing k'+ -> (f @@ v)+ -> v+ -> (ext @@ v)+ -> r+ )+ -> Either SKeyedError r+gwithStatic tab val@(SKeyed k ga) post go =+ toSKeyedEither k $ case lookupTC2 @_ @_ @_ @f k tab post of+ (TCNothing , TCNothing ) -> Nothing+ (TCJust Dict k' v, TCJust Dict _ p) -> Just $ go k' p v <$> fromRep k' ga+ -- note: yes, it's possible to implement this in terms of withStaticCxt+ -- IMO this version is a bit nicer++withStaticCts+ :: forall c0 c1 g ext (k :: Symbol) (kk :: [Symbol]) vv r+ . TCTab (RepExtSym3 c0 g ext) kk vv+ -> SKeyed k g+ -> TCTab c1 kk (Fmap (TyContIXSym2 r ext) vv)+ -> Either SKeyedError r+withStaticCts tab val post =+ gwithStatic @_ @_ @(TyContIXSym2 r ext) tab val post (flip const)++withSomeStaticCts+ :: forall c0 c1 g ext (kk :: [Symbol]) vv r+ . TCTab (RepExtSym3 c0 g ext) kk vv+ -> SKeyedExt g+ -> TCTab c1 kk (Fmap (TyContIXSym2 r ext) vv)+ -> Either SKeyedError r+withSomeStaticCts tab ext post =+ withSKeyedExt ext $ \(val :: SKeyed k g) -> withStaticCts tab val post++withStaticCxt+ :: forall c f g ext (k :: Symbol) (kk :: [Symbol]) vv r+ . TCTab (RepExtSym3 c g ext) kk vv+ -> SKeyed k g+ -> ( forall k' v+ . 'Just '(k', v) ~ LookupKV k kk vv+ => ProofLookupKV f k kk vv+ => (c @@ k' @@ v) => Sing k' -> v -> (ext @@ v) -> r+ )+ -> Either SKeyedError r+withStaticCxt tab val@(SKeyed k ga) go =+ toSKeyedEither k $ case lookupTC @_ @_ @f k tab of+ (TCNothing , _ ) -> Nothing+ (TCJust Dict k' v, Dict) -> Just $ go k' v <$> fromRep k' ga++withSomeStaticCxt+ :: forall c f g ext (kk :: [Symbol]) vv r+ . TCTab (RepExtSym3 c g ext) kk vv+ -> SKeyedExt g+ -> ( forall k k' v+ . 'Just '(k', v) ~ LookupKV k kk vv+ => ProofLookupKV f k kk vv+ -- keep above constraints; caller can either use or ignore as they wish+ -- without them, caller is prevented from using them at all+ => (c @@ k' @@ v) => Sing k' -> v -> (ext @@ v) -> r+ )+ -> Either SKeyedError r+withSomeStaticCxt tab ext go =+ withSKeyedExt ext $ \(val :: SKeyed k g) -> withStaticCxt @_ @f tab val (go @k)
+ src/Control/Static/TH.hs view
@@ -0,0 +1,227 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module Control.Static.TH+ ( staticRef+ , staticKey+ , staticKeyType+ , mkStatics+ , mkStaticsWithRefs+ , defaultStaticTab+ , mkDefStaticTab+ , mkStaticTab+ -- special utils some users might need+ , CxtW(..)+ )+where++-- external+import Control.Concurrent.MVar (newEmptyMVar, putMVar, takeMVar)+import Data.Functor (($>))+import Data.List (unzip5)+import Data.Singletons (sing)+import GHC.IO.Unsafe (unsafeDupableInterleaveIO)+import Language.Haskell.TH++-- internal+import Control.Static.Common (CxtW (..), TCTab (..), TTab)+import Control.Static.Static (SKeyed (..), skeyedCons)+++-- | Needed for 'mkStaticsWithRefs', definition taken from+-- https://gitlab.haskell.org/ghc/ghc/issues/12073+mfixQ :: (b -> Q b) -> Q b+mfixQ k = do+ m <- runIO newEmptyMVar+ ans <- runIO (unsafeDupableInterleaveIO (takeMVar m))+ result <- k ans+ runIO (putMVar m result)+ pure result++-- | Create top-level statically-keyed values from regular top-level values.+mkStatics :: [Name] -> Q [Dec]+mkStatics ns = mapM getType ns >>= createStatics Nothing++-- | Create top-level statically-keyed values from regular top-level values,+-- when their definitions need to refer to other statically-keyed values.+--+-- Since TH cannot handle references to names defined later in the source file,+-- it is not possible to use 'mkStatics' for this purpose; you must use this+-- function instead, and then register the names later using 'mkStaticTab'.+--+-- See unit tests for example usage.+mkStaticsWithRefs :: ([Exp] -> Q [Dec]) -> Q [Dec]+mkStaticsWithRefs mkDecs = do+ statics <- mfixQ f+ decls <- mkDecs statics+ closures <- createStatics Nothing (sigsOf decls)+ pure $ decls <> closures+ where+ -- note: f must be like this; as per the contract to 'mfix' one must not+ -- evaluate its argument in the definition, or we'll get an infinite loop+ f :: ([Exp] -> Q [Exp])+ f statics = do+ decls <- mkDecs statics+ traverse (staticRef . fst) (sigsOf decls)++defaultStaticTab :: Name+defaultStaticTab = mkName "staticTab"++-- | Create a table holding the static values for a list of top-level names,+-- binding it to the top-level name "staticTab".+mkDefStaticTab :: [Name] -> Q [Dec]+mkDefStaticTab = mkStaticTab defaultStaticTab++-- | Create a table holding the static values for a list of top-level names,+-- binding it to the given top-level name.+mkStaticTab :: Name -> [Name] -> Q [Dec]+mkStaticTab tabName ns = mapM getType ns >>= createStatics (Just tabName)++-- | Refer to a static value, as a 'SKeyed'.+--+-- Be sure to pass the argument to 'mkStaticTab' so the referent exists.+staticRef :: Name -> Q Exp+staticRef = varE . staticName++-- | Get the symbol key of a static value, as a 'Control.Static.SKey'.+--+-- Be sure to pass the argument to 'mkStaticTab' so the referent exists.+--+-- Users typically don't need this; 'staticRef' is more type-safe as it+-- includes the type of the value, and this does not.+staticKey :: Name -> Q Exp+staticKey name = [| sing @ $(symFQN name) |]++-- | Get the symbol key type of a static value, as a type-level string.+staticKeyType :: Name -> Q Type+staticKeyType = symFQN++-- Internal++createStatics :: Maybe Name -> [(Name, Type)] -> Q [Dec]+createStatics tabName sigs = do+ (closures, tyVars, keys, vals, inserts) <- unzip5 <$> mapM genStaticDefs sigs+ staticTab <- maybe (pure [])+ (\n -> genStaticTab n (concat tyVars) keys vals inserts)+ tabName+ pure $ concat closures <> staticTab++genStaticTab :: Name -> [TyVarBndr] -> [Q Type] -> [Q Type] -> [Q Exp] -> Q [Dec]+genStaticTab name tyVars keys vals is = sequence+ [ sigD name $ do+ ForallT tyVars [] <$> [t| TTab $(tyList keys) $(tyList vals) |]+ , sfnD name $ apList is [| TCNil |]+ ]++genStaticDefs :: (Name, Type) -> Q ([Dec], [TyVarBndr], Q Type, Q Type, Q Exp)+genStaticDefs (fullName, fullType) = do+ tyTval <- [t| SKeyed |]+ tyCxtw <- [t| CxtW |]+ --fail $ show fullType+ let (tyVars', tyCxt', typ') = case fullType of+ ForallT vars cxt' mono -> (vars, cxt', mono)+ _ -> ([], [], fullType)+ let tyCxt1 = cxtToType tyCxt'++ -- If there is a constraint, have it wrapped in a CxtW later+ let cxtVal mk n = appE (conE 'CxtW) (mk n)+ (maybeCxt, maybeCxtTy) = case tyCxt' of+ [] -> (id, pure)+ _ -> (cxtVal, \typ -> pure (tyCxtw `AppT` tyCxt1 `AppT` typ))++ -- If the type is of the special forms+ -- - (SKeyed s T -> T) or+ -- - (C => SKeyed s (CxtW C T) -> T)+ -- this means it wants the staticRef passed in as an argument, so arrange for+ -- that to be done later too.+ --+ -- TODO: we probably don't need this, now that we have 'mkStaticsWithRefs'.+ let+ fixVal mk n = appE (mk n) (staticRef n)+ (maybeFix, tyVars, typ) = case typ' of+ ArrowT `AppT` (t `AppT` (VarT sym) `AppT` (c `AppT` cxt' `AppT` typ_)) `AppT` typX+ | t == tyTval && c == tyCxtw && cxt' == tyCxt1 && typ_ == typX+ -> (fixVal, filter (\v -> tyVarName v /= sym) tyVars', typX)++ ArrowT `AppT` (tyTval' `AppT` (VarT sym) `AppT` typ_) `AppT` typX+ | tyTval' == tyTval && typ_ == typX+ -> (fixVal, filter (\v -> tyVarName v /= sym) tyVars', typX)++ _ -> (id, tyVars', typ')++ let mkVal = maybeCxt (maybeFix varE)+ let tyK = symFQN fullName+ let tyV = maybeCxtTy typ+ let name = staticName fullName++ -- define the static only if it wasn't already defined, e.g. via mkStaticsWithRefs+ static <- flip recover (reify name $> []) $ sequence+ [ sigD name $ ForallT tyVars [] <$> [t| SKeyed $(tyK) $(tyV) |]+ , sfnD name [| SKeyed sing $(mkVal fullName) |]+ ]+ pure (static, tyVars, tyK, tyV, [| skeyedCons $(staticRef fullName) |])++staticName :: Name -> Name+staticName n = mkName $ nameBase n ++ "__static"++-- Utils++-- | Apply a list of expressions to a base expression.+apList :: [Q Exp] -> Q Exp -> Q Exp+apList [] base = base+apList (e : es) base = [| $e $ $(apList es base) |]++-- | Construct a promoted-list of types.+tyList :: [Q Type] -> Q Type+tyList [] = promotedNilT+tyList (h : tl) = do+ ty <- h+ (PromotedConsT `AppT` ty `AppT`) <$> tyList tl++-- | Convert a context (a list of types) to a single type.+cxtToType :: Cxt -> Type+cxtToType cxt' = case cxt' of+ [] -> TupleT 0+ [t] -> t+ _ -> go (TupleT (length cxt')) cxt' where+ go part [] = part+ go part (h : tl) = go (part `AppT` h) tl++-- | Look up the "original name" (module:name) and type of a top-level function+getType :: Name -> Q (Name, Type)+getType name = do+ info <- reify name+ case info of+ VarI origName typ _ -> pure (origName, typ)+ _ -> fail $ show name ++ " not a type: " ++ show info++-- | Extract type info from top-level decls without using 'reify'.+sigsOf :: [Dec] -> [(Name, Type)]+sigsOf [] = []+sigsOf (SigD n t : tl) = (n, simplifyType t) : sigsOf tl+sigsOf (_ : tl) = sigsOf tl++-- | Simplify a source-level type. This attempts to do what 'reify' does but+-- without needing the definition to exist at the splice point.+simplifyType :: Type -> Type+simplifyType (ForallT t0 c0 (ForallT t1 c1 t)) =+ simplifyType (ForallT (t0 <> t1) (c0 <> c1) t)+simplifyType t = t++-- | Variation on 'funD' which takes a single expression to define the function+sfnD :: Name -> Q Exp -> Q Dec+sfnD n e = funD n [clause [] (normalB e) []]++-- | The name of a type variable binding occurrence+tyVarName :: TyVarBndr -> Name+tyVarName (PlainTV n ) = n+tyVarName (KindedTV n _) = n++-- | Fully qualified name, as a type-level String literal of kind Symbol+symFQN :: Name -> Q Type+symFQN n = do+ loc <- location+ pure $ LitT $ StrTyLit $ loc_module loc ++ "." ++ nameBase n
+ static.cabal view
@@ -0,0 +1,185 @@+Cabal-Version: 3.0+Name: static+Version: 0.1.0.0+Synopsis: Type-safe and interoperable static values and closures+Description:+ Serialise closures in a type-safe way that interoperates across binaries.++ This package is inspired by @distributed-static@ and GHC's /static pointers/+ in @GHC.StaticPtr@, which came out of the same research. However, we make+ some significantly-different design choices, described below.++ GHC made the design choice to focus on guaranteeing that static values could+ be passed between nodes if they were running the exact same binary, since+ they are indexed by 64-bit integers automatically-generated by the compiler.+ @distributed-static@ attempts to support the same source program compiled by+ different versions of GHC. As part of this effort to preserve stability, one+ must pass in a table ('RemoteTable') whose keys represent the stability, and+ whose values are resolved potentially differently across compiler versions.++ The need for the caller to pass in a 'RemoteTable' is seen as a liability, so+ two subsequent packages @distributed-closure@ and @static-closure@ take the+ opposite approach, ripping out the 'RemoteTable' but doubling down on GHC's+ choice to guarantee compatibility only across different processes running the+ exact same binary program. Their uses cases are focused around compute+ clusters and other forms of centralised distributed computing, where this is+ easy to achieve and not a problem.++ Sometimes security is cited as a reason to have this restriction, but this is+ a /bogus argument/. "Guarantee compatibility only across same binary" means+ "same binary => compatibility" whereas the bogus security argument depends on+ "compatibility => same binary", which is not true - anyone who analyses your+ binary will know which numbers to spoof, to convince your program via this+ interface that they are "running the same code". Guaranteeing "same binary"+ in an adversial setting is in fact extremely hard and cannot be achieved+ perfectly; in the real-world it can only be approximated, and should be done+ so via mechanisms designed for it, not via numbers that are slightly hard to+ brute force at best and trivial to find out at worst.++ This package makes the /opposite/ choice, intended for less restricted and+ more open distributed computing environments such as the internet and+ decentralised protocols. In these contexts, the requirement of running the+ exact same binary program is impossible to achieve in practise. Furthermore,+ we see it as an /advantage/ that code does not need to be exactly the same -+ for example, one can serialise a closure and its inputs, /upgrade your code/,+ then resume running the closure on the same deserialised input arguments but+ with a bugfixed closure. The necessity to pass in an explicit 'RemoteTable'+ (here simply called 'staticTab') is not a liability, but a useful tool to+ represent high-level compatibility and interoperability. Two nodes with the+ same keys in their 'staticTab's, know that they can talk to each other+ interoperably even if their implementations differ significantly. One node+ that wishes to talk to different nodes running different minor versions of+ the same protocol, could instantiate two different 'staticTab's with the same+ keys but different implementations, to handle behavioural nuances between the+ minor versions. In general, it's a useful bit of metadata to keep around in+ your program code, and can help you perform smooth upgrades of a+ non-centralised networking protocol more easily.++ There are also a few technical differences between this and+ @distributed-static@, some of which could be re-adopted there too:++ * We use dependent-types and type-level programming to guarantee type+ safety, rather than 'Rank1Dynamic'. This enables us to store all possible+ closure types instead of just rank-1 polymorphic functions, including but+ not limited to: rank-n functions, functions with constraints, those using+ higher-kinded types, etc.++ * Our serialisation typeclasses are designed to interoperate with many+ different serialisation frameworks. Instances for 'Data.Binary' and+ 'Codec.Serialise' are provided here for convenience.++ * We have additional Template Haskell splices that support creating static+ values from top-level definitions that must refer to other static values,+ whether they be recursive or mutually-recursive or neither. This is+ achieved using an implementation of @mfix@ for the @Q@ monad.++ We did /not/ implement the ability to compose static references. The main+ reason is that, in our view, the /purpose/ of static closures is to represent+ which top-level tasks to execute, and the inputs to execute it on. This is+ the /interface/ or /contract/ of this concept. /How you run/ the task is an+ implementation detail, and as discussed above, this might be different across+ different machines or as time passes and we upgrade the code. Therefore it+ makes no sense to serialise a representation of "task A is the composition of+ closure B and closure C", because it is irrelevant to the /interface/.++ If your /interface/ is actually "run arbitrary user-defined code" (e.g. in a+ VM or EDSL evaluator) then it would indeed make sense to support composition,+ but then you should define your own AST, evaluator, and serialiser for this;+ and pass the ASTs around as regular runtime values, not static values.+ Supporting arbitrary ASTs like this is outside of the scope of this library.++ Further, in Haskell there are many ways of applying values not just @(_ :: a+ -> b) (_ :: a) :: b@, e.g. with constraints, with a combination of static and+ non-static arguments, with type applications, and so on. Only the simple form+ @(_ :: a -> b) (_ :: a) :: b@ is likely to be interoperable across multiple+ languages. Supporting AST statics would therefore unnecessarily restrict how+ we can implement the behaviour of a static closure in our chosen language.++ See unit tests for example usage, e.g.+ <https://github.com/infinity0/hs-static/tree/master/test/Control/Static/UnitTests.hs UnitTests>+Homepage: https://github.com/infinity0/hs-static+Bug-Reports: https://github.com/infinity0/hs-static/issues+License: GPL-3.0-or-later+License-File: LICENSE.GPL-3+Author: Ximin Luo+Maintainer: infinity0@pwned.gg+Copyright: 2020 Ximin Luo+Category: Control, Static, Closure+Tested-With: GHC >= 8.8.3+Extra-Source-Files: CHANGELOG.md++Source-Repository head+ Type: git+ Location: https://github.com/infinity0/hs-static++Flag dev+ Description: Set compile flags for development+ Default: False+ Manual: True++Common generic+ Default-Language: Haskell2010+ Build-Depends: base >= 4 && < 5,+ GHC-Options:+ -Wall+ -Wno-unused-matches+ -Wredundant-constraints+ -Wincomplete-record-updates+ -Wincomplete-uni-patterns+ if flag(dev)+ GHC-Options:+ -Werror+ -O2+ -- some optimisations cause memory leaks; switch on -O2 and profiling so we+ -- can detect this during development so it doesn't cause surprises later+ GHC-Prof-Options:+ -fprof-auto++Library+ Import: generic+ Build-Depends:+ constraints+ , text+ , singletons+ -- for serialisation+ , binary+ , bytestring+ , serialise+ -- Control.Static.TH+ , template-haskell+ HS-Source-Dirs: src+ Exposed-Modules:+ Control.Static+ , Control.Static.Common+ , Control.Static.Closure+ , Control.Static.Serialise+ , Control.Static.Static+ , Control.Static.TH++Test-Suite doctests+ Import: generic+ GHC-Options: -threaded+ Build-Depends:+ doctest+ , static+ HS-Source-Dirs: test+ Type: exitcode-stdio-1.0+ Main-Is: DocTests.hs++Test-Suite unit+ Import: generic+ GHC-Options: -threaded+ Build-Depends:+ tasty+ , tasty-quickcheck+ , tasty-hunit+ , checkers+ , static+ , lens+ , mtl+ , transformers+ HS-Source-Dirs: test+ Type: exitcode-stdio-1.0+ Main-Is: UnitTests.hs+ Other-Modules:+ Control.Static.UnitTests
+ test/Control/Static/UnitTests.hs view
@@ -0,0 +1,234 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}++module Control.Static.UnitTests where++-- external, testing+import Test.Tasty+import Test.Tasty.HUnit++-- external+import Control.Monad.RWS.Strict (RWST (..), evalRWST)+import Control.Monad.State.Class (MonadState (..))+import Control.Monad.Writer.Class (MonadWriter (..))+import Control.Static (ClosureApply, DSerialise,+ RepVal (..), applyClosure,+ envTabCons, envTabNil,+ evalSomeClosure, mkClosureTab,+ repClosureTab)+import Control.Static.TH (mkDefStaticTab, mkStatics,+ mkStaticsWithRefs, staticKeyType,+ staticRef)++-- These unit tests are written to showcase all the features & possibilities of+-- using this library. It is certainly not the simplest way of achieving what+-- it is actually doing. When using this library, bear this in mind and don't+-- just blindly copy the below - aim to simplify as much of it as possible.++data TEnv m g = TEnv {+ pushTask :: !(ClosureApply g -> m ())+ , pushLog :: !(String -> m ())+}++writeLog :: MonadWriter [String] m => () -> String -> m [Int]+writeLog _ x = tell [x] >> pure []+mkStatics ['writeLog]+-- note: the above call to mkStatics is actually redundant; mkDefStaticTab+-- automatically will do this for any passed-in names that did not already have+-- statics created for them. We call it here for demonstration purposes.++collatzCycle0 :: [Integer]+collatzCycle0 = [0]+collatzCycle1 :: [Integer]+collatzCycle1 = [1, 4, 2]+collatzCycle2 :: [Integer]+collatzCycle2 = [-1, -2]+collatzCycle3 :: [Integer]+collatzCycle3 = [-5, -14, -7, -20, -10]+collatzCycle4 :: [Integer]+collatzCycle4 =+ [-17, -50, -25, -74, -37, -110, -55, -164, -82, -41]+ ++ [-122, -61, -182, -91, -272, -136, -68, -34]++mkStaticsWithRefs $ \(~[collatz', collatzOdd', collatzEven']) -> [d|+ collatz+ :: RepVal g Integer $(staticKeyType 'collatzOdd)+ => RepVal g Integer $(staticKeyType 'collatzEven)+ => Monad m => TEnv m g -> Integer -> m [Int]+ collatz env x = do+ pushLog $ "got: " <> show x+ if+ | x `elem` collatzCycle0 -> pure [0]+ | x `elem` collatzCycle1 -> pure [1]+ | x `elem` collatzCycle2 -> pure [2]+ | x `elem` collatzCycle3 -> pure [3]+ | x `elem` collatzCycle4 -> pure [4]+ | x `mod` 2 == 1 -> do+ pushTask (applyClosure $(pure collatzOdd') x)+ pure []+ | otherwise -> do+ pushTask (applyClosure $(pure collatzEven') x)+ pure []+ where TEnv {..} = env++ collatzOdd+ :: RepVal g Integer $(staticKeyType 'collatz)+ => Monad m => TEnv m g -> Integer -> m [Int]+ collatzOdd env x = do+ pushLog $ "got odd: " <> show x+ pushTask (applyClosure $(pure collatz') (3 * x + 1))+ pure []+ where TEnv {..} = env++ collatzEven+ :: RepVal g Integer $(staticKeyType 'collatz)+ => Monad m => TEnv m g -> Integer -> m [Int]+ collatzEven env x = do+ pushLog $ "got even: " <> show x+ pushTask (applyClosure $(pure collatz') (x `div` 2))+ pure []+ where TEnv {..} = env+ |]++mkDefStaticTab ['writeLog, 'collatz, 'collatzOdd, 'collatzEven]++-- In most use-cases, you don't need to distinguish between the tasks, and+-- 'TaskArg' (further below) is simpler and better . On the off-chance that you+-- do need to, this is how you would do that, using @$(staticKeyType 'KEY)@.+data Task =+ TaskLog !String+ | TaskCollatz !Integer+ | TaskCollatzOdd !Integer+ | TaskCollatzEven !Integer+ deriving (Show, Read, Eq, Ord)+instance RepVal Task String $(staticKeyType 'writeLog) where+ toRep _ = TaskLog+ fromRep _ (TaskLog i) = Right i+ fromRep _ t = Left $ "expect TaskLog, got " <> show t+instance RepVal Task Integer $(staticKeyType 'collatz) where+ toRep _ = TaskCollatz+ fromRep _ (TaskCollatz i) = Right i+ fromRep _ t = Left $ "expect TaskCollatz, got " <> show t+instance RepVal Task Integer $(staticKeyType 'collatzOdd) where+ toRep _ = TaskCollatzOdd+ fromRep _ (TaskCollatzOdd i) = Right i+ fromRep _ t = Left $ "expect TaskCollatzOdd, got " <> show t+instance RepVal Task Integer $(staticKeyType 'collatzEven) where+ toRep _ = TaskCollatzEven+ fromRep _ (TaskCollatzEven i) = Right i+ fromRep _ t = Left $ "expect TaskCollatzEven, got " <> show t++-- You can either define your own 'g' like here, or use one of the provided+-- ones, like 'DSerialise' or 'DBinary'.+data TaskArg =+ ArgString !String+ | ArgInteger !Integer+ deriving (Show, Read, Eq, Ord)+instance RepVal TaskArg String k where+ toRep _ = ArgString+ fromRep _ (ArgString i) = Right i+ fromRep _ t = Left $ "expect ArgString, got " <> show t+instance RepVal TaskArg Integer k where+ toRep _ = ArgInteger+ fromRep _ (ArgInteger i) = Right i+ fromRep _ t = Left $ "expect ArgInteger, got " <> show t++monadEnv+ :: RepVal g String $(staticKeyType 'writeLog)+ => MonadState [ClosureApply g] m => String -> TEnv m g+monadEnv prefix =+ let pushTask t = state (\tt -> ((), tt ++ [t]))+ pushLog s = pushTask (applyClosure $(staticRef 'writeLog) s)+ in TEnv { .. }++runAllTasks+ :: forall g tm+ . RepVal g String $(staticKeyType 'writeLog)+ => RepVal g Integer $(staticKeyType 'collatz)+ => RepVal g Integer $(staticKeyType 'collatzOdd)+ => RepVal g Integer $(staticKeyType 'collatzEven)+ => MonadWriter [String] (tm IO)+ => MonadState [ClosureApply g] (tm IO)+ => MonadFail (tm IO)+ => (String -> TEnv (tm IO) g)+ -> (tm IO Int -> [ClosureApply g] -> IO (Int, [String]))+ -> [ClosureApply g]+ -> Int+ -> [String]+ -> IO ()+runAllTasks mkEnv evalT initCl expectRuns expectLogs = do+ (actualRuns, actualLogs) <- evalT (go 0) initCl+ assertEqual "runs" expectRuns actualRuns+ assertEqual "logs" expectLogs actualLogs+ where+ go i = state popTask >>= \case+ Nothing -> pure i+ Just t -> do+ res <- run t+ let msg = (\c -> "result: cycle #" <> show c) <$> res+ state $ pushTasks $ applyClosure $(staticRef 'writeLog) <$> msg+ go (i + 1)+ popTask [] = (Nothing, [])+ popTask (h : tl) = (Just h, tl)+ pushTasks tt' tt = ((), tt ++ tt')+ run cl = case evalSomeClosure closureTab cl of+ Left e -> fail (show e)+ Right r -> r+ closureTab =+ repClosureTab @_ @g+ $ mkClosureTab staticTab+ $ envTabCons $(staticRef 'writeLog) ()+ $ envTabCons $(staticRef 'collatz) (mkEnv "collatz")+ $ envTabCons $(staticRef 'collatzOdd) (mkEnv "collatzOdd")+ $ envTabCons $(staticRef 'collatzEven) (mkEnv "collatzEven")+ $ envTabNil++tests :: TestTree+tests = testGroup+ "Control.Static.UnitTests"+ [ testCase "smoke @Task" $ do+ runAllTasks @Task @(RWST () [String] [ClosureApply Task])+ monadEnv+ (`evalRWST` ())+ [applyClosure $(staticRef 'collatz) (4 :: Integer)]+ 3+ ["got: 4", "result: cycle #1"]+ , testCase "smoke @TaskArg" $ do+ runAllTasks @TaskArg @(RWST () [String] [ClosureApply TaskArg])+ monadEnv+ (`evalRWST` ())+ [applyClosure $(staticRef 'collatz) (30 :: Integer)]+ 67+ ( ["got: 30", "got even: 30", "got: 15", "got odd: 15", "got: 46"]+ ++ ["got even: 46", "got: 23", "got odd: 23", "got: 70", "got even: 70"]+ ++ ["got: 35", "got odd: 35", "got: 106", "got even: 106", "got: 53"]+ ++ ["got odd: 53", "got: 160", "got even: 160", "got: 80", "got even: 80"]+ ++ ["got: 40", "got even: 40", "got: 20", "got even: 20", "got: 10"]+ ++ ["got even: 10", "got: 5", "got odd: 5", "got: 16", "got even: 16"]+ ++ ["got: 8", "got even: 8", "got: 4", "result: cycle #1"]+ )+ , testCase "smoke @DSerialise" $ do+ runAllTasks @DSerialise @(RWST () [String] [ClosureApply DSerialise])+ monadEnv+ (`evalRWST` ())+ [applyClosure $(staticRef 'collatz) (-30 :: Integer)]+ 39+ ( ["got: -30", "got even: -30", "got: -15", "got odd: -15", "got: -44"]+ ++ ["got even: -44", "got: -22", "got even: -22", "got: -11"]+ ++ ["got odd: -11", "got: -32", "got even: -32", "got: -16"]+ ++ ["got even: -16", "got: -8", "got even: -8", "got: -4", "got even: -4"]+ ++ ["got: -2", "result: cycle #2"]+ )+ ]
+ test/DocTests.hs view
@@ -0,0 +1,4 @@+import Test.DocTest++main :: IO ()+main = doctest ["-i", "src"]
+ test/UnitTests.hs view
@@ -0,0 +1,7 @@+import Test.Tasty++import Control.Static.UnitTests (tests)++main :: IO ()+main = do+ defaultMain $ testGroup "Static *" [Control.Static.UnitTests.tests]