diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 466376adf..b82c5b757 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -10,6 +10,10 @@ on: - opened - synchronize +permissions: + contents: read + statuses: write + env: CARGO_TERM_COLOR: always diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml index ec50f6e85..db5e33f6a 100644 --- a/.github/workflows/lint.yml +++ b/.github/workflows/lint.yml @@ -10,6 +10,8 @@ on: - opened - synchronize +permissions: read-all + jobs: build: name: Lint Code Base @@ -17,14 +19,13 @@ jobs: steps: - name: Checkout Code - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 - name: Lint Code Base - uses: github/super-linter/slim@v4 + uses: super-linter/super-linter/slim@v6.3.0 env: - VALIDATE_ALL_CODEBASE: false # JSCPD is disabled because it falsely flags duplicated Rust generic parameter definitions VALIDATE_JSCPD: false # We use eslint instead of the linter named "standard" @@ -33,5 +34,7 @@ jobs: TYPESCRIPT_DEFAULT_STYLE: prettier # We use a slightly different stylelint version/setup VALIDATE_CSS: false - DEFAULT_BRANCH: master + # We don't validate formatting of bash scripts + VALIDATE_SHELL_SHFMT: false + DEFAULT_BRANCH: main GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 08788fff2..7cdd908d7 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -2,12 +2,12 @@ Pull requests, bug reports and feature requests are highly welcomed and encouraged! -### Contents +## Contents - [Pull Request Workflow](#pull-request-workflow) - [Release Workflow](#release-workflow) -### Pull request workflow +## Pull request workflow All changes to the codebase should go through pull-requests. We do not allow commits directly on the `main` branch of the repository. @@ -18,7 +18,7 @@ Please check that you observe the following guidelines: - Every PR needs to have at least 1 approval before it can be merged. - We enforce a linear history on the `main` branch, so every PR must either be rebased or rebased and squashed before it is merged into `main`. -### Release workflow +## Release workflow We use the following workflow for generating a new release for version `x.x.x`: diff --git a/web/packages/app/assets/tutorial.css b/web/packages/app/assets/demo.css similarity index 100% rename from web/packages/app/assets/tutorial.css rename to web/packages/app/assets/demo.css diff --git a/web/packages/app/assets/tutorial.html b/web/packages/app/assets/demo.html similarity index 55% rename from web/packages/app/assets/tutorial.html rename to web/packages/app/assets/demo.html index 65328f613..6c13eb12d 100644 --- a/web/packages/app/assets/tutorial.html +++ b/web/packages/app/assets/demo.html @@ -4,7 +4,7 @@ - Deriving Dependently-Typed OOP from First Principles + Polarity Demo @@ -30,14 +30,7 @@
-

Deriving Dependently-Typed OOP from First Principles

- -

This is the web demo accompanying the OOPSLA 2024 paper Deriving Dependently-Typed OOP from First Principles. - You - will find - the most recent version of the language on polarity-lang.github.io. -

+

Polarity Demo

- -
-

Tutorial

-

- This is a short overview of the syntax of our language. - Feel free to copy and paste sections of the tutorial code into the interactive editor above to try out the - examples on your own. -

