Add once-useful template

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

.gitignore

@@ -1 +1,4 @@
 **/build/*
+
+/.quarto/
+**/*.quarto_ipynb

Gemfile.lock

@@ -3,11 +3,11 @@ GEM
   specs:
     duktape (2.7.0.0)
     execjs (2.9.1)
-    mini_portile2 (2.8.6)
+    mini_portile2 (2.8.8)
-    nokogiri (1.15.6)
+    nokogiri (1.18.3)
       mini_portile2 (~> 2.8.2)
       racc (~> 1.4)
-    racc (1.8.0)
+    racc (1.8.1)
 
 PLATFORMS
   ruby

_quarto.yml

@@ -0,0 +1,3 @@
+format:
+  gfm:
+    variant: +yaml_metadata_block

agda.rb

@@ -23,7 +23,7 @@ class AgdaContext
     return @file_infos[file] if @file_infos.include? file
 
     @file_infos[file] = line_infos = {}
-    unless File.exists?(file)
+    unless File.exist?(file)
       return line_infos
     end
 
@@ -160,6 +160,14 @@ class FileGroup
         line_range = 1..
       end
 
+      # Sometimes, code is deeply nested in the source file, but we don't
+      # want to show the leading space. In that case, the generator sets
+      # data-source-offset with how much leading space was stripped off.
+      initial_offset = 0
+      if source_offset_attr = t.attribute("data-source-offset")
+        initial_offset = source_offset_attr.to_s.to_i
+      end
+
       full_path = t.attribute("data-file-path").to_s
       full_path_dirs = Pathname(full_path).each_filename.to_a
 
@@ -195,7 +203,7 @@ class FileGroup
         line_info = agda_info[line_no]
         next unless line_info
 
-        offset = 0
+        offset = initial_offset
         line.traverse do |lt|
           if lt.text?
             content = lt.content

analyze.rb

@@ -43,7 +43,7 @@ files.each do |file|
   tags = []
   group = 1
   draft = false
-  next unless File.exists?(file)
+  next unless File.exist?(file)
   value = File.size(file)
   url = file.gsub(/^content/, "https://danilafe.com").delete_suffix("/index.md").delete_suffix(".md")
   File.readlines(file).each do |l|

build-agda-html.rb

@@ -26,7 +26,7 @@ files = ARGV
 code_paths = Dir.entries(root_path).select do |f|
   File.directory?(File.join(root_path, f)) and f != '.' and f != '..'
 end.to_set
-code_paths += JSON.parse(File.read(data_file)).keys if File.exists? data_file
+code_paths += JSON.parse(File.read(data_file)).keys if File.exist? data_file
 # Extending code_paths from submodules.json means that nested Agda modules
 # have their root dir correctly set.
 

chatgpt-subset-feather-icon.rb

@@ -0,0 +1,49 @@
+#!/usr/bin/env ruby
+# frozen_string_literal: true
+
+require 'nokogiri'
+require 'set'
+
+# 1) Process all files passed in from the command line
+svgpath = ARGV[0]
+files = ARGV[1..]
+
+# 2) Extract used Feather icons
+used_icons = Set.new
+
+files.each do |file|
+  # Parse each HTML file
+  doc = File.open(file, "r:UTF-8") { |f| Nokogiri::HTML(f) }
+
+  # Look for <use xlink:href="/feather-sprite.svg#iconName">
+  doc.css("use").each do |use_tag|
+    href = use_tag["xlink:href"] || use_tag["href"]
+    if href && href.start_with?("/feather-sprite.svg#")
+      icon_name = href.split("#").last
+      used_icons << icon_name
+    end
+  end
+end
+
+puts "Found #{used_icons.size} unique icons: #{used_icons.to_a.join(', ')}"
+
+# 3) Load the full feather-sprite.svg as XML
+sprite_doc = File.open(svgpath, "r:UTF-8") { |f| Nokogiri::XML(f) }
+
+# 4) Create a new SVG with only the required symbols
+new_svg = Nokogiri::XML::Document.new
+svg_tag = Nokogiri::XML::Node.new("svg", new_svg)
+svg_tag["xmlns"] = "http://www.w3.org/2000/svg"
+new_svg.add_child(svg_tag)
+
+sprite_doc.css("symbol").each do |symbol_node|
+  if used_icons.include?(symbol_node["id"])
+    # Duplicate the symbol node (so it can be inserted in the new document)
+    svg_tag.add_child(symbol_node.dup)
+  end
+end
+
+# 5) Save the subset sprite
+File.open(svgpath, "w:UTF-8") do |f|
+  f.write(new_svg.to_xml)
+end

chatgpt-subset-one-go.py

@@ -0,0 +1,69 @@
+import os
+import sys
+from bs4 import BeautifulSoup
+from fontTools.subset import Subsetter, Options
+from fontTools.ttLib import TTFont
+
+FONT_EXTENSIONS = (".ttf", ".woff", ".woff2", ".otf")  # Font file types
+
+def extract_text_from_html(file_path):
+    """Extract text content from a single HTML file."""
+    with open(file_path, "r", encoding="utf-8") as f:
+        soup = BeautifulSoup(f.read(), "html.parser")
+        return soup.get_text()
+
+def get_used_characters(files):
+    """Collect unique characters from all .html files in the given directory."""
+    char_set = set()
+    for file in files:
+        text = extract_text_from_html(file)
+        char_set.update(text)
+    return "".join(sorted(char_set))
+
+def find_font_files(directory):
+    """Find all font files in the given directory, recursively."""
+    font_files = []
+    for root, _, files in os.walk(directory):
+        for file in files:
+            if file.endswith(FONT_EXTENSIONS):
+                font_files.append(os.path.join(root, file))
+    return font_files
+
+def subset_font_in_place(font_path, characters):
+    """Subsets the given font file to include only the specified characters."""
+    # Convert characters to their integer code points
+    unicode_set = {ord(c) for c in characters}
+
+    font = TTFont(font_path)
+    options = Options()
+    options.drop_tables += ["DSIG"]
+    options.drop_tables += ["LTSH", "VDMX", "hdmx", "gasp"]
+    options.unicodes = unicode_set
+    options.variations = False
+    options.drop_variations = True
+    options.layout_features = ["*"]  # keep all OT features
+    options.hinting = False
+
+    # Preserve original format if it was WOFF/WOFF2
+    if font_path.endswith(".woff2"):
+        options.flavor = "woff2"
+    elif font_path.endswith(".woff"):
+        options.flavor = "woff"
+
+    subsetter = Subsetter(options)
+    subsetter.populate(unicodes=unicode_set)
+    subsetter.subset(font)
+
+    # Overwrite the original font file
+    font.save(font_path)
+    print(f"Subsetted font in place: {font_path}")
+
+if __name__ == "__main__":
+    used_chars = get_used_characters(sys.argv[2:])
+    print(f"Extracted {len(used_chars)} unique characters from {len(sys.argv[2:])} HTML files.")
+
+    font_files = find_font_files(sys.argv[1])
+    print(f"Found {len(font_files)} font files to subset.")
+
+    for font_file in font_files:
+        subset_font_in_place(font_file, used_chars)

content/blog/02_types_variables.md

@@ -339,9 +339,8 @@ this means the rule applies to (object) variables declared to have type
 our system. A single rule takes care of figuring the types of _all_
 variables.
 
-{{< todo >}}
+> [!TODO]
-The rest of this, but mostly statements.
+> The rest of this, but mostly statements.
-{{< /todo >}}
 
 ### This Page at a Glance
 #### Metavariables

content/blog/chapel_runtime_types.md

@@ -0,0 +1,591 @@
+---
+title: "Chapel's Runtime Types as an Interesting Alternative to Dependent Types"
+date: 2025-03-02T22:52:01-08:00
+tags: ["Chapel", "C++", "Idris", "Programming Languages"]
+description: "In this post, I discuss Chapel's runtime types as a limited alternative to dependent types."
+---
+
+One day, when I was in graduate school, the Programming Languages research
+group was in a pub for a little gathering. Amidst beers, fries, and overpriced
+sandwiches, the professor and I were talking about [dependent types](https://en.wikipedia.org/wiki/Dependent_type). Speaking
+loosely and imprecisely, these are types that are somehow constructed from
+_values_ in a language, like numbers.
+
+For example, in C++, [`std::array`](https://en.cppreference.com/w/cpp/container/array)
+is a dependent type. An instantiation of the _type_ `array`, like `array<string, 3>`
+is constructed from the type of its elements (here, `string`) and a value
+representing the number of elements (here, `3`). This is in contrast with types
+like `std::vector`, which only depends on a type (e.g., `vector<string>` would
+be a dynamically-sized collection of strings).
+
+I was extolling the virtues of general dependent types, like you might find
+in [Idris](https://www.idris-lang.org/) or [Agda](https://agda.readthedocs.io/en/latest/getting-started/what-is-agda.html):
+more precise function signatures! The
+{{< sidenote "right" "curry-howard-note" "Curry-Howard isomorphism!" >}}
+The Curry-Howard isomorphism is a common theme on this blog. I've
+<a href="{{< relref "typesafe_interpreter_revisited#curry-howard-correspondence" >}}">
+written about it myself</a>, but you can also take a look at the
+<a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">
+Wikipedia page</a>.
+{{< /sidenote >}} The professor was skeptical. He had been excited about
+dependent types in the past, but nowadays he felt over them. They were cool, he
+said, but there are few practical uses. In fact, he posed a challenge:
+
+> Give me one good reason to use dependent types in practice that doesn't
+> involve keeping track of bounds for lists and matrices!
+{#bounds-quote}
+
+This challenge alludes to fixed-length lists -- [vectors](https://agda.github.io/agda-stdlib/master/Data.Vec.html)
+-- which are one of the first dependently-typed data structures one learns about.
+Matrices are effectively vectors-of-vectors. In fact, even in giving my introductory
+example above, I demonstrated the C++ equivalent of a fixed-length list, retroactively
+supporting the professor's point.
+
+It's not particularly important to write down how I addressed the challenge;
+suffice it to say that the notion resonated with some of the other
+students present in the pub. In the midst of practical development, how much
+of dependent types' power can you leverage, and how much power do you pay
+for but never use?
+
+A second round of beers arrived. The argument was left largely unresolved,
+and conversation flowed to other topics. Eventually, I graduated, and started
+working on the [Chapel language](https://chapel-lang.org/) team (I also
+[write on the team's blog](https://chapel-lang.org/blog/authors/daniel-fedorin/)).
+
+When I started looking at Chapel programs, I could not believe my eyes...
+
+### A Taste of Chapel's Array Types
+
+Here's a simple Chapel program that creates an array of 10 integers.
+
+```Chapel
+var A: [0..9] int;
+```
+
+Do you see the similarity to the `std::array` example above? Of course, the
+syntax is quite different, but in _essence_ I think the resemblance is
+uncanny. Let's mangle the type a bit --- producing invalid Chapel programs ---
+just for the sake of demonstration.
+
+```Chapel
+var B: array(0..9, int); // first, strip the syntax sugar
+var C: array(int, 0..9); // swap the order of the arguments to match C++
+```
+
+Only one difference remains: in C++, arrays are always indexed from zero. Thus,
+writing `array<int, 10>` would implicitly create an array whose indices start
+with `0` and end in `9`. In Chapel, array indices can start at values other
+than zero (it happens to be useful for elegantly writing numerical programs),
+so the type explicitly specifies a lower and a higher bound. Other than that,
+though, the two types look very similar.
+
+In general, Chapel arrays have a _domain_, typically stored in variables like `D`.
+The domain of `A` above is `{0..9}`. This domain is part of the array's type.
+
+Before I move on, I'd like to pause and state a premise that is crucial
+for the rest of this post: __I think knowing the size of a data structure,
+like `std::array` or Chapel's `[0..9] int`, is valuable__. If this premise
+were not true, there'd be no reason to prefer `std::array` to `std::vector`, or
+care that Chapel has indexed arrays. However, having this information
+can help in numerous ways, such as:
+
+* __Enforcing compatible array shapes.__ For instance, the following Chapel
+  code would require two arrays passed to function `foo` to have the same size.
+
+  ```Chapel
+  proc doSomething(people: [?D] person, data: [D] personInfo) {}
+  ```
+
+  Similarly, we can enforce the fact that an input to a function has the same shape
+  as the output:
+
+  ```Chapel
+  proc transform(input: [?D] int): [D] string;
+  ```
+* __Consistency in generics__. Suppose you have a generic function that declares
+  a new variable of a given type, and just returns it:
+
+  ```Chapel
+  proc defaultValue(type argType) {
+    var x: argType;
+    return x;
+  }
+  ```
+
+  Code like this exists in "real" Chapel software, by the way --- the example
+  is not contrived. By including the bounds etc. into the array type, we can
+  ensure that `x` is appropriately allocated. Then, `defaultValue([1,2,3].type)`
+  would return an array of three default-initialized integers.
+* __Eliding boundary checking__. Boundary checking is useful for safety,
+  since it ensures that programs don't read or write past the end of allocated
+  memory. However, bounds checking is also slow. Consider the following function that
+  sums two arrays:
+
+  ```Chapel
+  proc sumElementwise(A: [?D] int, B: [D] int) {
+    var C: [D] int;
+    for idx in D do
+      C[idx] = A[idx] + B[idx];
+  }
+  ```
+
+  Since arrays `A`, `B`, and `C` have the same domain `D`, we don't need
+  to do bound checking when accessing any of their elements. I don't believe
+  this is currently an optimisation in Chapel, but it's certainly on the
+  table.
+* __Documentation__. Including the size of the array as part of type
+  signature clarifies the intent of the code being written. For instance,
+  in the following function:
+
+  ```Chapel
+  proc sendEmails(numEmails: int, destinationAddrs: [1..numEmails] address) { /* ... */ }
+  ```
+
+  It's clear from the type of the `destinationAddrs`s that there ought to
+  be exactly as many `destinationAddrs` as the number of emails that should
+  be sent.
+
+Okay, recap: C++ has `std::array`, which is a dependently-typed container
+that represents an array with a fixed number of elements. Chapel has something
+similar. I think these types are valuable.
+
+At this point, it sort of looks like I'm impressed with Chapel for copying a C++
+feature from 2011. Not so! As I played with Chapel programs more and more,
+arrays miraculously supported patterns that I knew I couldn't write in C++.
+The underlying foundation of Chapel's array types is quite unlike any other.
+Before we get to that, though, let's take a look at how dependent types
+are normally used (by us mere mortal software engineers).
+
+### Difficulties with Dependent Types
+
+Let's start by looking at a simple operation on fixed-length lists: reversing them.
+One might write a reverse function for "regular" lists, ignoring details
+like ownership, copying, that looks like this:
+
+```C++
+std::vector<int> reverse(std::vector<int>);
+```
+
+This function is not general: it won't help us reverse lists of
+strings, for instance. The "easy fix" is to replace `int` with some kind
+of placeholder that can be replaced with any type.
+
+```C++
+std::vector<T> reverse(std::vector<T>);
+```
+
+You can try compiling this code, but you will immediately run into an error.
+What the heck is `T`? Normally,
+when we name a variable, function, or type (e.g., by writing `vector`, `reverse`),
+we are referring to its declaration somewhere else. At this time, `T` is not
+declared anywhere. It just "appears" in our function's type. To fix this,
+we add a declaration for `T` by turning `reverse` into a template:
+
+```C++
+template <typename T>
+std::vector<T> reverse(std::vector<T>);
+```
+
+The new `reverse` above takes two arguments: a type and a list of values of
+that type. So, to _really_ call this `reverse`, we need to feed the type
+of our list's elements into it. This is normally done automatically
+(in C++ and otherwise) but under the hood, invocations might look like this:
+
+```C++
+reverse<int>({1,2,3});              // produces 3, 2, 1
+reverse<string>({"world", "hello"}) // produces "hello", "world"
+```
+
+This is basically what we have to do to write `reverse` on `std::array`, which,
+includes an additional parameter that encodes its length. We might start with
+the following (using `n` as a placeholder for length, and observing that
+reversing an array doesn't change its length):
+
+```C++
+std::array<T, n> reverse(std::array<T, n>);
+```
+
+Once again, to make this compile, we need to add template parameters for `T` and `n`.
+
+```C++
+template <typename T, size_t n>
+std::array<T, n> reverse(std::array<T, n>);
+```
+
+Now, you might be asking...
+
+{{< dialog >}}
+{{< message "question" "reader" >}}
+This section is titled "Difficulties with Dependent Types". What's the difficulty?
+{{< /message >}}
+{{< /dialog >}}
+
+Well, here's the kicker. C++ templates are a __compile-time mechanism__. As
+a result, arguments to `template` (like `T` and `n`) must be known when the
+program is being compiled. This, in turn, means
+{{< sidenote "right" "deptype-note" "the following program doesn't work:" >}}
+The observant reader might have noticed that one of the Chapel programs we
+saw above, <code>sendEmails</code>, does something similar. The
+<code>numEmails</code> argument is used in the type of the
+<code>destinationAddrs</code> parameter. That program is valid Chapel.
+{{< /sidenote >}}
+
+```C++
+void buildArray(size_t len) {
+  std::array<int, len> myArray;
+  // do something with myArray
+}
+```
+
+You can't use these known-length types like `std::array` with any length
+that is not known at compile-time. But that's a lot of things! If you're reading
+from an input file, chances are, you don't know how big that file is. If you're
+writing a web server, you likely don't know the length the HTTP requests.
+With every setting a user can tweak when running your code, you sacrifice the
+ability to use templated types.
+
+Also, how do you _return_ a `std::array`? If the size of the returned array is
+known in advance, you just list that size:
+
+```C++
+std::array<int, 10> createArray();
+```
+
+If the size is not known at compile-time, you might want to do something like
+the following --- using an argument `n` in the type of the returned array ---
+but it would not compile:
+
+```C++
+auto computeNNumbers(size_t n) -> std::array<int, n>; // not valid C++
+```
+
+Moreover, you actually can't use `createArray` to figure out the required
+array size, and _then_ return an array that big, even if in the end you
+only used compile-time-only computations in the body of `createArray`.
+What you would need is to provide a "bundle" of a value and a type that is somehow
+built from that value.
+
+```C++
+// magic_pair is invented syntax, will not even remotely work
+auto createArray() -> magic_pair<size_t size, std::array<int, size>>;
+```
+
+This pair contains a `size` (suppose it's known at compilation time for
+the purposes of appeasing C++) as well as an array that uses that `size`
+as its template argument. This is not real C++ -- not even close -- but
+such pairs are a well-known concept. They are known as
+[dependent pairs](https://unimath.github.io/agda-unimath/foundation.dependent-pair-types.html),
+or, if you're trying to impress people, \(\Sigma\)-types. In Idris, you
+could write `createArray` like this:
+
+```Idris
+createArray : () -> (n : Nat ** Vec n Int)
+```
+
+There are languages out there -- that are not C++, alas -- that support
+dependent pairs, and as a result make it more convenient to use types that
+depend on values. Not only that, but a lot of these languages do not force
+dependent types to be determined at compile-time. You could write that
+coveted `readArrayFromFile` function:
+
+```Idris
+readArrayFromFile : String -> IO (n : Nat ** Vec n String)
+```
+
+Don't mind `IO`; in pure languages like Idris, this type is a necessity when
+interacting when reading data in and sending it out. The key is that
+`readArrayFromFile` produces, at runtime, a pair of `n`, which is the size
+of the resulting array, and a `Vec` of that many `String`s (e.g., one string
+per line of the file).
+
+Dependent pairs are cool and very general. However, the end result of
+types with bounds which are not determined at compile-time is that you're
+_required_ to use dependent pairs. Thus, you must always carry the array's length
+together with the array itself.
+
+The bottom line is this:
+
+* In true dependently typed languages, a type that depends on a value (like `Vec`
+  in Idris) lists that value in its type. When this value is listed by
+  referring to an identifier --- like `n` in `Vec n String` above --- this
+  identifier has to be defined somewhere, too. This necessitates dependent pairs,
+  in which the first element is used syntactically as the "definition point"
+  of a type-level value. For example, in the following piece of code:
+
+  ```Idris
+  (n : Nat ** Vec n String)
+  ```
+
+  The `n : Nat` part of the pair serves both to say that the first element
+  is a natural number, and to introduce a variable `n` that refers to
+  this number so that the second type (`Vec n String`) can refer to it.
+
+  A lot of the time, you end up carrying this extra value (bound to `n` above)
+  with your type.
+* In more mainstream languages, things are even more restricted: dependently
+  typed values are a compile-time property, and thus, cannot be used with
+  runtime values like data read from a file, arguments passed in to a function,
+  etc..
+
+### Hiding Runtime Values from the Type
+
+Let's try to think of ways to make things more convenient. First of all, as
+we saw, in Idris, it's possible to use runtime values in types. Not only that,
+but Idris is a compiled language, so presumably we can compile dependently typed programs
+with runtime-enabled dependent types. The trick is to forget some information:
+turn a vector `Vec n String` into two values (the size of the vector and the
+vector itself), and forget -- for the purposes of generating code -- that they're
+related. Whenever you pass in a `Vec n String`, you can compile that similarly
+to how you'd compile passing in a `Nat` and `List String`. Since the program has
+already been type checked, you can be assured that you don't encounter cases
+when the size and the actual vector are mismatched, or anything else of that
+nature.
+
+Additionally, you don't always need the length of the vector at all. In a
+good chunk of Idris code, the size arguments are only used to ensure type
+correctness and rule out impossible cases; they are never accessed at runtime.
+As a result, you can _erase_ the size of the vector altogether. In fact,
+[Idris 2](https://github.com/idris-lang/Idris2/) leans on [Quantitative Type Theory](https://bentnib.org/quantitative-type-theory.html)
+to make erasure easier.
+
+At this point, one way or another, we've "entangled" the vector with a value
+representing its size:
+
+* When a vector of some (unknown, but fixed) length needs to be produced from
+  a function, we use dependent pairs.
+* Even in other cases, when compiling, we end up treating a vector as a
+  length value and the vector itself.
+
+Generally speaking, a good language design practice is to hide extraneous
+complexity, and to remove as much boilerplate as necessary. If the size
+value of a vector is always joined at the hip with the vector, can we
+avoid having to explicitly write it?
+
+This is pretty much exactly what Chapel does. It _allows_ explicitly writing
+the domain of an array as part of its type, but doesn't _require_ it. When
+you do write it (re-using my original snippet above):
+
+```Chapel
+var A: [0..9] int;
+```
+
+What you are really doing is creating a value (the [range](https://chapel-lang.org/docs/primers/ranges.html) `0..9`),
+and entangling it with the type of `A`. This is very similar to what a language
+like Idris would do under the hood to compile a `Vec`, though it's not quite
+the same.
+
+At the same time, you can write code that omits the bounds altogether:
+
+```Chapel
+proc processArray(A: [] int): int;
+proc createArray(): [] int;
+```
+
+In all of these examples, there is an implicit runtime value (the bounds)
+that is associated with the array's type. However, we are never forced to
+explicitly thread through or include a size. Where reasoning about them is not
+necessary, Chapel's domains are hidden away. Chapel refers to the implicitly
+present value associated with an array type as its _runtime type_.
+
+I hinted earlier that things are not quite the same in this representation
+as they are in my simplified model of Idris. In Idris, as I mentioned earlier,
+the values corresponding to vectors' indices can be erased if they are not used.
+In Chapel, this is not the case --- a domain always exists at runtime. At the
+surface level, this means that you may pay for more than what you use. However,
+domains enable a number of interesting patterns of array code. We'll get
+to that in a moment; first, I want to address a question that may be on
+your mind:
+
+{{< dialog >}}
+{{< message "question" "reader" >}}
+At this point, this looks just like keeping a <code>.length</code> field as
+part of the array value. Most languages do this. What's the difference
+between this and Chapel's approach?
+{{< /message >}}
+{{< /dialog >}}
+
+This is a fair question. The key difference is that the length exists even if an array
+does not. The following is valid Chapel code (re-using the `defaultValue`
+snippet above):
+
+```Chapel
+proc defaultValue(type argType) {
+  var x: argType;
+  return x;
+}
+
+proc doSomething() {
+  type MyArray = [1..10] int;
+  var A = defaultValue(MyArray);
+}
+```
+
+Here, we created an array `A` with the right size (10 integer elements)
+without having another existing array as a reference. This might seem like
+a contrived example (I could've just as well written `var A: [1..10] int`),
+but the distinction is incredibly helpful for generic programming. Here's
+a piece of code from the Chapel standard library, which implements
+a part of Chapel's [reduction](https://chapel-lang.org/docs/primers/reductions.html) support:
+
+{{< githubsnippet "chapel-lang/chapel" "e8ff8ee9a67950408cc6d4c3220ac647817ddae3" "modules/internal/ChapelReduce.chpl" "Chapel" 146 >}}
+    inline proc identity {
+      var x: chpl__sumType(eltType); return x;
+    }
+{{< /githubsnippet >}}
+
+Identity elements are important when performing operations like sums and products,
+for many reasons. For one, they tell you what the sum (e.g.) should be when there
+are no elements at all. For another, they can be used as an initial value for
+an accumulator. In Chapel, when you are performing a reduction, there is a
+good chance you will need several accumulators --- one for each thread performing
+a part of the reduction.
+
+That `identity` function looks almost like `defaultValue`! Since it builds the
+identity element from the type, and since the type includes the array's dimensions,
+summing an array-of-arrays, even if it's empty, will produce the correct output.
+
+```Chapel
+type Coordinate = [1..3] real;
+
+var Empty: [0..<0] Coordinate;
+writeln(+ reduce Empty); // sum up an empty list of coordinates
+```
+
+As I mentioned before, having the domain be part of the type can also enable
+indexing optimizations --- without any need for [interprocedural analysis](https://en.wikipedia.org/wiki/Interprocedural_optimization) ---
+in functions like `sumElementwise`:
+
+```Chapel
+proc sumElementwise(A: [?D] int, B: [D] int) {
+  var C: [D] int;
+  for idx in D do
+    C[idx] = A[idx] + B[idx];
+}
+```
+
+The C++ equivalent of this function -- using `vectors` to enable arbitrary-size
+lists of numbers read from user input, and `.at` to enable bounds checks ---
+does not include enough information for this optimization to be possible.
+
+```C++
+void sumElementwise(std::vector<int> A, std::vector<int> B) {
+  std::vector<int> C(A.size());
+
+  for (size_t i = 0; i < A.size(); i++) {
+    C.at(i) = A.at(i) + B.at(i);
+  }
+}
+```
+
+All in all, this makes for a very interesting mix of features:
+
+* __Chapel arrays have their bounds as part of types__, like `std::array` in C++
+  and `Vec` in Idris. This enables all the benefits I've described above.
+* __The bounds don't have to be known at compile-time__, like all dependent
+  types in Idris. This means you can read arrays from files (e.g.) and still
+  reason about their bounds as part of the type system.
+* __Domain information can be hidden when it's not used__, and does not require
+  explicit additional work like template parameters or dependent pairs.
+
+Most curiously, runtime types only extend to arrays and domains. In that sense,
+they are not a general purpose replacement for dependent types. Rather,
+they make arrays and domains special, and single out the exact case my
+professor was [talking about in the introduction](#bounds-quote). Although
+at times I've [twisted Chapel's type system in unconventional ways](https://chapel-lang.org/blog/posts/linear-multistep/)
+to simulate dependent types, rarely have I felt a need for them while
+programming in Chapel. In that sense --- and in the "practical software engineering"
+domain --- I may have been proven wrong.
+
+### Pitfalls of Runtime Types
+
+Should all languages do things the way Chapel does? I don't think so. Like
+most features, runtime types like that in Chapel are a language design
+tradeoff. Though I've covered their motivation and semantics, perhaps
+I should mention the downsides.
+
+The greatest downside is that, generally speaking, _types are not always a
+compile-time property_. We saw this earlier with `MyArray`:
+
+```Chapel
+type MyArray = [1..10] int;
+```
+
+Here, the domain of `MyArray` (one-dimensional with bounds `1..10`) is a runtime
+value. It has an
+{{< sidenote "right" "dce-note" "execution-time cost." >}}
+The execution-time cost is, of course, modulo <a href="https://en.wikipedia.org/wiki/Dead-code_elimination">dead code elimination</a> etc.. If
+my snippet made up the entire program being compiled, the end result would
+likely do nothing, since <code>MyArray</code> isn't used anywhere.
+{{< /sidenote >}}
+Moreover, types that serve as arguments to functions (like `argType` for
+`defaultValue`), or as their return values (like the result of `chpl__sumType`)
+also have an execution-time backing. This is quite different from most
+compiled languages. For instance, in C++, templates are "stamped out" when
+the program is compiled. A function with a `typename T` template parameter
+called with type `int`, in terms of generated code, is always the same as
+a function where you search-and-replaced `T` with `int`. This is called
+[monomorphization](https://en.wikipedia.org/wiki/Monomorphization), by the
+way. In Chapel, however, if the function is instantiated with an array type,
+it will have an additional parameter, which represents the runtime component
+of the array's type.
+
+The fact that types are runtime entities means that compile-time type checking
+is insufficient. Take, for instance, the above `sendEmails` function:
+
+```Chapel
+proc sendEmails(numEmails: int, destinationAddrs: [1..numEmails] address) { /* ... */ }
+```
+
+Since `numEmails` is a runtime value (it's a regular argument!), we can't ensure
+at compile-time that a value of some array matches the `[1..numEmails] address`
+type. As a result, Chapel defers bounds checking to when the `sendEmails`
+function is invoked.
+
+This leads to some interesting performance considerations. Take two Chapel records
+(similar to `struct`s in C++) that simply wrap a value. In one of them,
+we provide an explicit type for the field, and in the other, we leave the field
+type generic.
+
+```Chapel
+record R1 { var field: [1..10] int; }
+record R2 { var field; }
+
+var A = [1,2,3,4,5,6,7,8,9,10];
+var r1 = new R1(A);
+var r2 = new R2(A);
+```
+
+In a conversation with a coworker, I learned that these are not the same.
+That's because the record `R1` explicitly specifies a type
+for `field`. Since the type has a runtime component, the constructor
+of `R1` will actually perform a runtime check to ensure that the argument
+has 10 elements. `R2` will not do this, since there isn't any other type
+to check against.
+
+Of course, the mere existence of an additional runtime component is a performance
+consideration. To ensure that Chapel programs perform as well as possible,
+the Chapel standard library attempts to avoid using runtime components
+wherever possible. This leads to a distinction between a "static type"
+(known at compile-time) and a "dynamic type" (requiring a runtime value).
+The `chpl__sumType` function we saw mentioned above uses static components of
+types, because we don't want each call to `+ reduce` to attempt to run a number
+of extraneous runtime queries.
+
+### Conclusion
+
+Though runtime types are not a silver bullet, I find them to be an elegant
+middle-ground solution to the problem of tracking array bounds. They enable
+optimizations, generic programming, and more, without the complexity of
+a fully dependently-typed language. They are also quite unlike anything I've
+seen in any other language.
+
+What's more, this post only scratches the surface of what's possible using
+arrays and domains. Besides encoding array bounds, domains include information
+about how an array is distributed across several nodes (see the
+[distributions primer](https://chapel-lang.org/docs/primers/distributions.html)),
+and how it's stored in memory (see the [sparse computations](https://chapel-lang.org/blog/posts/announcing-chapel-2.3/#sparse-computations)
+section of the recent 2.3 release announcement). In general, they are a very
+flavorful component to Chapel's "special sauce" as a language for parallel
+computing.
+
+You can read more about arrays and domains in the [corresponding primer](https://chapel-lang.org/docs/primers/arrays.html).

content/blog/idris_catamorphisms.md

@@ -17,7 +17,8 @@ spend time explaining dependent types, nor the syntax for them in Idris,
 which is the language I'll use in this article. Below are a few resources
 that should help you get up to speed.
 
-{{< todo >}}List resources{{< /todo >}}
+> [!TODO]
+> List resources
 
 We've seen that, given a function `F a -> a`, we can define a function
 `B -> a`, if `F` is a base functor of the type `B`. However, what if

content/blog/music_theory/index.qmd

@@ -0,0 +1,484 @@
+---
+title: "Some Music Theory From (Computational) First Principles"
+date: 2025-09-20T18:36:28-07:00
+draft: true
+filters: ["./to-parens.lua"]
+custom_js: ["playsound.js"]
+---
+
+Sound is a perturbation in air pressure that our ear recognizes and interprets.
+A note, which is a fundamental building block of music, is a perturbation
+that can be described by a sine wave. All sine waves have a specific and
+unique frequency. The frequency of a note determines how it sounds (its
+_pitch_). Pitch is a matter of our perception; however, it happens to
+correlate with frequency, such that notes with higher frequencies
+are perceived as higher pitches. 
+
+Let's encode a frequency as a class in Python.
+
+```{python}
+#| echo: false
+import math
+import colorsys
+```
+
+```{python}
+class Frequency:
+    def __init__(self, hz):
+        self.hz = hz
+```
+
+```{python}
+#| echo: false
+
+def points_to_polyline(points, color):
+    return """<polyline fill="none" stroke="{color}"
+                     stroke-width="4"
+                     points="{points_str}" />""".format(
+        color=color,
+        points_str=" ".join(f"{x},{y}" for x, y in points)
+    )
+
+def wrap_svg(inner_svg, width, height):
+    return f"""<svg xmlns="http://www.w3.org/2000/svg"
+                   width="{width}" height="{height}"
+                   viewBox="0 0 {width} {height}">
+                   {inner_svg}
+               </svg>"""
+
+OVERLAY_HUE = 0
+class Superimpose:
+    def __init__(self, *args):
+        global OVERLAY_HUE
+
+        self.args = args
+        self.color = hex_from_hsv(OVERLAY_HUE, 1, 1)
+        OVERLAY_HUE = (OVERLAY_HUE + 1.618033988) % 1
+
+    def points(self, width, height):
+        points = []
+        if not self.args:
+            return [0 for _ in range(width)]
+
+        first_points = [(x, y - height/2) for (x, y) in self.args[0].points(width, height)]
+        for thing in self.args[1:]:
+            other_points = thing.points(width, height)
+            for (i, ((x1, y1), (x2, y2))) in enumerate(zip(first_points, other_points)):
+                assert(x1 == x2)
+                first_points[i] = (x1, y1 + (y2 - height/2))
+
+        # normalize
+        max_y = max(abs(y) for x, y in first_points)
+        if max_y > height / 2:
+            first_points = [(x, y * (0.9 * height / 2) / max_y) for x, y in first_points]
+
+        return [(x, height/2 + y) for x, y in first_points]
+
+    def get_color(self):
+        return self.color
+
+    def _repr_svg_(self):
+        width = 720
+        height = 100
+
+        points = self.points(width, height)
+        return wrap_svg(
+            points_to_polyline(points, self.get_color()),
+            width, height
+        )
+
+def hugo_shortcode(body):
+    return "{{" + "< " + body + " >" + "}}"
+
+class PlayNotes:
+    def __init__(self, *hzs):
+        self.hzs = hzs
+
+    def _repr_html_(self):
+        toplay = ",".join([str(hz) for hz in self.hzs])
+        return hugo_shortcode(f"playsound \"{toplay}\"")
+
+class VerticalStack:
+    def __init__(self, *args):
+        self.args = args
+
+    def _repr_svg_(self):
+        width = 720
+        height = 100
+        buffer = 10
+
+        polylines = []
+        for (i, arg) in enumerate(self.args):
+            offset = i * (height + buffer)
+            points = [(x, y+offset) for (x,y) in arg.points(width, height)]
+            polylines.append(points_to_polyline(points, arg.get_color()))
+
+        return wrap_svg(
+            "".join(polylines),
+            width, len(self.args) * (height + buffer)
+        )
+
+def hex_from_hsv(h, s, v):
+    r, g, b = colorsys.hsv_to_rgb(h, s, v)
+    return f"#{int(r*255):02x}{int(g*255):02x}{int(b*255):02x}"
+
+def color_for_frequency(hz):
+    while hz < 261.63:
+        hz *= 2
+    while hz > 523.25:
+        hz /= 2
+
+    hue = (math.log2(hz / 261.63) * 360)
+    return hex_from_hsv(hue / 360, 1, 1)
+
+def Frequency_points(self, width=720, height=100):
+    # let 261.63 Hz be 5 periods in the width
+    points = []
+    period = width / 5
+    for x in range(width):
+        y = 0.9 * height / 2 * math.sin(x/period * self.hz / 261.63 * 2 * math.pi)
+        points.append((x, height/2 - y))
+    return points
+
+def Frequency_get_color(self):
+    return color_for_frequency(self.hz)
+
+def Frequency_repr_svg_(self):
+    # the container on the blog is 720 pixels wide. Use that.
+    width = 720
+    height = 100
+
+    points = self.points(width, height)
+    points_str = " ".join(f"{x},{y}" for x, y in points)
+    return wrap_svg(
+        points_to_polyline(points, self.get_color()),
+        width, height
+    )
+
+Frequency.points = Frequency_points
+Frequency.get_color = Frequency_get_color
+Frequency._repr_svg_ = Frequency_repr_svg_
+```
+
+Let's take a look at a particular frequency. For reason that are historical
+and not particularly interesting to me, this frequency is called "middle C".
+
+```{python}
+middleC = Frequency(261.63)
+middleC
+```
+
+```{python}
+#| echo: false
+PlayNotes(middleC.hz)
+```
+
+Great! Now, if you're a composer, you can play this note and make music out
+of it. Except, music made with just one note is a bit boring, just like saying
+the same word over and over again won't make for an interesting story.
+No big deal -- we can construct a whole variety of notes by picking any
+other frequency.
+
+```{python}
+g4 = Frequency(392.445)
+g4
+```
+
+```{python}
+#| echo: false
+PlayNotes(g4.hz)
+```
+
+```{python}
+fSharp4 = Frequency(370.000694) # we write this F#
+fSharp4
+```
+
+```{python}
+#| echo: false
+PlayNotes(fSharp4.hz)
+```
+
+This is pretty cool. You can start making melodies with these notes, and sing
+some jingles. However, if your friend sings along with you, and happens to
+sing F# while you're singing the middle C, it's going to sound pretty awful.
+So awful does it sound that somewhere around the 18th century, people started
+calling it _diabolus in musica_ (the devil in music).
+
+Why does it sound so bad? Let's take a look at the
+{{< sidenote "right" "superposition-note" "superposition" >}}
+When waves combine, they follow the principle of superposition. One way
+to explain this is that their graphs are added to each other. In practice,
+what this means is that two peaks in the same spot combine to a larger
+peak, as do two troughs; on the other hand, a peak and a trough "cancel out"
+and produce a "flatter" line.
+{{< /sidenote >}} of these two
+notes, which is what happens when they are played at the same time. For reason I'm
+going to explain later, I will multiply each frequency by 4. These frequencies
+still sound bad together, but playing them higher lets me "zoom out" and
+show you the bigger picture.
+
+```{python}
+Superimpose(Frequency(middleC.hz*4), Frequency(fSharp4.hz*4))
+```
+```{python}
+#| echo: false
+PlayNotes(middleC.hz, fSharp4.hz)
+```
+
+Looking at this picture, we can see that it's far more disordered than the
+pure sine waves we've been looking at so far. There's not much of a pattern
+to the peaks. This is interpreted by our brain as unpleasant.
+
+{{< dialog >}}
+{{< message "question" "reader" >}}
+So there's no fundamental reason why these notes sound bad together?
+{{< /message >}}
+{{< message "answer" "Daniel" >}}
+That's right. We might objectively characterize the combination of these
+two notes as having a less clear periodicity, but that doesn't mean
+that fundamentally it should sound bad. Them sounding good is a purely human
+judgement.
+{{< /message >}}
+{{< /dialog >}}
+
+If picking two notes whose frequencies don't combine into a nice pattern
+makes for a bad sound, then to make a good sound we ought to pick two notes
+whose frequencies *do* combine into a nice pattern. 
+Playing the same frequency twice at the same time certainly will do it,
+because both waves will have the exact same peaks and troughs.
+
+```{python}
+Superimpose(middleC, middleC)
+```
+
+In fact, this is just like playing one note, but louder. The fact of the matter
+is that *playing any other frequency will mean that not all extremes of the graph align*.
+We'll get graphs that are at least a little bink wonky. Intuitively, let's say
+that our wonky-ish graph has a nice pattern when they repeat quickly. That way,
+there's less time for the graph to do other, unpredictable things.
+
+What's the soonest we can get our combined graph to repeat? It can't
+repeat any sooner than either one of the individual notes --- how could it?
+We can work with that, though. If we make one note have exactly twice
+the frequency of the other, then exactly at the moment the less frequent
+note completes its first repetition, the more frequent note will complete
+its second. That puts us right back where we started. Here's what this looks
+like graphically:
+
+```{python}
+twiceMiddleC = Frequency(middleC.hz*2)
+VerticalStack(
+    middleC,
+    twiceMiddleC,
+    Superimpose(middleC, twiceMiddleC)
+)
+```
+
+```{python}
+#| echo: false
+PlayNotes(middleC.hz, twiceMiddleC.hz)
+```
+
+You can easily inspect the new graph to verify that it has a repeating pattern,
+and that this pattern repeats exactly as frequently as the lower-frequency
+note at the top. Indeed, these two notes sound quite good together. It turns
+out, our brains consider them the same in some sense. If you have ever tried to
+sing a song that was outside of your range (like me singing along to Taylor Swift),
+chances are you sang notes that had half the frequency of the original.
+We say that these notes are _in the same pitch class_. While only the first
+of the two notes I showed above was the _middle_ C, we call both notes C.
+To distinguish different-frequency notes of the same pitch class, we sometimes
+number them. The ones in this example were C4 and C5.
+We can keep applying this trick to get C6, C7, and so on.
+
+```{python}
+C = {}
+note = middleC
+for i in range(4, 10):
+    C[i] = note
+    note = Frequency(note.hz * 2)
+
+C[4]
+```
+
+To get C3 from C4, we do the reverse, and halve the frequency.
+```{python}
+note = middleC
+for i in range(4, 0, -1):
+    C[i] = note
+    note = Frequency(note.hz / 2)
+
+C[1]
+```
+
+You might've already noticed, but I set up this page so that individual
+sine waves in the same pitch class have the same color.
+
+All of this puts us almost right back where we started. We might have
+different pithes, but we've only got one pitch _class_. Let's try again.
+Previously, we made it so the second repeat of one note lined up with the
+first repeat of another. What if we pick another note that repeats _three_
+times as often instead?
+
+```{python}
+thriceMiddleC = Frequency(middleC.hz*3)
+VerticalStack(
+    middleC,
+    thriceMiddleC,
+    Superimpose(middleC, thriceMiddleC)
+)
+```
+```{python}
+#| echo: false
+PlayNotes(middleC.hz, thriceMiddleC.hz)
+```
+
+That's not bad! These two sound good together as well, but they are not
+in the same pitch class. There's only one problem: these notes are a bit
+far apart in terms of pitch. That `triceMiddleC` note is really high!
+Wait a minute --- weren't we just talking about singing notes that were too
+high at half their original frequency? We can do that here. The result is a
+note we've already seen:
+
+```{python}
+print(thriceMiddleC.hz/2)
+print(g4.hz)
+```
+
+```{python}
+#| echo: false
+PlayNotes(middleC.hz, g4.hz)
+```
+
+In the end, we got G4 by multiplying our original frequency by $3/2$. What if
+we keep applying this process to find more notes? Let's not even worry
+about the specific frequencies (like `261.63`) for a moment. We'll start
+with a frequency of $1$. This makes our next frequency $3/2$. Taking this
+new frequency and again multiplying it by $3/2$, we get $9/4$. But that
+again puts us a little bit high: $9/4 > 2$. We can apply our earlier trick
+and divide the result, getting $9/16$.
+
+```{python}
+from fractions import Fraction
+
+note = Fraction(1, 1)
+seen = {note}
+while len(seen) < 6:
+    new_note = note * 3 / 2
+    if new_note > 2:
+        new_note = new_note / 2
+
+    seen.add(new_note)
+    note = new_note
+```
+
+For an admittedly handwavy reason, let's also throw in one note that we
+get from going _backwards_: dividing by $2/3$ instead of multiplying.
+This division puts us below our original frequency, so let's double it.
+
+```{python}
+# Throw in one more by going *backwards*. More on that in a bit.
+seen.add(Fraction(2/3) * 2)
+fractions = sorted(list(seen))
+fractions
+```
+
+```{python}
+frequencies = [middleC.hz * float(frac) for frac in fractions]
+frequencies
+```
+
+```{python}
+steps = [frequencies[i+1]/frequencies[i] for i in range(len(frequencies)-1)]
+minstep = min(steps)
+print([math.log(step)/math.log(minstep) for step in steps])
+```
+
+Since peaks and troughs
+in the final result arise when peaks and troughs in the individual waves align,
+we want to pick two frequencies that align with a nice pattern.
+
+But that begs the question: what determines
+how quickly the pattern of two notes played together repeats?
+
+We can look at things geometrically, by thinking about the distance
+between two successive peaks in a single note. This is called the
+*wavelength* of a wave. Take a wave with some wavelength $w$.
+If we start at a peak, then travel a distance of $w$ from where we started,
+there ought to be another peak. Arriving at a distance of $2w$ (still counting
+from where we started), we'll see another peak. Continuing in the same pattern,
+we'll see peaks at distances of $3w$, $4w$, and so on. For a second wave
+with wavelength $v$, the same will be true: peaks at $v$, $2v$, $3v$, and so on.
+
+If we travel a distance that happens to be a multiple of both $w$ and $v$,
+then we'll have a place where both peaks are present. At that point, the
+pattern starts again. Mathematically, we can
+state this as follows:
+
+$$
+nw = mv,\ \text{for some integers}\ n, m
+$$
+
+As we decided above, we'll try to find a combination of wavelengths/frequencies
+where the repetition happens early.
+
+__TODO:__ Follow the logic from Digit Sum Patterns
+
+The number of iterations of the smaller wave before we reach a cycle is:
+
+$$
+k = \frac{w}{\text{gcd}(w, v)}
+$$
+
+
+```{python}
+Superimpose(Frequency(261.63), Frequency(261.63*2))
+```
+
+```{python}
+Superimpose(Frequency(261.63*4), Frequency(392.445*4))
+```
+
+```{python}
+VerticalStack(
+    Frequency(440*8),
+    Frequency(450*8),
+    Superimpose(Frequency(440*8), Frequency(450*8))
+)
+```
+
+
+```{python}
+from enum import Enum
+class Note(Enum):
+    C = 0
+    Cs = 1
+    D = 2
+    Ds = 3
+    E = 4
+    F = 5
+    Fs = 6
+    G = 7
+    Gs = 8
+    A = 9
+    As = 10
+    B = 11
+
+    def __add__(self, other):
+        return Note((self.value + other.value) % 12)
+
+    def __sub__(self, other):
+        return Interval((self.value - other.value + 12) % 12)
+```
+
+```{python, echo=false}
+class MyClass:
+    def _repr_svg_(self):
+        return """<svg xmlns="http://www.w3.org/2000/svg"
+                       width="120" height="120" viewBox="0 0 120 120">
+          <circle cx="60" cy="60" r="50" fill="red"/>
+        </svg>"""
+
+MyClass()
+```

content/blog/music_theory/playsound.js

@@ -0,0 +1,15 @@
+window.addEventListener("load", (event) => {
+    for (const elt of document.getElementsByClassName("mt-sound-play-button")) {
+        elt.addEventListener("click", (event) => {
+            const audioCtx = new (window.AudioContext || window.webkitAudioContext)();
+            for (const freq of event.target.getAttribute("data-sound-info").split(",")) {
+                const oscillator = audioCtx.createOscillator();
+                oscillator.type = "sine";      // waveform: sine, square, sawtooth, triangle
+                oscillator.frequency.value = parseInt(freq); // Hz
+                oscillator.connect(audioCtx.destination);
+                oscillator.start();
+                oscillator.stop(audioCtx.currentTime + 2); // stop after 1 second
+            }
+        });
+    }
+});

content/blog/music_theory/svg-inline.lua

@@ -0,0 +1,13 @@
+function Image(el)
+  local src = el.src
+  if src:match("%.svg$") then
+    local alt = el.caption and pandoc.utils.stringify(el.caption) or ""
+    local obj = string.format(
+      '{{< inlinesvg "%s" "%s" >}}',
+      src, alt
+    )
+    return pandoc.RawInline("html", obj)
+  else
+    return el
+  end
+end

content/blog/music_theory/to-parens.lua

@@ -0,0 +1,5 @@
+function Math(el)
+  if el.mathtype == "InlineMath" then
+    return pandoc.RawInline("markdown", "\\(" .. el.text .. "\\)")
+  end
+end

content/series/static-program-analysis-in-agda/_index.md

@@ -6,6 +6,6 @@ summary = """
   in Agda. The goal is to have a formally verified, yet executable, static
   analyzer for a simple language.
   """
-status = "ongoing"
+status = "complete"
 divider = ": "
 +++

convert.rb

@@ -25,13 +25,16 @@ class KatexRenderer
   end
 
   def substitute(content)
+    found_any = false
     rendered = content.gsub /\\\(((?:[^\\]|\\[^\)])*)\\\)/ do |match|
+      found_any = true
       render(false, $~[1])
     end
     rendered = rendered.gsub /\$\$((?:[^\$]|$[^\$])*)\$\$/ do |match|
+      found_any = true
       render(true, $~[1])
     end
-    return rendered
+    return rendered, found_any
   end
 end
 
@@ -58,8 +61,20 @@ renderer = KatexRenderer.new(katex)
 files.each do |file|
   puts "Rendering file: #{file}"
   document = Nokogiri::HTML.parse(File.open(file))
+  found_any = false
   document.search('//*[not(ancestor-or-self::code or ancestor-or-self::script)]/text()').each do |t|
-    t.replace(renderer.substitute(t.content))
+    rendered, found_any_in_text = renderer.substitute(t.content)
+    found_any ||= found_any_in_text
+    t.replace(rendered)
   end
+
+  # If we didn't find any mathematical equations, no need to include KaTeX CSS.
+  # Disabled here because Bergamot technically doesn't require math blocks
+  # on the page but does need the CSS.
+  #
+  # unless found_any
+  #   document.css('link[href$="katex.css"], link[href$="katex.min.css"]').each(&:remove)
+  # end
+
   File.write(file, document.to_html(encoding: 'UTF-8'))
 end

layouts/shortcodes/donate_css.html

@@ -1,2 +1,2 @@
-{{ $style := resources.Get "scss/donate.scss" | resources.ToCSS | resources.Minify }}
+{{ $style := resources.Get "scss/donate.scss" | css.Sass | resources.Minify }}
 <link rel="stylesheet" href="{{ $style.Permalink }}">

layouts/shortcodes/gmachine_css.html

@@ -1,2 +1,2 @@
-{{ $style := resources.Get "scss/gmachine.scss" | resources.ToCSS | resources.Minify }}
+{{ $style := resources.Get "scss/gmachine.scss" | css.Sass | resources.Minify }}
 <link rel="stylesheet" href="{{ $style.Permalink }}">

layouts/shortcodes/inlinesvg.html

@@ -0,0 +1 @@
+<object type="image/svg+xml" data="{{ .Get 0 }}" aria-label="{{ .Get 1 }}"></object>

layouts/shortcodes/playsound.html

@@ -0,0 +1 @@
+<button class="mt-sound-play-button" data-sound-info="{{ .Get 0 }}">Play</button>

layouts/shortcodes/stack_css.html

@@ -1,2 +1,2 @@
-{{ $style := resources.Get "scss/stack.scss" | resources.ToCSS | resources.Minify }}
+{{ $style := resources.Get "scss/stack.scss" | css.Sass | resources.Minify }}
 <link rel="stylesheet" href="{{ $style.Permalink }}">

layouts/thevoid/baseof.html

@@ -3,7 +3,7 @@
 <html lang="{{ .Site.Language.Lang }}">
     {{- partial "head.html" . -}}
     <body>
-        {{ $voidcss := resources.Get "scss/thevoid.scss" | resources.ToCSS | resources.Minify }}
+        {{ $voidcss := resources.Get "scss/thevoid.scss" | css.Sass | resources.Minify }}
         <link rel="stylesheet" href="{{ $voidcss.Permalink }}">
         {{- partial "header.html" . -}}
         <div class="container"><hr class="header-divider"></div>