diff --git a/README.md b/README.md index d413ec3..e8236e5 100644 --- a/README.md +++ b/README.md @@ -524,21 +524,21 @@ Below is a table for all benchmark items as a quick reference. For language details: [SETUP.md](./SETUP.md) -| Benchmark | Typed Racket | TypeScript | Flow | mypy | Pyright | Sorbet | -|:------------------|:------------:|:----------:|:----:|:----:|:-------:|:------:| -| positive | O | O | O | O | O | O | -| negative | O | O | O | O | O | O | -| connectives | O | O | O | O | O | O | -| nesting_body | O | O | O | O | O | O | -| struct_fields | O | O | O | O | O | X | -| tuple_elements | O | O | O | O | O | O | -| tuple_length | x | O | O | O | O | X | -| alias | O | O | x | x | O | O | -| nesting_condition | O | x | x | x | x | O | -| merge_with_union | O | O | O | x | O | O | -| predicate_2way | O | O | O | O | O | X | -| predicate_1way | O | x | O | O | O | X | -| predicate_checked | O | O | O | O | O | X | +| Benchmark | Typed Racket | TypeScript | Flow | mypy | Pyright | Sorbet | Typed Clojure | +|:------------------|:------------:|:----------:|:----:|:----:|:-------:|:------:|:-------------:| +| positive | O | O | O | O | O | O | O | +| negative | O | O | O | O | O | O | O | +| connectives | O | O | O | O | O | O | O | +| nesting_body | O | O | O | O | O | O | O | +| struct_fields | O | O | O | O | O | X | O | +| tuple_elements | O | O | O | O | O | O | O | +| tuple_length | x | O | O | O | O | X | O | +| alias | O | O | x | x | O | O | O | +| nesting_condition | O | x | x | x | x | O | O | +| merge_with_union | O | O | O | x | O | O | O | +| predicate_2way | O | O | O | O | O | X | O | +| predicate_1way | O | x | O | O | O | X | O | +| predicate_checked | O | O | O | O | O | X | O | `O` means passed, `x` means not passed. @@ -547,12 +547,12 @@ For language details: [SETUP.md](./SETUP.md) [EXAMPLES.md](./EXAMPLES.md) contains more examples that are not included in the benchmark items. Those are real-world-like examples showing the use of type narrowing in various contexts. For more details about the examples, see [EXAMPLES.md](./EXAMPLES.md). For more details about the results, see the README.md file in the respective typechecker directories. The results of these examples are demonstrated below. -| Benchmark | Typed Racket | TypeScript | Flow | mypy | Pyright | Sorbet | -|:----------|:------------:|:----------:|:----:|:----:|:-------:|:------:| -| filter | O | O | O | O | O | O | -| flatten | O | O | O | O | O | O | -| tree_node | O | x | x | x | x | x | -| rainfall | O | O | O | O | O | O | +| Benchmark | Typed Racket | TypeScript | Flow | mypy | Pyright | Sorbet | Typed Clojure | +|:----------|:------------:|:----------:|:----:|:----:|:-------:|:------:|:-------------:| +| filter | O | O | O | O | O | O | O | +| flatten | O | O | O | O | O | O | O | +| tree_node | O | x | x | x | x | x | O | +| rainfall | O | O | O | O | O | O | O | ## Other Discussions diff --git a/typed-clojure/.gitignore b/typed-clojure/.gitignore new file mode 100644 index 0000000..d956ab0 --- /dev/null +++ b/typed-clojure/.gitignore @@ -0,0 +1,13 @@ +/target +/classes +/checkouts +profiles.clj +pom.xml +pom.xml.asc +*.jar +*.class +/.lein-* +/.nrepl-port +/.prepl-port +.hgignore +.hg/ diff --git a/typed-clojure/LICENSE b/typed-clojure/LICENSE new file mode 100644 index 0000000..2315126 --- /dev/null +++ b/typed-clojure/LICENSE @@ -0,0 +1,280 @@ +Eclipse Public License - v 2.0 + + THE ACCOMPANYING PROGRAM IS PROVIDED UNDER THE TERMS OF THIS ECLIPSE + PUBLIC LICENSE ("AGREEMENT"). ANY USE, REPRODUCTION OR DISTRIBUTION + OF THE PROGRAM CONSTITUTES RECIPIENT'S ACCEPTANCE OF THIS AGREEMENT. + +1. DEFINITIONS + +"Contribution" means: + + a) in the case of the initial Contributor, the initial content + Distributed under this Agreement, and + + b) in the case of each subsequent Contributor: + i) changes to the Program, and + ii) additions to the Program; + where such changes and/or additions to the Program originate from + and are Distributed by that particular Contributor. A Contribution + "originates" from a Contributor if it was added to the Program by + such Contributor itself or anyone acting on such Contributor's behalf. + Contributions do not include changes or additions to the Program that + are not Modified Works. + +"Contributor" means any person or entity that Distributes the Program. + +"Licensed Patents" mean patent claims licensable by a Contributor which +are necessarily infringed by the use or sale of its Contribution alone +or when combined with the Program. + +"Program" means the Contributions Distributed in accordance with this +Agreement. + +"Recipient" means anyone who receives the Program under this Agreement +or any Secondary License (as applicable), including Contributors. + +"Derivative Works" shall mean any work, whether in Source Code or other +form, that is based on (or derived from) the Program and for which the +editorial revisions, annotations, elaborations, or other modifications +represent, as a whole, an original work of authorship. + +"Modified Works" shall mean any work in Source Code or other form that +results from an addition to, deletion from, or modification of the +contents of the Program, including, for purposes of clarity any new file +in Source Code form that contains any contents of the Program. Modified +Works shall not include works that contain only declarations, +interfaces, types, classes, structures, or files of the Program solely +in each case in order to link to, bind by name, or subclass the Program +or Modified Works thereof. + +"Distribute" means the acts of a) distributing or b) making available +in any manner that enables the transfer of a copy. + +"Source Code" means the form of a Program preferred for making +modifications, including but not limited to software source code, +documentation source, and configuration files. + +"Secondary License" means either the GNU General Public License, +Version 2.0, or any later versions of that license, including any +exceptions or additional permissions as identified by the initial +Contributor. + +2. GRANT OF RIGHTS + + a) Subject to the terms of this Agreement, each Contributor hereby + grants Recipient a non-exclusive, worldwide, royalty-free copyright + license to reproduce, prepare Derivative Works of, publicly display, + publicly perform, Distribute and sublicense the Contribution of such + Contributor, if any, and such Derivative Works. + + b) Subject to the terms of this Agreement, each Contributor hereby + grants Recipient a non-exclusive, worldwide, royalty-free patent + license under Licensed Patents to make, use, sell, offer to sell, + import and otherwise transfer the Contribution of such Contributor, + if any, in Source Code or other form. This patent license shall + apply to the combination of the Contribution and the Program if, at + the time the Contribution is added by the Contributor, such addition + of the Contribution causes such combination to be covered by the + Licensed Patents. The patent license shall not apply to any other + combinations which include the Contribution. No hardware per se is + licensed hereunder. + + c) Recipient understands that although each Contributor grants the + licenses to its Contributions set forth herein, no assurances are + provided by any Contributor that the Program does not infringe the + patent or other intellectual property rights of any other entity. + Each Contributor disclaims any liability to Recipient for claims + brought by any other entity based on infringement of intellectual + property rights or otherwise. As a condition to exercising the + rights and licenses granted hereunder, each Recipient hereby + assumes sole responsibility to secure any other intellectual + property rights needed, if any. For example, if a third party + patent license is required to allow Recipient to Distribute the + Program, it is Recipient's responsibility to acquire that license + before distributing the Program. + + d) Each Contributor represents that to its knowledge it has + sufficient copyright rights in its Contribution, if any, to grant + the copyright license set forth in this Agreement. + + e) Notwithstanding the terms of any Secondary License, no + Contributor makes additional grants to any Recipient (other than + those set forth in this Agreement) as a result of such Recipient's + receipt of the Program under the terms of a Secondary License + (if permitted under the terms of Section 3). + +3. REQUIREMENTS + +3.1 If a Contributor Distributes the Program in any form, then: + + a) the Program must also be made available as Source Code, in + accordance with section 3.2, and the Contributor must accompany + the Program with a statement that the Source Code for the Program + is available under this Agreement, and informs Recipients how to + obtain it in a reasonable manner on or through a medium customarily + used for software exchange; and + + b) the Contributor may Distribute the Program under a license + different than this Agreement, provided that such license: + i) effectively disclaims on behalf of all other Contributors all + warranties and conditions, express and implied, including + warranties or conditions of title and non-infringement, and + implied warranties or conditions of merchantability and fitness + for a particular purpose; + + ii) effectively excludes on behalf of all other Contributors all + liability for damages, including direct, indirect, special, + incidental and consequential damages, such as lost profits; + + iii) does not attempt to limit or alter the recipients' rights + in the Source Code under section 3.2; and + + iv) requires any subsequent distribution of the Program by any + party to be under a license that satisfies the requirements + of this section 3. + +3.2 When the Program is Distributed as Source Code: + + a) it must be made available under this Agreement, or if the + Program (i) is combined with other material in a separate file or + files made available under a Secondary License, and (ii) the initial + Contributor attached to the Source Code the notice described in + Exhibit A of this Agreement, then the Program may be made available + under the terms of such Secondary Licenses, and + + b) a copy of this Agreement must be included with each copy of + the Program. + +3.3 Contributors may not remove or alter any copyright, patent, +trademark, attribution notices, disclaimers of warranty, or limitations +of liability ("notices") contained within the Program from any copy of +the Program which they Distribute, provided that Contributors may add +their own appropriate notices. + +4. COMMERCIAL DISTRIBUTION + +Commercial distributors of software may accept certain responsibilities +with respect to end users, business partners and the like. While this +license is intended to facilitate the commercial use of the Program, +the Contributor who includes the Program in a commercial product +offering should do so in a manner which does not create potential +liability for other Contributors. Therefore, if a Contributor includes +the Program in a commercial product offering, such Contributor +("Commercial Contributor") hereby agrees to defend and indemnify every +other Contributor ("Indemnified Contributor") against any losses, +damages and costs (collectively "Losses") arising from claims, lawsuits +and other legal actions brought by a third party against the Indemnified +Contributor to the extent caused by the acts or omissions of such +Commercial Contributor in connection with its distribution of the Program +in a commercial product offering. The obligations in this section do not +apply to any claims or Losses relating to any actual or alleged +intellectual property infringement. In order to qualify, an Indemnified +Contributor must: a) promptly notify the Commercial Contributor in +writing of such claim, and b) allow the Commercial Contributor to control, +and cooperate with the Commercial Contributor in, the defense and any +related settlement negotiations. The Indemnified Contributor may +participate in any such claim at its own expense. + +For example, a Contributor might include the Program in a commercial +product offering, Product X. That Contributor is then a Commercial +Contributor. If that Commercial Contributor then makes performance +claims, or offers warranties related to Product X, those performance +claims and warranties are such Commercial Contributor's responsibility +alone. Under this section, the Commercial Contributor would have to +defend claims against the other Contributors related to those performance +claims and warranties, and if a court requires any other Contributor to +pay any damages as a result, the Commercial Contributor must pay +those damages. + +5. NO WARRANTY + +EXCEPT AS EXPRESSLY SET FORTH IN THIS AGREEMENT, AND TO THE EXTENT +PERMITTED BY APPLICABLE LAW, THE PROGRAM IS PROVIDED ON AN "AS IS" +BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, EITHER EXPRESS OR +IMPLIED INCLUDING, WITHOUT LIMITATION, ANY WARRANTIES OR CONDITIONS OF +TITLE, NON-INFRINGEMENT, MERCHANTABILITY OR FITNESS FOR A PARTICULAR +PURPOSE. Each Recipient is solely responsible for determining the +appropriateness of using and distributing the Program and assumes all +risks associated with its exercise of rights under this Agreement, +including but not limited to the risks and costs of program errors, +compliance with applicable laws, damage to or loss of data, programs +or equipment, and unavailability or interruption of operations. + +6. DISCLAIMER OF LIABILITY + +EXCEPT AS EXPRESSLY SET FORTH IN THIS AGREEMENT, AND TO THE EXTENT +PERMITTED BY APPLICABLE LAW, NEITHER RECIPIENT NOR ANY CONTRIBUTORS +SHALL HAVE ANY LIABILITY FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING WITHOUT LIMITATION LOST +PROFITS), HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN +CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) +ARISING IN ANY WAY OUT OF THE USE OR DISTRIBUTION OF THE PROGRAM OR THE +EXERCISE OF ANY RIGHTS GRANTED HEREUNDER, EVEN IF ADVISED OF THE +POSSIBILITY OF SUCH DAMAGES. + +7. GENERAL + +If any provision of this Agreement is invalid or unenforceable under +applicable law, it shall not affect the validity or enforceability of +the remainder of the terms of this Agreement, and without further +action by the parties hereto, such provision shall be reformed to the +minimum extent necessary to make such provision valid and enforceable. + +If Recipient institutes patent litigation against any entity +(including a cross-claim or counterclaim in a lawsuit) alleging that the +Program itself (excluding combinations of the Program with other software +or hardware) infringes such Recipient's patent(s), then such Recipient's +rights granted under Section 2(b) shall terminate as of the date such +litigation is filed. + +All Recipient's rights under this Agreement shall terminate if it +fails to comply with any of the material terms or conditions of this +Agreement and does not cure such failure in a reasonable period of +time after becoming aware of such noncompliance. If all Recipient's +rights under this Agreement terminate, Recipient agrees to cease use +and distribution of the Program as soon as reasonably practicable. +However, Recipient's obligations under this Agreement and any licenses +granted by Recipient relating to the Program shall continue and survive. + +Everyone is permitted to copy and distribute copies of this Agreement, +but in order to avoid inconsistency the Agreement is copyrighted and +may only be modified in the following manner. The Agreement Steward +reserves the right to publish new versions (including revisions) of +this Agreement from time to time. No one other than the Agreement +Steward has the right to modify this Agreement. The Eclipse Foundation +is the initial Agreement Steward. The Eclipse Foundation may assign the +responsibility to serve as the Agreement Steward to a suitable separate +entity. Each new version of the Agreement will be given a distinguishing +version number. The Program (including Contributions) may always be +Distributed subject to the version of the Agreement under which it was +received. In addition, after a new version of the Agreement is published, +Contributor may elect to Distribute the Program (including its +Contributions) under the new version. + +Except as expressly stated in Sections 2(a) and 2(b) above, Recipient +receives no rights or licenses to the intellectual property of any +Contributor under this Agreement, whether expressly, by implication, +estoppel or otherwise. All rights in the Program not expressly granted +under this Agreement are reserved. Nothing in this Agreement is intended +to be enforceable by any entity that is not a Contributor or Recipient. +No third-party beneficiary rights are created under this Agreement. + +Exhibit A - Form of Secondary Licenses Notice + +"This Source Code may also be made available under the following +Secondary Licenses when the conditions for such availability set forth +in the Eclipse Public License, v. 2.0 are satisfied: GNU General Public +License as published by the Free Software Foundation, either version 2 +of the License, or (at your option) any later version, with the GNU +Classpath Exception which is available at +https://www.gnu.org/software/classpath/license.html." + + Simply including a copy of this Agreement, including this Exhibit A + is not sufficient to license the Source Code under Secondary Licenses. + + If it is not possible or desirable to put the notice in a particular + file, then You may include the notice in a location (such as a LICENSE + file in a relevant directory) where a recipient would be likely to + look for such a notice. + + You may add additional accurate notices of copyright ownership. diff --git a/typed-clojure/README.md b/typed-clojure/README.md new file mode 100644 index 0000000..42795a0 --- /dev/null +++ b/typed-clojure/README.md @@ -0,0 +1,149 @@ +Typed Clojure +=== + +Typed Clojure is a gradual type system for Clojure, providing static type checking for a dynamically typed language. + +* Language resources: + - + - +* If-T version: **1.0** +* Implementation: [./main.clj](./main.clj), [./examples.clj](./examples.clj) +* Raw command to run the benchmark: `clj -M:typed/check ` + +#### Type System Basics + +> Q. What is the top type in this language? What is the bottom type? What is the dynamic type? If these types do not exist, explain the alternatives. + +* **Top**: `t/Any` — Represents any possible value in Clojure, analogous to Clojure's dynamic typing. +* **Bottom**: `t/Nothing` — Represents the absence of any value (uninhabited type), used for functions that never return or always throw. +* **Dynamic**: `t/Any` — Serves as the dynamic type, allowing any value without type checking restrictions, effectively disabling static type checking for that expression. + +Typed Clojure uses `t/Any` for both top and dynamic types, as Clojure's dynamic nature means most untyped code implicitly operates at this level. `t/Nothing` is rarely used explicitly but exists for type system completeness. + +> Q. What base types does this implementation use? Why? + +* `t/Str` (String) +* `t/Num` (Number, including integers and floating-point) +* `t/Bool` (Boolean) +* `t/Int` (Integer, a subtype of `t/Num`) +* `t/Double` (Double-precision floating-point, a subtype of `t/Num`) + +These types correspond to Clojure's core data types, which are immutable and commonly used in functional programming. They are chosen to align with Clojure's runtime type system, enabling precise type narrowing for common predicates like `string?`, `number?`, and `boolean?`. + +> Q. What container types does this implementation use (for objects, tuples, etc)? Why? + +* **Objects**: `t/HMap` (Heterogeneous Map) — Represents maps with specific keys and value types, e.g., `(t/HMap :mandatory {:a (t/U nil Number)} :complete? true)`. Used for struct-like data with known fields. +* **Tuples**: `t/NonEmptyVec` (Non-empty Vector) and `t/Vec` (Vector) — Represent sequences with specific element types, used for tuple-like structures. Vectors are Clojure's primary sequence type, and `t/NonEmptyVec` ensures at least one element. +* **Sequences**: `t/Seqable` — Represents any sequence (lists, vectors, etc.), used for recursive structures like trees. + +These types reflect Clojure's immutable data structures, which are central to its functional paradigm. `t/HMap` is used for structs because Clojure maps are commonly used for key-value data. Vectors are used for tuples due to their indexed access and immutability, which supports type narrowing on elements. + +#### Type Narrowing + +> Q. How do simple type tests work in this language? + +Type tests in Typed Clojure use Clojure's built-in predicates like `string?`, `number?`, `boolean?`, etc., which return a boolean indicating whether a value matches a type. These predicates are recognized by Typed Clojure's occurrence typing system, which refines the type of a variable based on the predicate's result in conditional branches. + +Example: +```clojure +(if (string? x) + (count x) ; x is refined to t/Str + x) ; x is refined to (t/I t/Any (t/Not t/Str)) +``` + +> Q. Are there other forms of type test? If so, explain. + +Typed Clojure supports custom predicates via annotations like `(t/Pred Type)` and filter annotations (`:filters {:then ... :else ...}`). These allow user-defined functions to act as type tests, refining types in both positive (`:then`) and negative (`:else`) branches. + +Example: +```clojure +(t/ann my-pred [(t/U t/Str t/Num) -> t/Bool :filters {:then (is t/Str 0) :else (! t/Str 0)}]) +(defn my-pred [x] (string? x)) +``` + +Additionally, Typed Clojure supports structural checks (e.g., `vector?`, `map?`) and length checks (e.g., `count`) for refining sequence types, as seen in `tuple_length`. + +> Q. How do type casts work in this language? + +Type casts in Typed Clojure are performed using `t/ann-form`, which asserts that an expression has a specific type. Unlike dynamic casts, `t/ann-form` is purely for the type checker and does not affect runtime behavior. If the asserted type is incorrect, the type checker will flag an error if it can detect the mismatch. + +Example: +```clojure +(t/ann-form x t/Num) ; Asserts x is a t/Num +``` + +> Q. What is the syntax for a symmetric (2-way) type-narrowing predicate? + +Symmetric predicates use the `:filters` annotation with `:then` and `:else` clauses to specify type refinements for both branches. + +Example: +```clojure +(t/ann predicate-2way-success-f [(t/U t/Str t/Num) -> t/Bool + :filters {:then (is t/Str 0) :else (! t/Str 0)}]) +(defn predicate-2way-success-f [x] + (string? x)) +``` +Here, `:then (is t/Str 0)` refines `x` to `t/Str` when the predicate is true, and `:else (! t/Str 0)` refines `x` to `(t/Not t/Str)` (i.e., `t/Num`) when false. + +> Q. If the language supports other type-narrowing predicates, describe them below. + +Typed Clojure supports 1-way predicates, which refine types only in the positive (`:then`) branch, leaving the negative branch unrefined. This is useful for underapproximations, like checking if a number is positive. + +Example: +```clojure +(t/ann predicate-1way-success-f [(t/U t/Str t/Num) -> t/Bool :filters {:then (is t/Num 0)}]) +(defn predicate-1way-success-f [x] + (and (number? x) (> x 0))) +``` + +#### Benchmark Details + +> Q. Are any benchmarks inexpressible? Why? + +All benchmarks are expressible in Typed Clojure, as shown in `main.clj`. The language's flexible type system, based on occurrence typing and union types, supports all the required constructs (e.g., `positive`, `negative`, `connectives`, etc.). The implementation closely mirrors the pseudocode in `readme.md`. + +> Q. Are any benchmarks expressed particularly well, or particularly poorly? Explain. + +Expressed Well: +- `positive`, `negative`, `connectives`: These are straightforward, as Typed Clojure's occurrence typing directly supports refining types based on predicates like `string?` and logical connectives (`and`, `or`, `not`). The syntax is concise and aligns with Clojure's functional style. +- `predicate_2way`, `predicate_1way`, `predicate_checked`: Typed Clojure's `:filters` annotation is designed for custom predicates, making these benchmarks natural to express. The explicit `:then` and `:else` filters clearly specify type refinements. +- `struct_fields`, `tuple_elements`: `t/HMap` and `t/NonEmptyVec` map well to Clojure's map and vector data structures, allowing precise type narrowing on fields and elements. + +Expressed Poorly: +- `tuple_length`: While expressible, length-based narrowing requires explicit checks with count, and the type system must infer the correct tuple type from a union. This can feel verbose compared to languages with native tuple length types (e.g., TypeScript's tuple types). +- `nesting_condition`: Nested conditionals are supported, but the syntax can become complex when combining multiple predicates, requiring careful annotation to ensure type refinements propagate correctly. + +> Q. How direct (or complex) is the implementation compared to the pseudocode from If-T? + +The implementation in `main.clj` is very direct compared to the pseudocode in `readme.md`. Typed Clojure's syntax for predicates, conditionals, and type annotations closely mirrors the pseudocode's structure. For example: + +- `positive` maps directly to `if` with `string?` checks and `count` operations. +- `merge_with-union` uses Clojure's `cond` to express multiple branches, aligning with the pseudocode's `if-else` chains. +- Custom predicates use `:filters`, which are a natural extension of the pseudocode's `x is T` syntax. + +The main complexity arises in verbose annotations for complex types (e.g., `t/HMap`, `t/NonEmptyVec`), but these are necessary for precision and do not deviate significantly from the pseudocode's intent. + +#### Advanced Examples + +> Q. Are any examples inexpressible? Why? + +All examples in `examples.clj` are expressible. + +> Q. Are any examples expressed particularly well, or particularly poorly? Explain. + +Expressed Well: +- `filter`: The filter-success function uses filterv, which is idiomatic in Clojure and aligns with the type annotation `(t/All [A] [(t/Vec A) [A :-> t/Bool] :-> (t/Vec A)])`. The type variable A ensures genericity, and the implementation is concise. +- flatten: The recursive `flatten-success` function leverages Clojure's sequence operations (`first`, `next`, `into`) and type annotations (`t/Seqable`, `t/Ve`c) to clearly express the tree-to-vector transformation. The use of `t/ann-form` for type assertions in base cases is natural. +- rainfall: The rainfall-success function uses a typed loop (`t/loop`) to process weather reports, with clear annotations for `t/Double` and `t/Long`. The implementation closely follows Clojure's functional style, making it idiomatic and precise. + +Expressed Poorly: +- The `tree-node-success?` and `tree-node-failure?` functions highlight a key weakness in how Typed Clojure handles predicate functions over recursive types. While the type alias is well-defined, the predicate logic — which checks structure via `vector?`, `count`, `number?`, and `sequential?` — operates at runtime and is not validated by the type system for correctness. + +> Q. How direct (or complex) is the implementation compared to the pseudocode from If-T? + +The implementations in examples.clj are direct but slightly more verbose due to explicit type annotations. For example: + +- `filter` maps directly to the pseudocode's filtering logic but requires a polymorphic type annotation `(t/All [A] ...)`. +- `flatten` follows the pseudocode's recursive structure but needs `t/ann-form` for base cases to assert types like `IntVector`. +- `rainfall` aligns closely with the pseudocode but includes additional checks (e.g., `map?`, `not (nil? day)`) to handle Clojure's dynamic nature, making it slightly more complex. +- `tree_node` function is a direct and faithful implementation of a structural predicate for a recursive tree type. It checks that the node is a vector of length 2, the first element is a number, and the second is a sequence of valid `TreeNodes` — exactly as specified. The recursive validation via every? mirrors the expected inductive definition. diff --git a/typed-clojure/_benchmark.rkt b/typed-clojure/_benchmark.rkt new file mode 100644 index 0000000..595f981 --- /dev/null +++ b/typed-clojure/_benchmark.rkt @@ -0,0 +1,41 @@ +#lang racket + +(require racket/cmdline) +(require "../lib.rkt") + +(define current-typechecker-symbol 'Typed Clojure) +(define current-typechecker-name "Typed Clojure") + +(define typechecker-parameters + `((name ,current-typechecker-name) + (comment-char #\;) + (extension ".clj") + (file-base-path ,(current-directory)) + (examples-file-base-path ,(current-directory)) + (arguments ,(list "src/typed_clojure/main.clj" "")) + (examples-arguments ,(list "src/typed_clojure/examples.clj" "")) + (command "npx"))) + +(command-line + #:program "_benchmark.rkt" + #:once-each + [("-v" "--verbose") "Print the output of the benchmarks to the console" + (benchmark-verbose #t)] + [("-f" "--format") output-format "Print the output of the benchmarks in the specified format. Options: plain, markdown, tex. Default: plain." + (benchmark-output-format (string->symbol output-format))] + [("-t" "--transpose") "Transpose the output of the benchmarks" + (benchmark-output-transposed #t)] + [("-e" "--examples") "Run the advanced examples" + (benchmark-run-examples #t)] + #:args () + (void)) + +(define benchmark-data (execute-benchmark-for-one-typechecker typechecker-parameters)) +(define benchmark-result-for-printing (list (cons current-typechecker-name benchmark-data))) + +(define actual-test-names (map car benchmark-data)) +(define header-row (cons "Benchmark" actual-test-names)) + +(print-benchmark benchmark-result-for-printing + (benchmark-output-format) + header-row) diff --git a/typed-clojure/project.clj b/typed-clojure/project.clj new file mode 100644 index 0000000..74288aa --- /dev/null +++ b/typed-clojure/project.clj @@ -0,0 +1,12 @@ +(defproject typed-clojure-benchmark "0.1.0-SNAPSHOT" + :description "Typed Clojure benchmark" + :dependencies [[org.clojure/clojure "1.11.1"] + [org.typedclojure/typed.clj.runtime "1.2.0"]] + :profiles {:dev {:dependencies [[org.typedclojure/typed.clj.checker "1.2.0"] + [nrepl/nrepl "1.0.0"]]}} + :plugins [[lein-exec "0.3.7"]] + :main ^:skip-aot typed-clojure.main + :target-path "target/%s" + :source-paths ["src"] + :test-paths ["test"] + :repl-options {:init-ns typed-clojure.main}) diff --git a/typed-clojure/src/typed_clojure/examples.clj b/typed-clojure/src/typed_clojure/examples.clj new file mode 100644 index 0000000..5f3d960 --- /dev/null +++ b/typed-clojure/src/typed_clojure/examples.clj @@ -0,0 +1,125 @@ +(ns typed-clojure.examples + (:require [typed.clojure :as t]) + (:gen-class)) + +;;; Code: +;; Example filter +;; success +(t/ann filter-success (t/All [A] [(t/Vec A) [A :-> t/Bool] :-> (t/Vec A)])) +(defn filter-success [array pred] + (filterv pred array)) + +;; failure +(t/ann filter-failure (t/All [A] [(t/Vec A) [A :-> t/Bool] :-> (t/Vec A)])) +(defn filter-failure [array pred] + (t/ann-form + (vec (for [value array] + (if (pred value) + value + "string"))) ; Type error: "string" doesn't match (t/Vec t/Num) + (t/Vec t/Num))) + +;; Example flatten +;; success +(t/defalias IntTree + (t/U Integer (t/Seqable IntTree))) +(t/defalias IntVector + (t/Vec Integer)) +(t/ann flatten-success [IntTree -> IntVector]) +(defn flatten-success [l] + (if (sequential? l) + (if (empty? l) + (t/ann-form [] IntVector) + (let [first-part (flatten-success (first l)) + rest-parts (flatten-success (next l))] + (into first-part rest-parts))) + (do + (assert (and (integer? l) (instance? Integer l)) "Expected an Integer in non-sequential case") + (t/ann-form [(t/ann-form l Integer)] IntVector)))) + +;; failure +(t/ann flatten-failure [IntTree -> IntVector]) +(defn flatten-failure [l] + (if (sequential? l) + (if (empty? l) + (t/ann-form [] IntVector) + (let [first-part (flatten-success (first l)) + rest-parts (flatten-success (next l))] + (into first-part rest-parts))) + (t/ann-form l Integer))) ; Expected error: Expected IntVector but found Integer + +;; Example tree_node +;; success +(t/defalias TreeNode + (t/HVec [t/Num (t/Seqable TreeNode)])) +(t/ann tree-node-success? [t/Any -> t/Bool]) +(defn tree-node-success? [node] + (and (vector? node) + (= (count node) 2) + (number? (nth node 0)) + (sequential? (nth node 1)))) + +;; failure +(t/ann tree-node-failure? [t/Any -> t/Bool]) +(defn tree-node-failure? [node] + (and (vector? node) + (= (count node) 2) + (number? (nth node 0)) + (sequential? (nth node 1)) + "false")) ; Expected error: Expected Boolean, Actual (t/Val "false") + +;; Example rainfall +;; success +(t/defalias DayReport + (t/Map t/Keyword (t/U nil Double))) +(t/defalias WeatherReport + (t/Seqable DayReport)) +(t/defalias ValidRainfall + (t/U nil Double)) +(t/defalias RainfallResult Double) +(t/ann rainfall-success [WeatherReport -> RainfallResult]) +(defn rainfall-success [weather-reports] + (t/loop [reports :- WeatherReport, weather-reports + total :- Double, 0.0 + count :- Long, (t/ann-form 0 Long)] + (if (empty? reports) + (if (> count 0) + (double (/ total count)) + 0.0) + (let [day (first reports)] + (if (and (map? day) (not (nil? day))) + (let [val (t/ann-form (get day :rainfall) (t/U nil Double))] + (if (and val (double? val)) + (let [val-d val] + (if (<= 0.0 val-d 999.0) + (recur (rest reports) + (+ total val-d) + (t/ann-form (inc count) Long)) + (recur (rest reports) total count))) + (recur (rest reports) total count))) + (recur (rest reports) total count)))))) + +;; failure +(t/defalias DayReport + (t/Map t/Keyword (t/U nil Double))) +(t/defalias WeatherReport + (t/Seqable DayReport)) +(t/defalias RainfallResult Double) +(t/ann rainfall-failure [WeatherReport -> RainfallResult]) +(defn rainfall-failure [weather-reports] + (t/loop [reports :- WeatherReport, weather-reports + total :- Double, 0.0 + count :- Long, (t/ann-form 0 Long)] + (if (empty? reports) + (if (> count 0) + (double (/ total count)) + 0.0) + (let [day (first reports)] + (if (and (map? day) (not (nil? day))) + (let [val (t/ann-form (get day :rainfall) String)] + (if (not (nil? val)) + (recur (rest reports) + (t/ann-form (+ total val) Double) ; Type error: Adding String to Double + (t/ann-form (inc count) Long)) + (recur (rest reports) total count))) + (recur (rest reports) total count)))))) diff --git a/typed-clojure/src/typed_clojure/main.clj b/typed-clojure/src/typed_clojure/main.clj new file mode 100644 index 0000000..881678a --- /dev/null +++ b/typed-clojure/src/typed_clojure/main.clj @@ -0,0 +1,281 @@ +(ns typed-clojure.main + (:require [typed.clojure :as t]) + (:gen-class)) + +;;; Code: +;; Example positive +;; success +(t/ann positive-success-f [t/Any :-> (t/U t/Int t/Any)]) +(defn positive-success-f [x] + (if (string? x) + (count x) + x)) + +;; failure +(t/ann positive-failure-f [t/Any :-> (t/U t/Int t/Any)]) +(defn positive-failure-f [x] + (if (string? x) + (t/ann-form (.isNaN x) t/Num) ; Type error: strings don't have .isNaN + x)) + +;; Example negative +;; success +(t/ann negative-success-f [(t/U t/Str t/Num) :-> t/Num]) +(defn negative-success-f [x] + (if (string? x) + (count x) + (+ x 1))) + +;; failure +(t/ann negative-failure-f [(t/U t/Str t/Num t/Bool) :-> t/Num]) +(defn negative-failure-f [x] + (if (string? x) + (count x) + (t/ann-form (+ x 1) t/Num))) ; Type error: x could be boolean + +;; Example connectives +;; success +(t/ann connectives-success-f [(t/U t/Str t/Num) :-> t/Num]) +(defn connectives-success-f [x] + (if (not (number? x)) + (count x) + 0)) + +(t/ann connectives-success-g [t/Any :-> t/Num]) +(defn connectives-success-g [x] + (if (or (string? x) (number? x)) + (connectives-success-f x) + 0)) + +(t/ann connectives-success-h [(t/U t/Str t/Num t/Bool) :-> t/Num]) +(defn connectives-success-h [x] + (if (and (not (boolean? x)) (not (number? x))) + (count x) + 0)) + +;; failure +(t/ann connectives-failure-f [(t/U t/Str t/Num) :-> t/Num]) +(defn connectives-failure-f [x] + (if (not (number? x)) + (t/ann-form (+ x 1) t/Num) ; Type error: x could be string + 0)) + +(t/ann connectives-failure-g [t/Any :-> t/Num]) +(defn connectives-failure-g [x] + (if (or (string? x) (number? x)) + (t/ann-form (+ x 1) t/Num) ; Type error: x could be string + 0)) + +(t/ann connectives-failure-h [(t/U t/Str t/Num t/Bool) :-> t/Num]) +(defn connectives-failure-h [x] + (if (and (not (boolean? x)) (not (number? x))) + (t/ann-form (+ x 1) t/Num) ; Type error: x is string + 0)) + +;; Example nesting_body +;; success +(t/ann nesting-body-success-f [(t/U t/Str t/Num t/Bool) :-> t/Num]) +(defn nesting-body-success-f [x] + (if (not (string? x)) + (if (not (boolean? x)) + (+ x 1) + 0) + 0)) + +;; failure +(t/ann nesting-body-failure-f [(t/U t/Str t/Num t/Bool) :-> t/Num]) +(defn nesting-body-failure-f [x] + (if (or (string? x) (number? x)) + (if (or (number? x) (boolean? x)) + (t/ann-form (count x) t/Num) ; Type error: x could be number + 0) + 0)) + +;; Example struct_fields +;; success +(t/defalias MyStruct + (t/HMap :mandatory {:a (t/U nil Number)} + :complete? true)) +(t/ann struct-fields-success-f [MyStruct -> t/Num]) +(defn struct-fields-success-f [x] + (if (number? (:a x)) + (:a x) + 0)) + +;; failure +(t/defalias MyStruct + (t/HMap :mandatory {:a (t/U nil Number)} + :complete? true)) +(t/ann struct-fields-failure-f [MyStruct -> t/Num]) +(defn struct-fields-failure-f [x] + (if (string? (:a x)) + (t/ann-form (:a x) t/Num) ; Error: can't cast string to Num + 0)) + +;; Example tuple_elements +;; success +(t/ann tuple-elements-success-f [(t/NonEmptyVec (t/U nil t/Num)) :-> t/Num]) +(defn tuple-elements-success-f [x] + (let [first-elem (nth x 0)] + (if (number? first-elem) + first-elem + 0))) + +;; failure +(t/ann tuple-elements-failure-f [(t/NonEmptyVec (t/U nil t/Num)) :-> t/Num]) +(defn tuple-elements-failure-f [x] + (if (number? (nth x 0)) + (+ (nth x 0) (nth x 1)) ; Type error: (nth x 1) could be non-number + 0)) + +;; Example tuple_length +;; success +(t/ann tuple-length-success-f [(t/NonEmptyVec t/Num) :-> t/Num]) +(defn tuple-length-success-f [x] + (if (= (count x) 2) + (let [first-elem (nth x 0) + second-elem (nth x 1)] + (+ first-elem second-elem)) + 0)) + +;; failure +(t/ann tuple-length-failure-f [(t/U (t/NonEmptyVec t/Num) (t/NonEmptyVec t/Str)) :-> t/Num]) +(defn tuple-length-failure-f [x] + (if (= (count x) 2) + (+ (nth x 0) (nth x 1)) + (+ (nth x 0) (nth x 1)))) ; Type error: with expected type: t/Num + +;; Example alias +;; success +(t/ann alias-success-f [t/Any :-> (t/U t/Int t/Any)]) +(defn alias-success-f [x] + (let [y (string? x)] + (if y + (count x) + x))) + +;; failure +(t/ann alias-failure-f [t/Any :-> (t/U t/Int t/Any)]) +(defn alias-failure-f [x] + (let [y (string? x)] + (if y + (t/ann-form (.isNaN x) t/Num) ; Type error: strings don't have .isNaN + x))) + +(t/ann alias-failure-g [t/Any :-> (t/U t/Int t/Any)]) +(defn alias-failure-g [x] + (let [y true] ; Overwrites type check + (if y + (t/ann-form (count x) t/Any) ; Type error: x could be any type + x))) + +;; Example nesting_condition +;; success +(t/ann nesting-condition-success-f [t/Any t/Any :-> t/Num]) +(defn nesting-condition-success-f [x y] + (if (if (number? x) (string? y) false) + (+ x (count y)) + 0)) + +;; failure +(t/ann nesting-condition-failure-f [t/Any t/Any :-> t/Num]) +(defn nesting-condition-failure-f [x y] + (if (if (number? x) (string? y) (string? y)) + (t/ann-form (+ x (count y)) t/Num) ; Type error: x could be non-number + 0)) + +;; Example merge_with_union +;; success +(t/ann merge-with-union-success-f [t/Any :-> (t/U t/Str t/Num t/Any)]) +(defn merge-with-union-success-f [x] + (let [result (cond + (string? x) (str x "hello") + (number? x) (+ x 1) + :else x)] + result)) + +;; failure +(t/ann merge-with-union-failure-f [t/Any :-> (t/U t/Str t/Num t/Any)]) +(defn merge-with-union-failure-f [x] + (let [result (cond + (string? x) (str x "hello") + (number? x) (+ x 1) + :else x)] + (t/ann-form (.isNaN result) t/Bool))) ; Type error: result could be string + +;; Example predicate_2way +;; success +(t/ann predicate-2way-success-f [(t/U t/Str t/Num) -> t/Bool + :filters {:then (is t/Str 0) + :else (! t/Str 0)}]) +(defn predicate-2way-success-f [x] + (string? x)) + +(t/ann predicate-2way-success-g [(t/U t/Str t/Num) -> t/Num]) +(defn predicate-2way-success-g [x] + (if (predicate-2way-success-f x) + (count x) + x)) + +;; failure +(t/ann predicate-2way-failure-f [(t/U t/Str t/Num) -> t/Bool + :filters {:then (is t/Str 0)}]) +(defn predicate-2way-failure-f [x] + (string? x)) + +(t/ann predicate-2way-failure-g [(t/U t/Str t/Num) -> t/Num]) +(defn predicate-2way-failure-g [x] + (if (predicate-2way-failure-f x) + (t/ann-form (+ x 1) t/Num) ; Type Error: x is string! + x)) + +;; Example predicate_1way +;; success +(t/ann predicate-1way-success-f [(t/U t/Str t/Num) -> t/Bool + :filters {:then (is t/Num 0)}]) +(defn predicate-1way-success-f [x] + (and (number? x) (> x 0))) + +(t/ann predicate-1way-success-g [(t/U t/Str t/Num) -> t/Num]) +(defn predicate-1way-success-g [x] + (if (predicate-1way-success-f x) + (+ x 1) + 0)) + +;; failure +(t/ann predicate-1way-failure-f [(t/U t/Str t/Num) -> t/Bool + :filters {:then (is t/Num 0)}]) +(defn predicate-1way-failure-f [x] + (and (number? x) (> x 0))) + +(t/ann predicate-1way-failure-g [(t/U t/Str t/Num) -> t/Num]) +(defn predicate-1way-failure-g [x] + (if (predicate-1way-failure-f x) + (+ x 1) + (t/ann-form (count x) t/Num))) ; Error: x could still be number (not ruled out) + +;; Example predicate_checked +;; success +(t/ann predicate-checked-success-f [(t/U t/Str t/Num t/Bool) -> t/Bool + :filters {:then (is t/Str 0) + :else (! t/Str 0)}]) +(defn predicate-checked-success-f [x] + (string? x)) + +(t/ann predicate-checked-success-g [(t/U t/Str t/Num t/Bool) -> t/Bool + :filters {:then (! t/Str 0) + :else (is t/Str 0)}]) +(defn predicate-checked-success-g [x] + (not (predicate-checked-success-f x))) + +;; failure +(t/ann predicate-checked-failure-f [(t/U t/Str t/Num t/Bool) -> t/Bool + :filters {:then (or (is t/Str 0) (is t/Num 0)) + :else (and (! t/Str 0) (! t/Num 0))}]) +(defn predicate-checked-failure-f [x] + (or (string? x) (number? x))) + +(t/ann predicate-checked-failure-g [(t/U t/Str t/Num t/Bool) -> t/Bool + :filters {:then (is t/Num 0)}]) +(defn predicate-checked-failure-g [x] + (number? x))