layout upd
This commit is contained in:
parent
cc538bc7f3
commit
0a6e73df19
|
|
@ -4,3 +4,4 @@
|
|||
|
||||
.hugo_build.lock
|
||||
.direnv
|
||||
*.agdai
|
||||
|
|
|
|||
3
Justfile
3
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
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
// @import "home";
|
||||
@import "footer";
|
||||
|
||||
html {
|
||||
min-height: 100vh;
|
||||
|
|
|
|||
|
|
@ -0,0 +1,3 @@
|
|||
footer {
|
||||
font-size: 0.85rem;
|
||||
}
|
||||
|
|
@ -0,0 +1,3 @@
|
|||
name: blog
|
||||
depend: standard-library
|
||||
include: content/posts
|
||||
|
|
@ -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. <!-- more
|
||||
--> 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.
|
||||
|
||||
<!-- more -->
|
||||
|
||||
### 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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
||||
<!--more-->
|
||||
|
||||
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:
|
||||
|
||||
<details>
|
||||
<summary>(click here for boring requisites)</summary>
|
||||
|
||||
```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
|
||||
∎
|
||||
```
|
||||
|
||||
</details>
|
||||
|
||||
```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
|
||||
```
|
||||
|
||||
<details>
|
||||
<summary>Inductive case proof, expand if you're interested</summary>
|
||||
|
||||
```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
|
||||
∎
|
||||
```
|
||||
|
||||
</details>
|
||||
|
||||
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)
|
||||
|
|
@ -25,7 +25,7 @@
|
|||
</div>
|
||||
|
||||
<footer>
|
||||
<p style="margin: 0;">
|
||||
<p>
|
||||
Blog code licensed under <a
|
||||
href="https://www.gnu.org/licenses/gpl-3.0.txt"
|
||||
target="_blank">[GPL-3.0]</a>.
|
||||
|
|
|
|||
|
|
@ -6,6 +6,8 @@
|
|||
</a>
|
||||
<div class="bio">
|
||||
{{ os.ReadFile "layouts/partials/left-nav.md" | .RenderString }}
|
||||
|
||||
<a href="/about">More »</a>
|
||||
</div>
|
||||
</div>
|
||||
</nav>
|
||||
|
|
|
|||
Loading…
Reference in New Issue