- -
- Data Types - {{ data-types }} -
- -
- Codata Types - {{ codata-types }} -
- -
- Definitions - {{ definitions }} -
- -
- Codefinitions - {{ codefinitions }} -
- -
- Comments - {{ comments }} -
- -
- Typed Holes - {{ typed-holes }} -
-
- The Main Expression - {{ main-expression }} -
-
diff --git a/web/packages/app/assets/tutorial/codata-types.md b/web/packages/app/assets/tutorial/codata-types.md deleted file mode 100644 index 9b3f3556a..000000000 --- a/web/packages/app/assets/tutorial/codata-types.md +++ /dev/null @@ -1,42 +0,0 @@ -Codata types are specified by a list of methods or destructors. -A very simple example is the type of pairs of a boolean and a natural number: - -```pol -data Bool { True, False } -data Nat { Z, S(n: Nat)} -codata Pair { - proj1: Bool, - proj2: Nat -} -``` - -This type supports two observations; the first observations `proj1` yields a boolean value when invoked on a `Pair`, and the observation `proj2` yields a natural number. - -A common codata type that is typically built into many programming languages is the function type. -In our language, it is not built-in, but we can define it as follows: - -```pol -codata Fun(a b: Type) { - Fun(a, b).ap(a: Type, b: Type, x: a) : b -} -``` - -Codata types can also model infinite types. The type of infinite streams is a classical example and written like this: - -```pol -codata Stream(a: Type) { - Stream(a).head(a: Type) : a, - Stream(a).tail(a: Type) : Stream(a), -} -``` - -Sometimes we also need to reference the object on which a method is invoked in its return type. -This is especially the case when we want an observation to yield a proof that the object satisfies some property. -Here is a simple example which shows how this can be expressed: - -```pol -codata Bool { - Bool.neg : Bool, - (x: Bool).neg_inverse : Eq(Bool, x, x.neg.neg), -} -``` diff --git a/web/packages/app/assets/tutorial/codefinitions.md b/web/packages/app/assets/tutorial/codefinitions.md deleted file mode 100644 index 9ac6af013..000000000 --- a/web/packages/app/assets/tutorial/codefinitions.md +++ /dev/null @@ -1,38 +0,0 @@ -Codefinitions create producers (or objects) for codata types. -They need to define the behavior of the object when each of its destructors is invoked. -Analogously to pattern matching, where we pattern match on the constructors of a data type, we *copattern match* on the destructors of a codata type. -For example, we can create a pair with the `Pair` codata type defined above as follows: - -```pol -codef MyPair: Pair { - proj1 => True, - proj2 => 42, -} -``` - -We can retrieve the values in the pair by invoking one of the destructors. -For instance, `MyPair.proj2` will yield the result of `42`. - -Codefinitions can also be used to construct infinite objects. -For instance, we can generate an infinite stream that counts upwards as follows: - -```pol -codef CountUp(n: Nat): Stream(Nat) { - head(_) => n, - tail(_) => CountUp(S(n)), -} -``` - -Finally, codefinitions can also return proofs that they fulfill certain properties: - -```pol -codef True: Bool { - not => False, - neg_inverse => Refl(Bool, True), -} - -codef False: Bool { - not => True, - neg_inverse => Refl(Bool, False), -} -``` diff --git a/web/packages/app/assets/tutorial/comments.md b/web/packages/app/assets/tutorial/comments.md deleted file mode 100644 index 49af76c87..000000000 --- a/web/packages/app/assets/tutorial/comments.md +++ /dev/null @@ -1,15 +0,0 @@ -Line comments are written using two dashes: `-- This is a comment`. -Certain items of the program can also be annotated with a documentation comment. -Here is an example using doc-comments: - -```pol --- | The type of booleans -data Bool { - -- | The boolean truth value - True, - -- | The boolean false value - False, -} -``` - -These documentation comments are preserved during defunctionalization and refunctionalization. diff --git a/web/packages/app/assets/tutorial/data-types.md b/web/packages/app/assets/tutorial/data-types.md deleted file mode 100644 index 552da1e67..000000000 --- a/web/packages/app/assets/tutorial/data-types.md +++ /dev/null @@ -1,44 +0,0 @@ -The simplest form of data types do not have parameters or indices. -In that case, the constructors of the data type can be given as a comma-separated list. -As with all syntactic constructs, we always allow trailing commas. - -```pol -data Bool { True, False, } -``` - -In the more general case we have to specify the precise type that a constructor constructs. -Therefore, the above data type declaration can be written more explicitly as: - -```pol -data Bool { True: Bool, False: Bool } -``` - -A simple example of a parameterized type is the type of singly-linked lists of some type `a`. -In that case, we have to specify both the parameters of the type constructor `List`, and the instantiations of the term constructors `Nil` and `Cons`. -For the parameter of the type constructor `List` we make use of the impredicative type universe, which is written `Type`. - -```pol -data List(a: Type) { - Nil(a: Type): List(a), - Cons(a: Type, x: a, xs: List(a)): List(a) -} -``` - -A proper dependent type is the type of length-indexed lists: the vector type. -The `VNil` and `VCons` constructors of vectors create vectors with different indices. - -```pol -data Nat { Z, S(n: Nat) } -data Vec(a: Type, n: Nat) { - VNil(a: Type): Vec(a, Z), - VCons(a: Type, n: Nat, x: a, xs: Vec(a, n)): Vec(a, S(n)) -} -``` - -Finally, we can define the Martin-Löf equality type as follows: - -```pol -data Eq (a: Type, x y: a) { - Refl(a: Type, x: a) : Eq(a, x, x) -} -``` diff --git a/web/packages/app/assets/tutorial/definitions.md b/web/packages/app/assets/tutorial/definitions.md deleted file mode 100644 index 34802e746..000000000 --- a/web/packages/app/assets/tutorial/definitions.md +++ /dev/null @@ -1,51 +0,0 @@ -Definitions create a consumer (method) for a data type. -These consumers receive an implicit input on which they pattern match. -As a simple example, we can define Boolean negation as follows: - -```pol -def Bool.neg: Bool { - True => False, - False => True, -} - -``` - -Definitions can be recursive. -For instance, we can define addition on natural numbers as follows: - -```pol -def Nat.add(y: Nat) : Nat { - Z => y, - S(x) => S(x.add(y)), -} -``` - -Definitions can also deal with parametrized types. -For instance, we can define a `map` method for the data type `List` as follows: - -```pol -def List(a).map(a b: Type, f: Fun(a, b)): List(b) { - Nil(a) => Nil(b), - Cons(a, x, xs) => Cons(b, f.ap(a, b, x), xs.map(a, b, f)), -} -``` - -Finally, to illustrate dependently typed definitions, let us give the classic example of defining `append` on length-indexed lists: - -```pol -def Vec(a, n).append(a: Type, n m: Nat, ys: Vec(a, m)) : Vec(a, n.add(m)) { - VNil(a) => ys, - VCons(a, n', x, xs) => VCons(a, n'.add(m), x, xs.append(a, n', m, ys)) -} -``` - -Last, but certainly not least, the return type of a definition may not only depend on its parameters but also on its (implicit) input. -To do so, we can make the input explicit by assigning it a name. -For instance, we can prove that Boolean negation is its own inverse as follows: - -```pol -def (x: Bool).neg_inverse: Eq(Bool, x, x.not.not) { - True => Refl(Bool, True), - False => Refl(Bool, False) -} -``` diff --git a/web/packages/app/assets/tutorial/main-expression.md b/web/packages/app/assets/tutorial/main-expression.md deleted file mode 100644 index 326efb33d..000000000 --- a/web/packages/app/assets/tutorial/main-expression.md +++ /dev/null @@ -1,11 +0,0 @@ -After all other data types, codata types, definitions and codefinitions an additional expression can be written. -This is called the "main" expression of the program. - -```pol -data Bool { True, False } -def Bool.neg { - True => False, - False => True, -} -True.neg -``` diff --git a/web/packages/app/assets/tutorial/typed-holes.md b/web/packages/app/assets/tutorial/typed-holes.md deleted file mode 100644 index 3076e9f07..000000000 --- a/web/packages/app/assets/tutorial/typed-holes.md +++ /dev/null @@ -1,10 +0,0 @@ -An incomplete program can be written using typed holes. -Typed holes are written using either `?`; they have type `?` which unifies with any other type. -For example, an incomplete implementation of boolean negation can be written as follows: - -```pol -def Bool.neg : Bool { - True => ?, - False => ?, -} -``` diff --git a/web/packages/app/src/tutorial/index.ts b/web/packages/app/src/tutorial/index.ts index 5af7457b3..95a2c5958 100644 --- a/web/packages/app/src/tutorial/index.ts +++ b/web/packages/app/src/tutorial/index.ts @@ -1,4 +1,4 @@ -import "../../assets/tutorial.css"; +import "../../assets/demo.css"; import * as highlight from "./highlight"; import * as editor from "./editor"; diff --git a/web/packages/app/webpack.config.js b/web/packages/app/webpack.config.js index f3df228e4..5b892340a 100644 --- a/web/packages/app/webpack.config.js +++ b/web/packages/app/webpack.config.js @@ -10,23 +10,11 @@ const Handlebars = require("handlebars"); const { marked } = require("marked"); const fs = require("fs"); -const loadMarkdown = () => { - const dir = fs.readdirSync("./assets/tutorial"); - const files = dir.filter((filename) => filename.endsWith(".md")).map((filename) => `./assets/tutorial/${filename}`); - let out = {}; - for (const filename of files) { - const content = fs.readFileSync(filename, "utf8"); - const html = marked.parse(content); - out[path.basename(filename, ".md")] = new Handlebars.SafeString(html); - } - return out; -}; - const loadExamples = () => { - const dir = fs.readdirSync("../../../oopsla_examples"); + const dir = fs.readdirSync("../../../examples"); const files = dir .filter((filename) => filename.endsWith(".pol")) - .map((filename) => `../../../oopsla_examples/${filename}`); + .map((filename) => `../../../examples/${filename}`); let out = []; for (const filename of files) { out.push(path.basename(filename, ".pol")); @@ -98,7 +86,7 @@ module.exports = (env, argv) => { preprocessor: (content, loaderContext) => { let result; - const input = Object.assign({}, loadMarkdown(), { examples: loadExamples() }); + const input = { examples: loadExamples() }; try { result = Handlebars.compile(content)(input); @@ -118,13 +106,13 @@ module.exports = (env, argv) => { new webpack.ProgressPlugin(), new CleanWebpackPlugin(), new CopyWebpackPlugin({ - patterns: [{ from: "../../../oopsla_examples", to: "examples" }], + patterns: [{ from: "../../../examples", to: "examples" }], }), new webpack.DefinePlugin({ DEBUG: !prod, }), new HtmlWebpackPlugin({ - template: "assets/tutorial.html", + template: "assets/demo.html", filename: "index.html", chunks: ["tutorial"], scriptLoading: "defer",