![](\"/img/gtp-lattice.png\")
Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.
") #t (u . "\nSound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.
\n\n\nWhat on earth is gradual typing performance and why does it matter?
\n\nThe second question is easy to answer: performance matters because the cost of gradual types can slow a program by several orders of magnitude. To answer the first question, we need to step back a bit…
\n\nNormally, 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.
\n\nGradual 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!
\n\nSuppose we have a typed function that averages the elements in a list:
\n\ndef avg(nums: list[int]):\n ....This function expects inputs that have the type list[int]. The typechecker will make sure that every call to avg in typed code match this expectation. But the typechecker will not check any calls to avg that appear in untyped code. How could it? Untyped code is, by definition, untyped and un-checked!
Consequently, untyped code can ask outrageous questions when the program runs:
\n\navg(\"hello\")\navg([[1, 7], \"X\", 0])\navg(avg)We clearly have a problem. Typed code might contain elegant data descriptions that untyped code does not know about. What to do?
\n\nThe 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 N modules generates 2^N partially-typed programs that sample the space of gradual possibilities:
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:
\n\n![](\"/img/gtp-programs.png\")
For more details, see the paper.
")) ((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)))) \ No newline at end of file +((3) 0 () 8 ((u . "") (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/2023-06-26-flowfpx-juliacon.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-06-28-gtp-benchmarks.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-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)") (? . 2) 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") (? . 1) (? . 5) () (? . 0) #f (? . 0)) ((p+ #"/Users/ben/code/uu/blog/_src/posts/2024-06-28-gtp-benchmarks.md" . unix) f post (u . "GTP Benchmarks for Gradual Typing Performance") (? . 4) 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") (? . 3) (? . 7) (c (u . "by Ben Greenman")) (u . "\nSound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.
") #t (u . "\nSound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.
\n\n\nWhat on earth is gradual typing performance and why does it matter?
\n\nThe second question is easy to answer: performance matters because the cost of gradual types can slow a program by several orders of magnitude. To answer the first question, we need to step back a bit…
\n\nNormally, 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.
\n\nGradual 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!
\n\nSuppose we have a typed function that averages the elements in a list:
\n\ndef avg(nums: list[int]):\n ....This function expects inputs that have the type list[int]. The typechecker will make sure that every call to avg in typed code match this expectation. But the typechecker will not check any calls to avg that appear in untyped code. How could it? Untyped code is, by definition, untyped and un-checked!
Consequently, untyped code can ask outrageous questions when the program runs:
\n\navg(\"hello\")\navg([[1, 7], \"X\", 0])\navg(avg)We clearly have a problem. Typed code might contain elegant data descriptions that untyped code does not know about. What to do?
\n\nThe 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 N modules generates 2^N partially-typed programs that sample the space of gradual possibilities:
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:
\n\n
For more details, see the paper.
")) ((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)") (? . 1) 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) (? . 2) () (? . 0) #f (? . 0)) ((? . 3) f post (u . "[FlowFPX: Nimble Tools for Debugging Floating-Point Exceptions](https://lambdaland.org/#flowfpx-nimble-tools-for-debugging-floating-point-exceptions--juliacon-2023)") (? . 3) 1720882180 (p+ #"/Users/ben/code/uu/blog/2023/06/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html" . unix) (u . "/2023/06/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html") (u . "2023-06-26T01:11:11") #f (? . 4) () (? . 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)") (? . 5) 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") (? . 2) #f () (? . 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) (? . 1) () (? . 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") (? . 4) (? . 6) () (? . 0) #f (? . 0)))) \ No newline at end of file diff --git a/2024/07/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html b/2023/06/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html similarity index 87% rename from 2024/07/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html rename to 2023/06/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html index 8dbfaa1..eb5ebf0 100644 --- a/2024/07/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html +++ b/2023/06/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html @@ -8,9 +8,9 @@ - - + + @@ -33,7 +33,7 @@