-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
3 changed files
with
7 additions
and
8 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1 +1 @@ | ||
| ((3) 0 () 8 ((u . "") (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-06-28-gtp-benchmarks.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-02-02-luau-telemetry.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-04-21-forge.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-07-07-ltlf.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2023-06-26-flowfpx-juliacon.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2023-10-31-conceptual-mutant-testing.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2023-09-19-generating-programs-trivially.md" . unix)) () (h ! (equal) ((p+ #"/Users/ben/code/uu/blog/_src/posts/2024-04-21-forge.md" . unix) f post (u . "[Forge: A Tool to Teach Formal Methods](https://blog.brownplt.org/2024/04/21/forge.html)") (? . 3) 1719613724 (p+ #"/Users/ben/code/uu/blog/2024/04/-forge-a-tool-to-teach-formal-methods-https-blog-brownplt-org-2024-04-21-forge-html.html" . unix) (u . "/2024/04/-forge-a-tool-to-teach-formal-methods-https-blog-brownplt-org-2024-04-21-forge-html.html") (u . "2024-04-21T01:11:11") (? . 2) (? . 4) () (? . 0) #f (? . 0)) ((? . 1) f post (u . "GTP Benchmarks for Gradual Typing Performance") (? . 1) 1720844960 (p+ #"/Users/ben/code/uu/blog/2023/06/gtp-benchmarks-for-gradual-typing-performance.html" . unix) (u . "/2023/06/gtp-benchmarks-for-gradual-typing-performance.html") (u . "2023-06-28T17:18:44") #f (? . 7) (c (u . "by Ben Greenman")) (u . "\n<p>Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.</p>") #t (u . "\n<p>Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.</p>\n<!-- more-->\n\n<hr />\n\n<p>What on earth is gradual typing performance and why does it matter?</p>\n\n<p>The second question is easy to answer: performance matters because the cost of gradual types can slow a program by several <a href=\"https://users.cs.utah.edu/~blg/publications/publications.html#tfgnvf-popl-2016\">orders of magnitude</a>. To answer the first question, we need to step back a bit…</p>\n\n<p>Normally, a type system is an ahead-of-time thing. Programs must typecheck before they can run. Afterwards, types can disappear. Compiled code can safely run full-throttle and assume that everything in its world behaves in a well-typed way.</p>\n\n<p>Gradual typing leads to an entirely different situation. It allows typed and untyped code to live together, which means that part of the codebase might rely on type assumptions that the rest of the codebase does not know about!</p>\n\n<p>Suppose we have a typed function that averages the elements in a list:</p>\n\n<div class=\"brush: python\">\n <pre><code>def avg(nums: list[int]):\n ....</code></pre></div>\n\n<p>This function expects inputs that have the type <code>list[int]</code>. The typechecker will make sure that every call to <code>avg</code> in typed code match this expectation. But the typechecker will not check any calls to <code>avg</code> that appear in untyped code. How could it? Untyped code is, by definition, untyped and un-checked!</p>\n\n<p>Consequently, untyped code can ask outrageous questions when the program runs:</p>\n\n<pre><code>avg(\"hello\")\navg([[1, 7], \"X\", 0])\navg(avg)</code></pre>\n\n<p>We clearly have a problem. Typed code might contain elegant data descriptions that untyped code does not know about. What to do?</p>\n\n<ul>\n <li>One option is to do nothing. Let the programmer beware that gradual types are unsound at the boundaries to untyped code. With this mindset, types remain cost-free but give zero help for debugging. Many languages follow this approach, including TypeScript and mypy.</li>\n <li>Another option is to enforce type soundness with runtime checks. Now we have reliable types (to some extent), but we also have costs to measure and minimize.</li></ul>\n\n<p>The GTP Benchmarks are a collection of 21 programs designed to test the costs of sound gradual types. Each program comes in two forms, untyped and typed (written in Racket and Typed Racket), with the crucial property that any module-by-module mix of the two forms results in a working program. A banchmark with <code>N</code> modules generates <code>2^N</code> partially-typed programs that give a broad picture of the possibilities that gradual typing enables:</p>\n\n<p><img src=\"/img/gtp-lattice.png\" width=\"50%\" /></p>\n\n<p>The table below is a birds-eye view of the benchmarks. It lists their name, purpose, and characteristics: whether they were originally typed (T Init), whether they depend on untyped (U Lib) or typed (T Lib) library code, whether they define geneative datatypes (Adapt), and whether they send higher-order function (HOF), polymorphic types (Poly), recursive types (Rec), mutable data-structure types (Mut), immutable data-structure types (Imm), object types (Obj), or class types (Cls) across a boundary to untyped code.</p>\n\n<p><img src=\"/img/gtp-programs.png\" /></p>\n\n<p>For more details, see <a href=\"https://users.cs.utah.edu/~blg/publications/publications.html#g-rep-2023\">the paper</a>.</p>")) ((p+ #"/Users/ben/code/uu/blog/_src/posts/2024-02-02-luau-telemetry.md" . unix) f post (u . "[Privacy-Respecting Type Error Telemetry at Scale](https://blog.brownplt.org/2024/02/02/privacy-telemetry.html)") (? . 2) 1719613751 (p+ #"/Users/ben/code/uu/blog/2024/02/-privacy-respecting-type-error-telemetry-at-scale-https-blog-brownplt-org-2024-02-02-privacy-telemetry-html.html" . unix) (u . "/2024/02/-privacy-respecting-type-error-telemetry-at-scale-https-blog-brownplt-org-2024-02-02-privacy-telemetry-html.html") (u . "2024-02-02T01:11:11") (? . 6) (? . 3) () (? . 0) #f (? . 0)) ((p+ #"/Users/ben/code/uu/blog/_src/posts/2023-06-26-flowfpx-juliacon.md" . unix) f post (u . "[FlowFPX: Nimble Tools for Debugging Floating-Point Exceptions](https://lambdaland.org/#flowfpx-nimble-tools-for-debugging-floating-point-exceptions--juliacon-2023)") (? . 5) 1720820051 (p+ #"/Users/ben/code/uu/blog/2024/07/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html" . unix) (u . "/2024/07/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html") (u . "2024-07-07T01:11:11") (? . 4) #f () (? . 0) #f (? . 0)) ((p+ #"/Users/ben/code/uu/blog/_src/posts/2024-07-07-ltlf.md" . unix) f post (u . "[Misconceptions In Finite-Trace and Infinite-Trace Linear Temporal Logic](https://blog.brownplt.org/2024/07/07/little-tricky-logics-2.html)") (? . 4) 1720817329 (p+ #"/Users/ben/code/uu/blog/2024/07/-misconceptions-in-finite-trace-and-infinite-trace-linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html" . unix) (u . "/2024/07/-misconceptions-in-finite-trace-and-infinite-trace-linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html") (u . "2024-07-07T01:11:11") (? . 3) (? . 5) () (? . 0) #f (? . 0)) ((p+ #"/Users/ben/code/uu/blog/_src/posts/2023-10-31-conceptual-mutant-testing.md" . unix) f post (u . "[Conceptual Mutation Testing](https://blog.brownplt.org/2023/10/31/conceptual-mutation-testing.html)") (? . 6) 1719613783 (p+ #"/Users/ben/code/uu/blog/2023/10/-conceptual-mutation-testing-https-blog-brownplt-org-2023-10-31-conceptual-mutation-testing-html.html" . unix) (u . "/2023/10/-conceptual-mutation-testing-https-blog-brownplt-org-2023-10-31-conceptual-mutation-testing-html.html") (u . "2023-10-31T01:11:11") (? . 7) (? . 2) () (? . 0) #f (? . 0)) ((p+ #"/Users/ben/code/uu/blog/_src/posts/2023-09-19-generating-programs-trivially.md" . unix) f post (u . "[Generating Programs Trivially: Student Use of Large Language Models](https://blog.brownplt.org/2023/09/19/generating-programs-trivially.html)") (? . 7) 1719613991 (p+ #"/Users/ben/code/uu/blog/2023/09/-generating-programs-trivially-student-use-of-large-language-models-https-blog-brownplt-org-2023-09-19-generating-programs-trivially-html.html" . unix) (u . "/2023/09/-generating-programs-trivially-student-use-of-large-language-models-https-blog-brownplt-org-2023-09-19-generating-programs-trivially-html.html") (u . "2023-09-19T01:11:11") (? . 1) (? . 6) () (? . 0) #f (? . 0)))) | ||
| ((3) 0 () 8 ((u . "") (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-06-28-gtp-benchmarks.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-02-02-luau-telemetry.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-04-21-forge.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-07-07-ltlf.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2023-06-26-flowfpx-juliacon.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2023-10-31-conceptual-mutant-testing.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2023-09-19-generating-programs-trivially.md" . unix)) () (h ! (equal) ((p+ #"/Users/ben/code/uu/blog/_src/posts/2024-04-21-forge.md" . unix) f post (u . "[Forge: A Tool to Teach Formal Methods](https://blog.brownplt.org/2024/04/21/forge.html)") (? . 3) 1719613724 (p+ #"/Users/ben/code/uu/blog/2024/04/-forge-a-tool-to-teach-formal-methods-https-blog-brownplt-org-2024-04-21-forge-html.html" . unix) (u . "/2024/04/-forge-a-tool-to-teach-formal-methods-https-blog-brownplt-org-2024-04-21-forge-html.html") (u . "2024-04-21T01:11:11") (? . 2) (? . 4) () (? . 0) #f (? . 0)) ((? . 1) f post (u . "GTP Benchmarks for Gradual Typing Performance") (? . 1) 1720879367 (p+ #"/Users/ben/code/uu/blog/2023/06/gtp-benchmarks-for-gradual-typing-performance.html" . unix) (u . "/2023/06/gtp-benchmarks-for-gradual-typing-performance.html") (u . "2023-06-28T17:18:44") #f (? . 7) (c (u . "by Ben Greenman")) (u . "\n<p>Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.</p>") #t (u . "\n<p>Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.</p>\n<!-- more-->\n\n<hr />\n\n<p>What on earth is gradual typing performance and why does it matter?</p>\n\n<p>The second question is easy to answer: performance matters because the cost of gradual types can slow a program by several <a href=\"https://users.cs.utah.edu/~blg/publications/publications.html#tfgnvf-popl-2016\">orders of magnitude</a>. To answer the first question, we need to step back a bit…</p>\n\n<p>Normally, a type system is an ahead-of-time thing. Programs must typecheck before they can run. Afterwards, types can disappear. Compiled code can safely run full-throttle and assume that everything in its world behaves in a well-typed way.</p>\n\n<p>Gradual typing leads to an entirely different situation. It allows typed and untyped code to live together, which means that part of the codebase might rely on type assumptions that the rest of the codebase does not know about!</p>\n\n<p>Suppose we have a typed function that averages the elements in a list:</p>\n\n<div class=\"brush: python\">\n <pre><code>def avg(nums: list[int]):\n ....</code></pre></div>\n\n<p>This function expects inputs that have the type <code>list[int]</code>. The typechecker will make sure that every call to <code>avg</code> in typed code match this expectation. But the typechecker will not check any calls to <code>avg</code> that appear in untyped code. How could it? Untyped code is, by definition, untyped and un-checked!</p>\n\n<p>Consequently, untyped code can ask outrageous questions when the program runs:</p>\n\n<pre><code>avg(\"hello\")\navg([[1, 7], \"X\", 0])\navg(avg)</code></pre>\n\n<p>We clearly have a problem. Typed code might contain elegant data descriptions that untyped code does not know about. What to do?</p>\n\n<ul>\n <li>One option is to do nothing. Let the programmer beware that gradual types are unsound at the boundaries to untyped code. With this mindset, types remain cost-free but give zero help for debugging. Many languages follow this approach, including TypeScript and mypy.</li>\n <li>Another option is to enforce type soundness with runtime checks. Now we have reliable types (to some extent), but we also have costs to measure and minimize.</li></ul>\n\n<p>The GTP Benchmarks are a collection of 21 programs designed to test the costs of sound gradual types. Each program comes in two forms, untyped and typed (written in Racket and Typed Racket), with the crucial property that any module-by-module mix of the two forms results in a working program. A benchmark with <code>N</code> modules generates <code>2^N</code> partially-typed programs that sample the space of gradual possibilities:</p>\n\n<p><img src=\"/img/gtp-lattice.png\" width=\"50%\" /></p>\n\n<p>The table below is a birds-eye view of the benchmarks. It lists their name, purpose, and characteristics: whether they were originally typed (T Init), whether they depend on untyped (U Lib) or typed (T Lib) library code, whether they define generative datatypes (Adapt), and whether they send higher-order function (HOF), polymorphic types (Poly), recursive types (Rec), mutable data-structure types (Mut), immutable data-structure types (Imm), object types (Obj), or class types (Cls) across any untyped boundary:</p>\n\n<p><img src=\"/img/gtp-programs.png\" /></p>\n\n<p>For more details, see <a href=\"https://users.cs.utah.edu/~blg/publications/publications.html#g-rep-2023\">the paper</a>.</p>")) ((p+ #"/Users/ben/code/uu/blog/_src/posts/2024-02-02-luau-telemetry.md" . unix) f post (u . "[Privacy-Respecting Type Error Telemetry at Scale](https://blog.brownplt.org/2024/02/02/privacy-telemetry.html)") (? . 2) 1719613751 (p+ #"/Users/ben/code/uu/blog/2024/02/-privacy-respecting-type-error-telemetry-at-scale-https-blog-brownplt-org-2024-02-02-privacy-telemetry-html.html" . unix) (u . "/2024/02/-privacy-respecting-type-error-telemetry-at-scale-https-blog-brownplt-org-2024-02-02-privacy-telemetry-html.html") (u . "2024-02-02T01:11:11") (? . 6) (? . 3) () (? . 0) #f (? . 0)) ((p+ #"/Users/ben/code/uu/blog/_src/posts/2023-06-26-flowfpx-juliacon.md" . unix) f post (u . "[FlowFPX: Nimble Tools for Debugging Floating-Point Exceptions](https://lambdaland.org/#flowfpx-nimble-tools-for-debugging-floating-point-exceptions--juliacon-2023)") (? . 5) 1720820051 (p+ #"/Users/ben/code/uu/blog/2024/07/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html" . unix) (u . "/2024/07/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html") (u . "2024-07-07T01:11:11") (? . 4) #f () (? . 0) #f (? . 0)) ((p+ #"/Users/ben/code/uu/blog/_src/posts/2024-07-07-ltlf.md" . unix) f post (u . "[Misconceptions In Finite-Trace and Infinite-Trace Linear Temporal Logic](https://blog.brownplt.org/2024/07/07/little-tricky-logics-2.html)") (? . 4) 1720817329 (p+ #"/Users/ben/code/uu/blog/2024/07/-misconceptions-in-finite-trace-and-infinite-trace-linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html" . unix) (u . "/2024/07/-misconceptions-in-finite-trace-and-infinite-trace-linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html") (u . "2024-07-07T01:11:11") (? . 3) (? . 5) () (? . 0) #f (? . 0)) ((p+ #"/Users/ben/code/uu/blog/_src/posts/2023-10-31-conceptual-mutant-testing.md" . unix) f post (u . "[Conceptual Mutation Testing](https://blog.brownplt.org/2023/10/31/conceptual-mutation-testing.html)") (? . 6) 1719613783 (p+ #"/Users/ben/code/uu/blog/2023/10/-conceptual-mutation-testing-https-blog-brownplt-org-2023-10-31-conceptual-mutation-testing-html.html" . unix) (u . "/2023/10/-conceptual-mutation-testing-https-blog-brownplt-org-2023-10-31-conceptual-mutation-testing-html.html") (u . "2023-10-31T01:11:11") (? . 7) (? . 2) () (? . 0) #f (? . 0)) ((p+ #"/Users/ben/code/uu/blog/_src/posts/2023-09-19-generating-programs-trivially.md" . unix) f post (u . "[Generating Programs Trivially: Student Use of Large Language Models](https://blog.brownplt.org/2023/09/19/generating-programs-trivially.html)") (? . 7) 1719613991 (p+ #"/Users/ben/code/uu/blog/2023/09/-generating-programs-trivially-student-use-of-large-language-models-https-blog-brownplt-org-2023-09-19-generating-programs-trivially-html.html" . unix) (u . "/2023/09/-generating-programs-trivially-student-use-of-large-language-models-https-blog-brownplt-org-2023-09-19-generating-programs-trivially-html.html") (u . "2023-09-19T01:11:11") (? . 1) (? . 6) () (? . 0) #f (? . 0)))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters