Compare commits
23 Commits
07408d01a9
...
music-theo
| Author | SHA1 | Date | |
|---|---|---|---|
| 3816599d7a | |||
| 64b2fec8c0 | |||
| e4e513faf0 | |||
| a8f69a71f0 | |||
| 9660c0d665 | |||
| 1e5ed34f0f | |||
| 7fbd4ea9f8 | |||
| 6fd1e1962b | |||
| 62c338e382 | |||
| 40ea9ec637 | |||
| 787e194d41 | |||
| 71162e2db9 | |||
| 43debc65e4 | |||
| b07ea85b70 | |||
| 06e8b8e022 | |||
| 647f47a5f3 | |||
| 36e4feb668 | |||
| 11be991946 | |||
| a8c2b1d05a | |||
| fb46142e9d | |||
| 0b33d03b73 | |||
| 804147caef | |||
| d847d20666 |
3
.gitignore
vendored
3
.gitignore
vendored
@@ -1 +1,4 @@
|
|||||||
**/build/*
|
**/build/*
|
||||||
|
|
||||||
|
/.quarto/
|
||||||
|
**/*.quarto_ipynb
|
||||||
|
|||||||
@@ -3,11 +3,11 @@ GEM
|
|||||||
specs:
|
specs:
|
||||||
duktape (2.7.0.0)
|
duktape (2.7.0.0)
|
||||||
execjs (2.9.1)
|
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)
|
mini_portile2 (~> 2.8.2)
|
||||||
racc (~> 1.4)
|
racc (~> 1.4)
|
||||||
racc (1.8.0)
|
racc (1.8.1)
|
||||||
|
|
||||||
PLATFORMS
|
PLATFORMS
|
||||||
ruby
|
ruby
|
||||||
|
|||||||
3
_quarto.yml
Normal file
3
_quarto.yml
Normal file
@@ -0,0 +1,3 @@
|
|||||||
|
format:
|
||||||
|
gfm:
|
||||||
|
variant: +yaml_metadata_block
|
||||||
2
agda.rb
2
agda.rb
@@ -23,7 +23,7 @@ class AgdaContext
|
|||||||
return @file_infos[file] if @file_infos.include? file
|
return @file_infos[file] if @file_infos.include? file
|
||||||
|
|
||||||
@file_infos[file] = line_infos = {}
|
@file_infos[file] = line_infos = {}
|
||||||
unless File.exists?(file)
|
unless File.exist?(file)
|
||||||
return line_infos
|
return line_infos
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|||||||
@@ -43,7 +43,7 @@ files.each do |file|
|
|||||||
tags = []
|
tags = []
|
||||||
group = 1
|
group = 1
|
||||||
draft = false
|
draft = false
|
||||||
next unless File.exists?(file)
|
next unless File.exist?(file)
|
||||||
value = File.size(file)
|
value = File.size(file)
|
||||||
url = file.gsub(/^content/, "https://danilafe.com").delete_suffix("/index.md").delete_suffix(".md")
|
url = file.gsub(/^content/, "https://danilafe.com").delete_suffix("/index.md").delete_suffix(".md")
|
||||||
File.readlines(file).each do |l|
|
File.readlines(file).each do |l|
|
||||||
|
|||||||
@@ -26,7 +26,7 @@ files = ARGV
|
|||||||
code_paths = Dir.entries(root_path).select do |f|
|
code_paths = Dir.entries(root_path).select do |f|
|
||||||
File.directory?(File.join(root_path, f)) and f != '.' and f != '..'
|
File.directory?(File.join(root_path, f)) and f != '.' and f != '..'
|
||||||
end.to_set
|
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
|
# Extending code_paths from submodules.json means that nested Agda modules
|
||||||
# have their root dir correctly set.
|
# have their root dir correctly set.
|
||||||
|
|
||||||
|
|||||||
@@ -5,7 +5,8 @@ require 'nokogiri'
|
|||||||
require 'set'
|
require 'set'
|
||||||
|
|
||||||
# 1) Process all files passed in from the command line
|
# 1) Process all files passed in from the command line
|
||||||
files = ARGV
|
svgpath = ARGV[0]
|
||||||
|
files = ARGV[1..]
|
||||||
|
|
||||||
# 2) Extract used Feather icons
|
# 2) Extract used Feather icons
|
||||||
used_icons = Set.new
|
used_icons = Set.new
|
||||||
@@ -27,7 +28,7 @@ end
|
|||||||
puts "Found #{used_icons.size} unique icons: #{used_icons.to_a.join(', ')}"
|
puts "Found #{used_icons.size} unique icons: #{used_icons.to_a.join(', ')}"
|
||||||
|
|
||||||
# 3) Load the full feather-sprite.svg as XML
|
# 3) Load the full feather-sprite.svg as XML
|
||||||
sprite_doc = File.open("feather-sprite.svg", "r:UTF-8") { |f| Nokogiri::XML(f) }
|
sprite_doc = File.open(svgpath, "r:UTF-8") { |f| Nokogiri::XML(f) }
|
||||||
|
|
||||||
# 4) Create a new SVG with only the required symbols
|
# 4) Create a new SVG with only the required symbols
|
||||||
new_svg = Nokogiri::XML::Document.new
|
new_svg = Nokogiri::XML::Document.new
|
||||||
@@ -43,8 +44,6 @@ sprite_doc.css("symbol").each do |symbol_node|
|
|||||||
end
|
end
|
||||||
|
|
||||||
# 5) Save the subset sprite
|
# 5) Save the subset sprite
|
||||||
File.open("custom-sprite.svg", "w:UTF-8") do |f|
|
File.open(svgpath, "w:UTF-8") do |f|
|
||||||
f.write(new_svg.to_xml)
|
f.write(new_svg.to_xml)
|
||||||
end
|
end
|
||||||
|
|
||||||
puts "Generated custom-sprite.svg with only the required icons."
|
|
||||||
|
|||||||
@@ -1,12 +1,9 @@
|
|||||||
import os
|
import os
|
||||||
|
import sys
|
||||||
from bs4 import BeautifulSoup
|
from bs4 import BeautifulSoup
|
||||||
from fontTools.subset import Subsetter, Options
|
from fontTools.subset import Subsetter, Options
|
||||||
from fontTools.ttLib import TTFont
|
from fontTools.ttLib import TTFont
|
||||||
|
|
||||||
# Directories
|
|
||||||
HTML_DIR = "." # Directory with .html files
|
|
||||||
FONT_DIR = "." # Directory containing fonts to be modified
|
|
||||||
|
|
||||||
FONT_EXTENSIONS = (".ttf", ".woff", ".woff2", ".otf") # Font file types
|
FONT_EXTENSIONS = (".ttf", ".woff", ".woff2", ".otf") # Font file types
|
||||||
|
|
||||||
def extract_text_from_html(file_path):
|
def extract_text_from_html(file_path):
|
||||||
@@ -15,14 +12,11 @@ def extract_text_from_html(file_path):
|
|||||||
soup = BeautifulSoup(f.read(), "html.parser")
|
soup = BeautifulSoup(f.read(), "html.parser")
|
||||||
return soup.get_text()
|
return soup.get_text()
|
||||||
|
|
||||||
def get_used_characters(directory):
|
def get_used_characters(files):
|
||||||
"""Collect unique characters from all .html files in the given directory."""
|
"""Collect unique characters from all .html files in the given directory."""
|
||||||
char_set = set()
|
char_set = set()
|
||||||
for root, _, files in os.walk(directory):
|
|
||||||
for file in files:
|
for file in files:
|
||||||
if file.endswith(".html"):
|
text = extract_text_from_html(file)
|
||||||
full_path = os.path.join(root, file)
|
|
||||||
text = extract_text_from_html(full_path)
|
|
||||||
char_set.update(text)
|
char_set.update(text)
|
||||||
return "".join(sorted(char_set))
|
return "".join(sorted(char_set))
|
||||||
|
|
||||||
@@ -65,10 +59,10 @@ def subset_font_in_place(font_path, characters):
|
|||||||
print(f"Subsetted font in place: {font_path}")
|
print(f"Subsetted font in place: {font_path}")
|
||||||
|
|
||||||
if __name__ == "__main__":
|
if __name__ == "__main__":
|
||||||
used_chars = get_used_characters(HTML_DIR)
|
used_chars = get_used_characters(sys.argv[2:])
|
||||||
print(f"Extracted {len(used_chars)} unique characters from HTML files.")
|
print(f"Extracted {len(used_chars)} unique characters from {len(sys.argv[2:])} HTML files.")
|
||||||
|
|
||||||
font_files = find_font_files(FONT_DIR)
|
font_files = find_font_files(sys.argv[1])
|
||||||
print(f"Found {len(font_files)} font files to subset.")
|
print(f"Found {len(font_files)} font files to subset.")
|
||||||
|
|
||||||
for font_file in font_files:
|
for font_file in font_files:
|
||||||
|
|||||||
@@ -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_
|
our system. A single rule takes care of figuring the types of _all_
|
||||||
variables.
|
variables.
|
||||||
|
|
||||||
{{< todo >}}
|
> [!TODO]
|
||||||
The rest of this, but mostly statements.
|
> The rest of this, but mostly statements.
|
||||||
{{< /todo >}}
|
|
||||||
|
|
||||||
### This Page at a Glance
|
### This Page at a Glance
|
||||||
#### Metavariables
|
#### Metavariables
|
||||||
|
|||||||
591
content/blog/chapel_runtime_types.md
Normal file
591
content/blog/chapel_runtime_types.md
Normal file
@@ -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).
|
||||||
@@ -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
|
which is the language I'll use in this article. Below are a few resources
|
||||||
that should help you get up to speed.
|
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
|
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
|
`B -> a`, if `F` is a base functor of the type `B`. However, what if
|
||||||
|
|||||||
484
content/blog/music_theory/index.qmd
Normal file
484
content/blog/music_theory/index.qmd
Normal file
@@ -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()
|
||||||
|
```
|
||||||
15
content/blog/music_theory/playsound.js
Normal file
15
content/blog/music_theory/playsound.js
Normal file
@@ -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
|
||||||
|
}
|
||||||
|
});
|
||||||
|
}
|
||||||
|
});
|
||||||
13
content/blog/music_theory/svg-inline.lua
Normal file
13
content/blog/music_theory/svg-inline.lua
Normal file
@@ -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
|
||||||
5
content/blog/music_theory/to-parens.lua
Normal file
5
content/blog/music_theory/to-parens.lua
Normal file
@@ -0,0 +1,5 @@
|
|||||||
|
function Math(el)
|
||||||
|
if el.mathtype == "InlineMath" then
|
||||||
|
return pandoc.RawInline("markdown", "\\(" .. el.text .. "\\)")
|
||||||
|
end
|
||||||
|
end
|
||||||
19
convert.rb
19
convert.rb
@@ -25,13 +25,16 @@ class KatexRenderer
|
|||||||
end
|
end
|
||||||
|
|
||||||
def substitute(content)
|
def substitute(content)
|
||||||
|
found_any = false
|
||||||
rendered = content.gsub /\\\(((?:[^\\]|\\[^\)])*)\\\)/ do |match|
|
rendered = content.gsub /\\\(((?:[^\\]|\\[^\)])*)\\\)/ do |match|
|
||||||
|
found_any = true
|
||||||
render(false, $~[1])
|
render(false, $~[1])
|
||||||
end
|
end
|
||||||
rendered = rendered.gsub /\$\$((?:[^\$]|$[^\$])*)\$\$/ do |match|
|
rendered = rendered.gsub /\$\$((?:[^\$]|$[^\$])*)\$\$/ do |match|
|
||||||
|
found_any = true
|
||||||
render(true, $~[1])
|
render(true, $~[1])
|
||||||
end
|
end
|
||||||
return rendered
|
return rendered, found_any
|
||||||
end
|
end
|
||||||
end
|
end
|
||||||
|
|
||||||
@@ -58,8 +61,20 @@ renderer = KatexRenderer.new(katex)
|
|||||||
files.each do |file|
|
files.each do |file|
|
||||||
puts "Rendering file: #{file}"
|
puts "Rendering file: #{file}"
|
||||||
document = Nokogiri::HTML.parse(File.open(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|
|
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
|
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'))
|
File.write(file, document.to_html(encoding: 'UTF-8'))
|
||||||
end
|
end
|
||||||
|
|||||||
@@ -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 }}">
|
<link rel="stylesheet" href="{{ $style.Permalink }}">
|
||||||
|
|||||||
@@ -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 }}">
|
<link rel="stylesheet" href="{{ $style.Permalink }}">
|
||||||
|
|||||||
1
layouts/shortcodes/inlinesvg.html
Normal file
1
layouts/shortcodes/inlinesvg.html
Normal file
@@ -0,0 +1 @@
|
|||||||
|
<object type="image/svg+xml" data="{{ .Get 0 }}" aria-label="{{ .Get 1 }}"></object>
|
||||||
1
layouts/shortcodes/playsound.html
Normal file
1
layouts/shortcodes/playsound.html
Normal file
@@ -0,0 +1 @@
|
|||||||
|
<button class="mt-sound-play-button" data-sound-info="{{ .Get 0 }}">Play</button>
|
||||||
@@ -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 }}">
|
<link rel="stylesheet" href="{{ $style.Permalink }}">
|
||||||
|
|||||||
@@ -3,7 +3,7 @@
|
|||||||
<html lang="{{ .Site.Language.Lang }}">
|
<html lang="{{ .Site.Language.Lang }}">
|
||||||
{{- partial "head.html" . -}}
|
{{- partial "head.html" . -}}
|
||||||
<body>
|
<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 }}">
|
<link rel="stylesheet" href="{{ $voidcss.Permalink }}">
|
||||||
{{- partial "header.html" . -}}
|
{{- partial "header.html" . -}}
|
||||||
<div class="container"><hr class="header-divider"></div>
|
<div class="container"><hr class="header-divider"></div>
|
||||||
|
|||||||
Submodule themes/vanilla updated: 2b7645a572...952502e690
Reference in New Issue
Block a user