Metadata

Source URL:: https://zenodo.org/records/5913940
Topics:: #zenodo, #polarized_subtyping, #polarized-subtyping, #artifact, #esop

Artifact accompanying the paper Polarized Subtyping, published in the proceedings of ESOP 2022. We've included an extended version of the paper with this submission (2201.10998.pdf), which is also available directly on arXiv.  Docker Image: The artifact is packaged as a docker container. The docker image is available on Github Packages, under the esop22 tag. We've also included the docker image as a .tar file (polite-esop:esop22.docker.tar), which can be loaded directly via: % docker load polite-esop:esop22.docker.tar Source Code: All of the software, source code (the Polite programming language), and related files are packaged within the docker container (available on Github Packages and in this submission). Follow the steps below (or in README.txt), to pull the docker image, run it, and run the paper-related examples, i.e. the .polsub files. We've also included these files as part of this submission for posterity: bin.polsub emptyfull.polsub examples.polsub omega.polsub stream.polsub   Getting Started Guide 1. Pull down the public docker image: % docker pull ghcr.io/zeeshanlakhani/polite-esop:esop22 2. Run the docker container interactively: % docker run --rm -it --name polite-esop ghcr.io/zeeshanlakhani/polite-esop:esop22 Of note, this is a x86-64/amd64 (Intel) built container. The artifact will not run on arm64 hosts (e.g. an M1 macbook). 3. After running step 2., you'll enter into the designated /polite/esop22 directory within the container, where there are 5 example .polsub files to run, associated with the paper submission. You can use the polite executable (already in the PATH) to view the output of each example: % polite bin.polsub % polite emptyfull.polsub % polite examples.polsub % polite omega.polsub % polite stream.polsub 4. To run examples and view purposeful typechecking errors in relation to subtyping, then run any of the examples above with the -d debug flag: % polite -d bin.polsub 5. Additionally, you can run the examples interactively in SML/NJ (by first running sml): CM.make "../src/sources.cm"; Top.polite "bin.polsub"; Top.polite "emptyfull.polsub"; Top.polite "examples.polsub"; Top.polite "omega.polsub"; Top.polite "stream.polsub"; Step by Step Instructions Now, we'll walk through each of the polsub programs in /polite/esop22, which exhibit key examples in and claims made by the paper. Throughout the example programs, [stream0] and (thunk stream0) are interchangeable, as is y and return y, where using thunk and return matches to how we express thunk values and return computations in the paper. As in the paper, our bidirectional typechecking algorithm is polarized. As is evident from the bidirectional rules, A : B, for positive types A and B, will hold exactly when fun x = x : A - B. Similarly, for negative types A and B, A : B is true exactly if fun x = force x : [A] - B. We use this in some of the examples to verify or refute some subtyping relations. 1. % polite -d examples.polsub This program demonstrates general type examples used throughout the paper, including much of what exists in Appendix A (in the extended version of the paper). Samples include: nat and bool (positive) variant records types, how list or queue datatypes would be constructed, identity functions mutually recursive even and odd datatypes, a simple, incorrect function type computation in succ' 2. % polite -d bin.polsub This program demonstrates our first example in Section 2.2, where we expect the subtyping relationships pos = std = bin to hold, as every positive standard number is a standard number, and every standard number is a binary number. The fail keyword showcases where subtyping is expected to fail. The precise locations of the errors are propagated when using the -d flag, e.g. ./esop22/bin.polsub:31.38-31.44:error:subtyping fails: std not : pos | 'b1 x2 = 'b0 x2 } eval evaluates computation expression, e.g. ten, eleven, etc. The inc, dec0 functions match up with our claims in the paper, where dec0 should indeed fail. Of note, the dec example in the first version of our paper had a typo, which we demonstrate the failure of in dectypo. We show the correct version with the computation dec and have already made the change in the available submission. 3. % polite stream.polsub This program demonstrates our second example in Section 2.2, where we have an example of a type with mixed polarities: a stream of std binary numbers with a finite amount of padding between consecutive numbers. As in the paper, we present padded streams as mutually dependent type definitions, one positive and one negative. zstream demonstrates the usefulness of variant records with one alternative 'some. The expressions compress and omit are two mutually recursive functions used to generate a stream with zero padding from a stream of arbitrary (but finite) padding. compress', omit' and the evaluation of stream0' are used here just to establish how the language implementation can interchangeably use [a] for thunk a and b for return b, where the latter of each is used in the paper, but is more cumbersome for writing programs. Evaluated expressions stream0 and stream1 validate how we can actuallycompress a padded stream into one with zero padding! 4. % polite omega.polsub This program demonstrates our third example in Section 2.2, where we consider the embedding of the untyped lambda calculus in a polarized setting, e.g. (U^- : [U] - U), and highlight the notion of semantic typing and how it ensures behavioral soundness. As in the paper, omega and Omega are equirecursive type definitions and well-typed even though the evaluation of Omega would diverge (i.e. never terminate). The commented-out eval nontermination showcases this and, indeed, would never terminate if actually executed. 5. % polite -d emptyfull.polsub Here we demonstrate examples in relation to our presentation of "emptiness" and "fullness" in the paper (Semantic Subtyping, Section 4.1). In this program, we showcase how to check for the emptiness and fullness of types with our implementation. For positive types, we check that a type t is empty by typechecking an identity function from t into an empty type (ex1, ex3). If typechecking the identity function from a positive type t to an empty type fails, we conclude that the type is not empty (ex2, ex4). For negative types, we can use our implementation to check when full types are supertypes of other types (inf_sub_top, inf_sub_emp) and when a type (e.g. inf) is not full by checking that the typechecking of an identity function from a full type fails (top_nsub_inf, comp emp_nsub_inf). The 5 programs above illustrate various examples related to our paper and show that our language implementation, Polite, works faithfully and as expected. Outside of the esop22 directory, (e.g. % cd /polite), we include all of the source code for the implementation, as well as more examples and regression tests, which include our ongoing and future work: adding intersections and unions to polarizing subtyping. The polite.readme.txt in the /polite directory also shows our language's grammar. Files (in the container) /polite/esop22/                       -- ESOP22 paper-related examples and documentation /polite/src/                               -- implementation in SML /polite/examples/                   -- some example programs, some of which include intersection and union (sub)typing /polite/tests/                           -- regression tests /polite/polite.readme.txt        -- general documentation for the Polite programming language implementation Description An implementation of the Polite programming language based on call-by-push-value, equirecursive types, subtyping, and intersection and union types.  The language version with subtyping but without intersections and unions is described in: Polarized Subtyping Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning European Symposium on Programming (ESOP 2022) Contributors (implementation): Zeeshan Lakhani Frank Pfenning Contributors (theory): Ankush Das Henry DeYoung Andreia Mordido

Highlights