From 5850483297234d2fefdb5971718f98eba79a70c4 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Tue, 4 Jul 2023 04:24:23 -0500 Subject: [PATCH] new blog post about nginx --- Justfile | 2 +- .../posts/2023-05-06-equivalences.lagda.md | 82 ++++++-- .../2023-07-04-learn-by-implementing-nginx.md | 190 ++++++++++++++++++ 3 files changed, 261 insertions(+), 13 deletions(-) create mode 100644 content/posts/2023-07-04-learn-by-implementing-nginx.md diff --git a/Justfile b/Justfile index 491ab13..953f4bf 100644 --- a/Justfile +++ b/Justfile @@ -1,5 +1,5 @@ serve: - hugo serve --bind 0.0.0.0 --buildDrafts + hugo serve --bind 0.0.0.0 --port 8313 --buildDrafts linkcheck: wget --spider -r -nd -nv -H -l 1 http://localhost:1313 diff --git a/content/posts/2023-05-06-equivalences.lagda.md b/content/posts/2023-05-06-equivalences.lagda.md index 3926e77..74ce698 100644 --- a/content/posts/2023-05-06-equivalences.lagda.md +++ b/content/posts/2023-05-06-equivalences.lagda.md @@ -1,11 +1,14 @@ -+++ -title = "Equivalences" -slug = "equivalences" -date = 2023-05-06 -tags = ["type-theory", "agda", "hott"] -math = true -draft = true -+++ +--- +title: "Equivalences" +slug: "equivalences" +date: 2023-05-06 +tags: +- type-theory +- agda +- hott +math: true +draft: true +---
Imports @@ -55,7 +58,6 @@ we can just give $y$ again, and use the `refl` function above for the equality proof ``` -Bool-id-is-equiv .equiv-proof y .fst = y , Bool-id-refl y ``` The next step is to prove that it's contractible. Using the same derivation for @@ -71,26 +73,72 @@ when $i = i0$, and something that equals the fiber $y_1$'s preimage $x_1$ when $i = i1$, aka $y \equiv proj_1\ y_1$. ``` + +-- 2023-05-13: Favonia's hint is to compute "ap g p", and then concatenate +-- it with a proof that g is the left-inverse of f +-- ok i'm pretty sure this should be the g = f^-1 +Bool-id-inv : Bool → Bool +Bool-id-inv b = (((Bool-id-is-equiv .equiv-proof) b) .fst) .fst + +Bool-id-inv-is-inv : (b : Bool) → Bool-id-inv (Bool-id b) ≡ b +Bool-id-inv-is-inv true = + Bool-id-inv (Bool-id true) + ≡⟨ refl ⟩ + Bool-id-inv true + ≡⟨ refl ⟩ + -- This isn't trivially true? + (Bool-id-is-equiv .equiv-proof true .fst) .fst + ≡⟨ ? ⟩ + true + ∎ +Bool-id-inv-is-inv false = ? + +Bool-id-is-equiv .equiv-proof y .fst = y , Bool-id-refl y + Bool-id-is-equiv .equiv-proof y .snd y₁ i .fst = let eqv = snd y₁ -- eqv : Bool-id (fst y₁) ≡ y + -- this is the second pieece of the other fiber passed in eqv2 = eqv ∙ sym (Bool-id-refl y) -- eqv2 : Bool-id (fst y₁) ≡ Bool-id y + -- concat the fiber (Bool-id (fst y₁) ≡ y) with (y ≡ Bool-id y) to get the + -- path from (Bool-id (fst y₁) ≡ Bool-id y) -- Ok, unap doesn't actually exist unless f is known to have an inverse. -- Fortunately, because we're proving an equivalence, we know that f has an - -- inverse, in particular going from y to x, which in thise case is also y. + -- inverse, in particular going from y to x, which in this case is also y. eqv3 = unap Bool-id eqv2 - Bool-id-inv : Bool → Bool - Bool-id-inv b = (((Bool-id-is-equiv .equiv-proof) b) .fst) .fst + -- Then, ap g p should be like: + ap-g-p : Bool-id-inv (Bool-id (fst y₁)) ≡ Bool-id-inv (Bool-id y) + ap-g-p = cong Bool-id-inv eqv2 + + -- OHHHHH now we just need to find that Bool-id-inv (Bool-id y) ≡ y, and + -- then we can apply it to both sides to simplify + -- So something like this: + + -- left-id : Bool-id-inv ∙ Bool-id ≡ ? + -- left-id = ? eqv3′ = cong Bool-id-inv eqv2 give-me-info = ? -- eqv3 : fst y₁ ≡ y + -- Use the equational reasoning shitter + final : y ≡ fst y₁ + final = + y + ≡⟨ ? ⟩ + fst y₁ + ∎ +``` + +Blocked on this issue: https://git.mzhang.io/school/cubical/issues/1 + +``` + eqv4′ = ? eqv4 = sym eqv3 -- eqv4 : y ≡ fst y₁ in @@ -117,4 +165,14 @@ Bool-id-is-equiv .equiv-proof y .snd y₁ i .snd j = c-d = y₁ .snd in ? + ``` + +Blocked on this issue: https://git.mzhang.io/school/cubical/issues/2 + ``` ``` + +## Other Equivalences + +There are 2 other ways we can define equivalences: + +TODO: Talk about them being equivalent to each other diff --git a/content/posts/2023-07-04-learn-by-implementing-nginx.md b/content/posts/2023-07-04-learn-by-implementing-nginx.md new file mode 100644 index 0000000..0d28b88 --- /dev/null +++ b/content/posts/2023-07-04-learn-by-implementing-nginx.md @@ -0,0 +1,190 @@ ++++ +title = "Learn by implementing Nginx's reverse proxy" +date = 2023-07-04 +tags = ["web", "learn-by-implementing"] ++++ + +What the hell does nginx do? Let's replicate it. + +- A proxy usually lets you access a site through some gateway when reaching that + site when your client is sitting behind some intercepting firewall +- A _reverse_ proxy lets others access a site through some gateway when reaching + a server that's serving a site from behind a firewall + +As a middleman, it gets all requests and can introspect on the header and body +details. Which means it can: + +- Serve multiple domains on the same server / port +- Wrap unencrypted services using HTTPS +- Perform load balancing +- Perform some basic routing +- Apply authentication +- Serve raw files without a server program + +I'm going to implement this using Deno. + +
+ Imports + + ```ts + import { serve } from "https://deno.land/std@0.192.0/http/mod.ts"; + const PORT = parseInt(Deno.env.get("PORT") || "8314"); + ``` +
+ +Deno implements an HTTP server for us. On a really high level, what this means +is it starts listening for TCP connections, and once it receives one, listens +for request headers and parses it. It then exposes methods for us to read the +headers and decide how to further receive the body. All we need to do is provide +it an async function to handle the request, and return a response. Something +like this: + +```ts +// @ts-ignore +async function handlerImpl1(request: Request): Promise { + // code goes here... +} + +// Later, +// serve(handlerImpl1, { port: PORT }); +``` + +Now one of the primarily utilties of something like Nginx is something called +**virtual hosts**. In networking, you would call a host the machine that runs +the server program. However, virtual hosts means the same machine can run +multiple server programs. This is possible because in the HTTP header +information, the client sends the domain it's trying to access. + +``` +Host: example.com +``` + +Using this info, the server can decide to route the request differently on a +per-domain basis. Something like SSH is not able to do this because nowhere +during the handshake process does the client ever request a particular domain. +You would have to wrap SSH with something else that's knowledgeable about that. + +In our reverse-proxy example, we would want to redirect the request internally +to some different server, and then serve the response back to the client +transparently so it never realizes it went through a middleman! + +So let's say we get some kind of config from the server admin, saying where to +send each request. It looks like this: + +```ts +interface Config1 { + /** An object mapping a particular domain to a destination URL */ + [domain: string]: string; +} +``` + +Let's wrap our function with another function, where we can take in the config +and make it accessible to the handler. + +
+ Why? + + The `serve` here is what's called a **higher-order function**. This means that + rather than passing just data to it, we're passing it a function as a + _variable_ to store and call of its own volition. A common example of + a higher-order function is `Array.map`, where you take a function and apply it + to all elements within the array. + + So since `serve` is calling our handler, we cannot change its signature. + That's because in order to change its signature, we have to change where it's + called, which is inside the Deno standard library. + + Fortunately, functions capture variables (like `config`) from outside of their + scope, and when we pass it to `serve`, it retains those captured variables. + + For an implementation like this, you don't actually need to wrap it in another + function like `mkHandler2`, but I'm doing it here to make it easier to + separate out the code into pieces that fit the prose of the blog post. You + could just as well just define it like this: + + ``` + const config = { ... }; + const handler = async function(request: Request): Promise { + // code goes here... + }; + serve(handler, { port: PORT }); + ``` +
+ +```ts +function mkHandler2(config: Config1) { + // @ts-ignore + return async function(request: Request): Promise { + // code goes here... + } +} +``` + +I'm going to write this in the most straightforward way possible, ignoring +`null` cases. Obviously in a real implementation, you would want to do error +checking and recovery (since the reverse proxy server must never crash, right?) + +```ts +function mkHandler3(config: Config1) { + return async function(request: Request): Promise { + // Look for the host header + const hostHeader = request.headers.get("Host") as string; + + // Look it up in our config + const proxyDestinationPrefix = config[hostHeader] as string; + + // Let's fetch the destination and return it! + const requestUrl = new URL(request.url); + const fullUrl = proxyDestinationPrefix + requestUrl.pathname; + return await fetch(fullUrl); + } +} +``` + +Time to run it! + +```ts +const config = { + "localhost:8314": "https://example.com", + "not-example.com": "https://text.npr.org", +}; +const handler = mkHandler3(config); +serve(handler, { port: PORT }); +``` + +First, try just making a request to `localhost:8314`. This is as easy as: + +```bash +curl http://localhost:8314 +``` + +This should load example.com, like we defined in our config. We did a simple +proxy, fetched the resource, and sent it back to the user. If there was a +resource that was not previously available to the public, but the reverse-proxy +could reach it, the public can now access it. Our reverse proxy feature is done. + +Next, try making a request to not-example.com. However, we're going to use a +trick in curl to make it not resolve the address on its own, but force it to use +our domain. This trick is just for demonstration purposes, but it emulates a +real-world need to have multiple domains pointed to the same IP (for example, +for serving the redirect from company.com to www.company.com on the same server) + +```bash +curl --connect-to not-example.com:80:localhost:8314 http://not-example.com +``` + +This should produce the HTML for NPR's text-only page. This demonstrates that we +can serve different content depending on the site that's requested. + +## Conclusion + +This is a very bare-bones implementation, and lacks lots of detail. For a +non-exhaustive list of improvements, consider: + +- Can we have the web server remove a prefix from the requested url's path name + if we want to serve a website from a non-root path? +- Can we allow the reverse-proxy to reject requests directly by IP? +- Can we wrap non-HTTP content? +- What are some performance improvements we could make? + +In a potential future blog post, I'll explore some of these topics.