From 0a6e73df192025d0f634cee788881b5d864f7f55 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 26 Sep 2022 12:58:51 -0500 Subject: [PATCH] layout upd --- .gitignore | 1 + Justfile | 3 + assets/sass/_content.scss | 2 +- assets/sass/_footer.scss | 3 + blog.agda-lib | 3 + content/about/_index.md | 66 ++++-- ...2022-09-20-higher-inductive-types.lagda.md | 189 ++++++++++++++++++ layouts/_default/baseof.html | 2 +- layouts/partials/left-nav.html | 2 + static/robots.txt | 0 10 files changed, 249 insertions(+), 22 deletions(-) create mode 100644 assets/sass/_footer.scss create mode 100644 blog.agda-lib create mode 100644 content/posts/2022-09-20-higher-inductive-types.lagda.md create mode 100644 static/robots.txt diff --git a/.gitignore b/.gitignore index 51e8812..ac7ca6e 100644 --- a/.gitignore +++ b/.gitignore @@ -4,3 +4,4 @@ .hugo_build.lock .direnv +*.agdai diff --git a/Justfile b/Justfile index 2167372..491ab13 100644 --- a/Justfile +++ b/Justfile @@ -1,2 +1,5 @@ serve: hugo serve --bind 0.0.0.0 --buildDrafts + +linkcheck: + wget --spider -r -nd -nv -H -l 1 http://localhost:1313 diff --git a/assets/sass/_content.scss b/assets/sass/_content.scss index 168bc83..d2e4d10 100644 --- a/assets/sass/_content.scss +++ b/assets/sass/_content.scss @@ -1,4 +1,4 @@ -// @import "home"; +@import "footer"; html { min-height: 100vh; diff --git a/assets/sass/_footer.scss b/assets/sass/_footer.scss new file mode 100644 index 0000000..30f5ebd --- /dev/null +++ b/assets/sass/_footer.scss @@ -0,0 +1,3 @@ +footer { + font-size: 0.85rem; +} diff --git a/blog.agda-lib b/blog.agda-lib new file mode 100644 index 0000000..feecedb --- /dev/null +++ b/blog.agda-lib @@ -0,0 +1,3 @@ +name: blog +depend: standard-library +include: content/posts diff --git a/content/about/_index.md b/content/about/_index.md index 455b973..f602c53 100644 --- a/content/about/_index.md +++ b/content/about/_index.md @@ -7,36 +7,62 @@ type = "generic" layout = "single" +++ -Hi there! I'm an incoming graduate student at the University of Minnesota. I -currently work as a Software Developer at [AWS][13] (previously at [SIFT][11]). My -computing-related interests lie in programming language design and formal -verification, systems security, cryptography, and distributed systems. Some of the projects I've been working on in my free time include: +# About Me -- [**Leanshot**][6], a Linux screen capture tool. -- [**Garbage**][7], a CLI interface to the trash can API. +Hi there! I'm a first-year master's student at the University of Minnesota. I +also currently work as a Software Developer at [AWS] (previously at [SIFT]). +My computing-related interests lie in programming language design and formal +verification, systems security, cryptography, and distributed +systems. + + + +### Research + +Currently, I'm learning about [cubical type theory][cubical]. I'll probably +write some blog posts as I learn more. My advisor is [Favonia]. + +### University Involvement + +- **[GopherHack]**. I'm an officer at the GopherHack organization, hoping to + grow a CTF community at the University. +- **[PL Seminar]**. A group focused on reading and discussing + programming-language-related papers + +### Open-source Projects + +Some of the projects I've been working on in my free time include: + +- **[Leanshot]**. A Linux screen capture tool. +- **[Garbage]**. A CLI interface to the trash can API. More can be found on [this page][12] or my public [Gitea][2]. -I've also started making an increased effort at using and supporting [FOSS][8], +I've also started making an increased effort at using and supporting [FOSS], and other software that're not predatory towards users. As a part of this effort, I'm also self-hosting and rewriting some of the services and software that I use regularly. Find out what I'm using [here][9]. -I'm also an avid rhythm game player and beatmap creator, mostly involved with -the free-to-play game [osu!][3]. Check out some of my beatmaps on my [osu! -userpage][4]. +### Hobbies + +I'm also an avid rhythm game player and beatmap creator, mostly involved with +the free-to-play game [osu!]. Check out some of my beatmaps on my osu! +[userpage]. + +I also enjoy playing badminton 🏸 at the rec. -[1]: https://keybase.io/michaelz/pgp_keys.asc?fingerprint=925ecc02890d5cdae26180d4bda47a31a3c8ee6b [2]: https://git.mzhang.io/explore -[3]: https://osu.ppy.sh -[4]: https://osu.ppy.sh/u/2688103 -[5]: https://libera.chat -[6]: https://git.mzhang.io/michael/leanshot -[7]: https://git.sr.ht/~iptq/garbage -[8]: https://en.wikipedia.org/wiki/Free_and_open-source_software [9]: setup [10]: pgp.txt -[11]: https://www.sift.net/ [12]: ../projects -[13]: https://aws.amazon.com/ +[aws]: https://aws.amazon.com/ +[cubical]: https://ncatlab.org/nlab/show/cubical+type+theory +[favonia]: https://favonia.org/ +[foss]: https://en.wikipedia.org/wiki/Free_and_open-source_software +[garbage]: https://git.sr.ht/~mzhang/garbage +[gopherhack]: https://gopherhack.com +[leanshot]: https://git.sr.ht/~mzhang/leanshot +[osu!]: https://osu.ppy.sh +[pl seminar]: https://umn-plseminar.github.io +[sift]: https://www.sift.net/ +[userpage]: https://osu.ppy.sh/u/2688103 diff --git a/content/posts/2022-09-20-higher-inductive-types.lagda.md b/content/posts/2022-09-20-higher-inductive-types.lagda.md new file mode 100644 index 0000000..9539639 --- /dev/null +++ b/content/posts/2022-09-20-higher-inductive-types.lagda.md @@ -0,0 +1,189 @@ ++++ +title = "Higher Inductive Types" +slug = "higher-inductive-types" +date = 2022-09-20 +tags = ["type-theory"] +toc = true +math = true +draft = true ++++ + +**Higher inductive types (HIT)** are central to developing cubical type theory. +What this article will try to do is develop an approach to understanding higher +inductive types based on my struggles to learn the topic. + + + +Ordinary inductive types +--- + +So first off, what is an inductive type? These are a kind of data structure +that's commonly used in _functional programming_. For example, consider the +definition of natural numbers (`Nat`): + +```agda +data Nat : Set where + zero : Nat + suc : Nat → Nat +``` + +This defines all `Nat`s as either zero, or one more than another `Nat`. For +example, here's the first few natural numbers and their corresponding +representation using this data structure: + +```txt +0 zero +1 suc zero +2 suc (suc zero) +3 suc (suc (suc zero)) +4 suc (suc (suc (suc zero))) +5 suc (suc (suc (suc (suc zero)))) +``` + +Why is this representation useful? Well, if you remember **proof by induction** +from maybe high school geometry, you'll recall that we can prove things about +all natural numbers by simply proving that it's true for the _base case_ 0, and +then proving that it's true for any _inductive case_ $n$, given that the +previous case $n - 1$ is true. + +This kind of definition of natural numbers makes this induction structure much +more clear. For example, look at the definition of a tree: + +```agda +data Tree (A : Set) : Set where + leaf : A → Tree A + left : Tree A → Tree A + right : Tree A → Tree A +``` + +We can do induction on trees by simply proving it's true for (1) the base case, +(2) the left case, and (3) the right case. In fact, all inductive data +structures have this kind of induction principle. So say you wanted to prove +that $1 + 2 + 3 + \cdots + n = \frac{n\cdot(n+1)}{2}$ for all $n \in +\mathbb{N}$, then you could say: + +
+(click here for boring requisites) + +```agda +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; module ≡-Reasoning) +open ≡-Reasoning using (begin_; _≡⟨_⟩_; _≡⟨⟩_; step-≡; _∎) +open import Data.Product using (_×_) +open import Data.Nat using (ℕ; zero; suc; _+_; _*_) +open import Data.Nat.DivMod using (_/_; 0/n≡0; n/n≡1; m*n/n≡m) +open import Data.Nat.Properties using (+-assoc; *-identityˡ; *-comm; *-distribʳ-+; +-comm) + +sum-to-n : ℕ → ℕ +sum-to-n zero = zero +sum-to-n (suc x) = (suc x) + (sum-to-n x) + +distrib-/ : ∀ (a b c : ℕ) → a / c + b / c ≡ (a + b) / c +distrib-/ zero b c = + begin + zero / c + b / c + ≡⟨ cong (_+ b / c) (0/n≡0 c) ⟩ + b / c + ≡⟨ cong (_/ c) refl ⟩ + (zero + b) / c + ∎ +distrib-/ (suc a) b c = + begin + (1 + a) / c + b / c + ≡⟨ cong (_+ b / c) (sym (distrib-/ 1 a c)) ⟩ + 1 / c + a / c + b / c + ≡⟨ +-assoc (1 / c) (a / c) (b / c) ⟩ + 1 / c + (a / c + b / c) + ≡⟨ cong (1 / c +_) (distrib-/ a b c) ⟩ + 1 / c + (a + b) / c + ≡⟨ distrib-/ 1 (a + b) c ⟩ + (suc a + b) / c + ∎ +``` + +
+ +```agda +-- Here's the proposition we want to prove: +our-prop : ∀ (n : ℕ) → sum-to-n n ≡ n * (n + 1) / 2 + +-- How do we prove this? +-- Well, we know it's true for zero: +base-case : sum-to-n 0 ≡ 0 * (0 + 1) / 2 +base-case = refl + +-- The next part is proving that it's true for any n + 1, given that it's true +-- for the previous case n: +inductive-case : ∀ {n : ℕ} + → (inductive-hypothesis : sum-to-n n ≡ n * (n + 1) / 2) + → sum-to-n (suc n) ≡ (suc n) * (suc n + 1) / 2 +``` + +
+Inductive case proof, expand if you're interested + +```agda +inductive-case {n} p = + begin + sum-to-n (suc n) + ≡⟨⟩ -- Expanding definition of sum-to-n + suc n + sum-to-n n + ≡⟨ cong (suc n +_) p ⟩ -- Substituting the previous case + suc n + n * (n + 1) / 2 + ≡⟨ cong (_+ n * (n + 1) / 2) (sym (m*n/n≡m (suc n) 2)) ⟩ + (suc n * 2) / 2 + (n * (n + 1)) / 2 + ≡⟨ distrib-/ (suc n * 2) (n * (n + 1)) 2 ⟩ + (suc n * 2 + n * (n + 1)) / 2 + ≡⟨ cong (_/ 2) (cong (_+ n * (n + 1)) (*-comm (suc n) 2)) ⟩ + (2 * suc n + n * (n + 1)) / 2 + ≡⟨ cong (_/ 2) (cong (2 * suc n +_) (cong (n *_) (+-comm n 1))) ⟩ + (2 * suc n + n * suc n) / 2 + ≡⟨ cong (_/ 2) (sym (*-distribʳ-+ (suc n) 2 n)) ⟩ + (1 + suc n) * suc n / 2 + ≡⟨ cong (_/ 2) (cong (_* suc n) (+-comm 1 (suc n))) ⟩ + (suc n + 1) * suc n / 2 + ≡⟨ cong (_/ 2) (*-comm (suc n + 1) (suc n)) ⟩ + (suc n) * (suc n + 1) / 2 + ∎ +``` + +
+ +So now that we have both the base and inductive cases, let's combine it using +this: + +```agda +-- Given any natural number property (p : ℕ → Set), if... +any-nat-prop : (p : ℕ → Set) + -- ...it's true for the base case and... + → p 0 + -- ...it's true for the inductive case... + → (∀ {n : ℕ} (a : p n) → p (suc n)) + -- ...then the property is true for all naturals. + → (∀ (n : ℕ) → p n) +any-nat-prop p base _ zero = base +any-nat-prop p base ind (suc n) = ind (any-nat-prop p base ind n) +``` + +Then: + +``` +our-prop = any-nat-prop + (λ n → sum-to-n n ≡ n * (n + 1) / 2) + base-case inductive-case +``` + +Using Agda, we can see that this type-checks correctly. + +**TODO:** Ensure totality + +Higher inductive types +--- + +Moving on, we want to know what _higher_ inductive types brings to the table. To +illustrate its effect, let's consider the following scenario: suppose you have + +#### References + +- [nLab](https://ncatlab.org/nlab/show/higher+inductive+type) +- Section 2.5 of [Favonia's thesis](https://favonia.org/files/thesis.pdf) +- [Quotient Types for Programmers](https://www.hedonisticlearning.com/posts/quotient-types-for-programmers.html) diff --git a/layouts/_default/baseof.html b/layouts/_default/baseof.html index f4c264b..f0c7247 100644 --- a/layouts/_default/baseof.html +++ b/layouts/_default/baseof.html @@ -25,7 +25,7 @@