From d4a81f9c8e5c89e8e13708eed3ebd5fee85c01a7 Mon Sep 17 00:00:00 2001 From: Ben Greenman Date: Sat, 13 Jul 2024 10:50:15 -0400 Subject: [PATCH] redate flowfpx --- .frog/build | 2 +- ...oating-point-exceptions-juliacon-2023.html | 6 +++--- ...hmarks-for-gradual-typing-performance.html | 2 +- ...024-07-07-little-tricky-logics-2-html.html | 2 +- _src/posts/2023-06-26-flowfpx-juliacon.md | 2 +- feeds/all.atom.xml | 20 +++++++++---------- feeds/all.rss.xml | 16 +++++++-------- index.html | 18 ++++++++--------- sitemap.txt | 2 +- 9 files changed, 35 insertions(+), 35 deletions(-) rename {2024/07 => 2023/06}/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html (87%) diff --git a/.frog/build b/.frog/build index 3b0ef62..540f308 100644 --- a/.frog/build +++ b/.frog/build @@ -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) 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

Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.

") #t (u . "\n

Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.

\n\n\n
\n\n

What on earth is gradual typing performance and why does it matter?

\n\n

The 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\n

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.

\n\n

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!

\n\n

Suppose we have a typed function that averages the elements in a list:

\n\n
\n 
def avg(nums: list[int]):\n  ....
\n\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!

\n\n

Consequently, untyped code can ask outrageous questions when the program runs:

\n\n
avg(\"hello\")\navg([[1, 7], \"X\", 0])\navg(avg)
\n\n

We clearly have a problem. Typed code might contain elegant data descriptions that untyped code does not know about. What to do?

\n\n\n\n

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 N modules generates 2^N partially-typed programs that sample the space of gradual possibilities:

\n\n

\n\n

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

\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)") (? . 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 . "\n

Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.

") #t (u . "\n

Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.

\n\n\n
\n\n

What on earth is gradual typing performance and why does it matter?

\n\n

The 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\n

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.

\n\n

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!

\n\n

Suppose we have a typed function that averages the elements in a list:

\n\n
\n 
def avg(nums: list[int]):\n  ....
\n\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!

\n\n

Consequently, untyped code can ask outrageous questions when the program runs:

\n\n
avg(\"hello\")\navg([[1, 7], \"X\", 0])\navg(avg)
\n\n

We clearly have a problem. Typed code might contain elegant data descriptions that untyped code does not know about. What to do?

\n\n\n\n

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 N modules generates 2^N partially-typed programs that sample the space of gradual possibilities:

\n\n

\n\n

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

\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 @@

FlowFPX: Nimble Tools for Debugging Floating-Point Exceptions

- ::

+ ::