試著寫了 JIT 框架，研究了 JIT: Write XOR Execute policy 怎麼實現。目前放在 https://github.com/dannypsnl/still-compiling/tree/develop/dynasm 中，目前還遠遠不成熟，可能做幾個 example 之後才會考慮釋出

最近發現 racket 生態系裡面出現一個 Rakka 程式庫，它似乎把 Erlang 大部分一階抽象都做出來了，這是我個人想像很久的寫法，所以我當然很有興趣去嘗試。我的第一個實驗是針對的 sauron 內部程式庫 collector 進行重構。collector 原本就是模仿 Erlang 的訊息傳遞方式來抽象，使用 rakka 之後，我直接把這些抽象邏輯寫成 GenServer 的形式。結果發現效果非常不錯

1. 程式碼數量減少：collector 的程式碼量變成原來的大約三分之二。
2. 維護性提升：整體結構變得更好維護。

所以之後遇到類似的需求，我就會考慮使用 rakka 處理，我就不用再寫處理訊息傳遞風格的樣板式重複程式碼了。而且它還實現了 EPMD protocol，可以跟其他 node 互動。

要理解 Display map category 的定義（參考 Categorical Logic and Type Theory, Definition 10.4.1），我們需要理解它的動機跟捕捉問題的方式，因此我們要觀察一個個相繼式（我假設讀者已經熟練相繼式定義的類型論），並用範疇論（category theory）的語言重述。

在用相繼式描述類型論時，公式

表示 $\Gamma$ 可派生出類型 $A$。對於所有 $\Gamma$ 可派生的類型，我們用 $Ty(\Gamma)$ 表示，所以我們也會用 $A \in Ty(\Gamma)$ 來表示上面的相繼式。Display map category 捕捉的第一件事就是 contexts 構成一個 category，我們用 $\mathcal{C}$ 記號表示這個範疇，並且我們要求 $\mathcal{C}$ 有 terminal object $\diamond$，用來表示空的 context。

context 的構造方式只有兩種：$\diamond$ 是一個 context；context $\Gamma$ 加入一個類型 $A$ 得到的 $\Gamma \triangleright A$ 還是 context。

因此 $\Gamma \triangleright A \triangleright B \triangleright \cdots$ 也常被稱為 telescope

在相繼式中如果我們寫

我們的意思是 $\Delta = \diamond \triangleright T_1 \triangleright \cdots \triangleright T_k$，對於每一個 $T_i$，都能找到 $\sigma_i : T_i$，我們稱「$\sigma$ 實現了 $\Delta$」。

但上面那樣寫有問題，因為 $\sigma$ 沒有憑依，因此正確的通用寫法是記錄成

這表示 $\sigma$ 參考 $\Gamma$ 中的變數，並實現了 $\Delta$，這叫做一個替換。

而很明顯的，對於所有 $\Gamma = \diamond \triangleright T_1 \triangleright \cdots \triangleright T_k$ 有一個「引用變數 $\Gamma_i$ 來實現 $T_i$ 的不變替換 $id_\Gamma$」，所以我們想把每個替換 $\sigma$ 視為 $\mathcal{C}$ 中的 morphism $\sigma : \Gamma \to \Delta$。這裡需要證明幾件事

1. 對於給定的 $\Gamma, \Delta$，可能的 $\Gamma \to \Delta$ 的 collection 是一個集合。由於所有替換都涉及對 $\Gamma$ 的引用（或是有限多的類型生成規則）並做出一個有限構造，所以可以用歸納的方式比較，這讓證明是唯一的，因此這些替換是 set
2. 對 $f : \Gamma \to \Delta$ 來說有 $f \circ id_\Gamma = f = id_\Delta \circ f$。根據定義就知道了
3. 替換要有 associative $f \circ (g \circ h) = (f \circ g) \circ h$。這個不好證明，就我所知都是對規則進行 induction 得到（參考 Substitution Without Copy and Paste 的 §4.3）

現在我們要進入 Display map 的部分

到這裡我們發現，這個模型很好的捕捉了 syntactic categorical 的觀點，把類型論的句法特性都保留了下來。前面說過每個替換都有逆變，現在我們要證明逆變是一個 functor：

Proposition. 逆變是 functor [local-6]

對於任何 $\sigma : \Delta \to \Gamma$，我們把逆變看成 slice category 的函數 $\mathcal{C} / \Gamma \to \mathcal{C} / \Delta$，要檢查這是否是 functor，我們想要證明兩件事：保留 identity 且保留 composition。

Proof. [local-5]

套上 display maps 的規範，知道逆變會產出一個 pullback：

這直接證明了 $\sigma \circ \sigma^*(id) = \sigma$，所以 $\sigma^*(id) = id_\Delta$，表示 $\sigma^*$ 保留了 identity。

要證明 composition，可以用 pullbacks 的結合知道如果 $\sigma^*(f) \circ \sigma^*(g)$ 跟 $\sigma^*(f \circ g)$ 的頂點 up to isomorphism 是同一個，因此這兩個 morphism 是一樣的，證明了也保留 composition。因此每個替換誘導出的逆變都是 functor。 □

既然 $\sigma^*$ 是個 functor，那在 display map category 裡，我們可以用 $\sigma^*$ 的 right adjoint 表示 product，而且加上 Beck-Chevalley 條件：存在一個 natural isomorphism，讓我們可以把 product 用替換推來推去而不會變成不同的東西。

weak sum 同理，只是變成 $\sigma^*$ 的 left adjoint，同樣要有 Beck-Chevalley 條件保證 coproduct 可以被推來推去而不遺失。strong sum 則是把條件強化到 display maps 組合一定是 display map，這蘊含 weak sum 條件。

我們前面完全沒有提到 $\Gamma \vdash a = a : A$ 這種形式，而確實這是 display map categorical 方法的額外條件：weak equality 用 diagonal 的 left adjoint $Eq_{\pi_A}$ 表示，還是用 Beck-Chevalley 條件避免遺失。strong equality 規定 diagonal 是 display map，蘊含 weak equality。

對細節有興趣的讀者可以看 Paige Randall North 的 slide：Homotopical models of type theory

現在我們看到，display map category 除了捕捉 type theory 的 syntactic 特性，還可以用直觀的範疇論語言表述 type theory 的數種特徵，成功的讓我們用範疇論的觀點來檢視類型論。

讓我們先從 LLM 開始談起，我認為 Context Widows 的觀點很適合開始理解問題在哪裡。問題不在 LLM 或是廣泛的 AI 領域有用或是沒用，正如 Context Widows 一文自己所說跟我從其他地方看到的，正面的產出確實存在，像是

1. 蛋白質折疊
2. 材料科學
3. 用壓縮映射模擬星系演變

而可質疑的問題也一直存在：幻覺、缺乏理解。更不用說直接的負面影響

1. 氣候
2. 佔用能源（包含在天災時電網供電給計算中心而不是醫院）
3. 剽竊創意

Context Widows 真正要談的是，比起問 LLM 有沒有用，更恰當的問題是：LLM 能否有效地融入科學知識的創造、驗證和傳播過程中？

而很明顯的，這不局限於學術界中，搜尋引擎的誕生改變了網路，SEO 變成很多網站在意的事，從而產生了內容農場這樣製造垃圾的存在。

到這裡我們先總結 Context Widows 的結論：

LLM 並非科學出版功能失調的始作俑者；它們繼承了這種功能失調，加劇並使其運行得更快。就像一種通常無害的病原體在免疫功能低下的患者體內肆虐一樣，它們指出了問題所在，但如果將它們視為問題的全部，那就大錯特錯了。人們或許會希望這種加速發展能加劇矛盾，讓系統如此迅速地產生大量劣質內容，最終讓問題變得無可辯駁。但是，正如我們現在應該都明白的那樣，系統可以無限期地處於功能失調狀態，而荒謬本身並不會自我糾正。這種加速發展究竟會導致崩潰、適應，還是只是延續現狀，並非技術本身的問題，也無法透過關於技術能力的爭論來解答。答案將由運行這個計畫六十年的機構來解答。

於是現在我們可以更進一步的詢問：LLM 能否有效的融入商業的創新、運作和責任之中？

監控資本主義提出現代商業的核心邏輯是：資本的來源是販售預測；最容易被預測的人群，是被監控甚或控制的人群。因此獲利的動力會驅動大規模的監視與控制。

按吳修銘的話來說，即使是 Google 最大的反對者也很難說監控資本主義談的是 Google 的主要目的。但這可以被視為一個特別黑暗的隱喻，指向現代商業實踐的最糟結果。而現實中最接近的，是中俄等專制政權已經學會怎麼用現代技術影響他國的政治。

1. 《讀賣新聞》報導台灣政府正高度警戒中國透過操縱輿論介入選舉
2. 法國國際廣播電台報導歐洲如何應對俄羅斯的政治宣傳和軍事威脅？

再次的，LLM 提供了加劇破壞社會討論的一種方式，即用無限量的劣質資訊破壞言論場域，但這是因為網路早已逐漸侵蝕了公眾對談的能力。參見 Are we too connected to social media? An explanatory research the problematic social media use in self-esteem, phubbing and procrastinating behaviour。

注意到，這篇文章的目的不是號稱 LLM 全然的不好，或是商業多麽的灰暗；即使是最荒謬的公司中都有很多好人試著改善問題；學術界就算深受引用指標影響，也依然有大量有用的研究出產。最糟糕的莫過於直接跳過具體案例的討論，做出這個世界已經完全沒有救的結論。

這篇文章的目的是，從我有限的觀察與閱讀中，指出具體的商業、科技與政治問題，並且試著改善它們。如果問萬事揭曉：打破文明演進的神話，開啟自由曙光的全新人類史最重要的意義是什麼，我會說是 Graeber 指出人類具有想像並構造自己的政治的能力，遠超過當代人對自己的想像。或許我們可以試著打造一個世界，減少指標的需要、降低對效率的要求、更關心你我周遭的人、更注重環境對我們說的話，這不是什麼烏托邦，衝突不會簡單的消失，但我們需要真的開始對話跟行動，這一切才有出路。

今年開源的一點貢獻

• 自己弄了個網站生成工具 tr
• 弄懂怎麼生成 induction principle
• 參與了一點 Yoxem 的 SICP 台語翻譯計畫
• agda-mode-vscode 提示 unicode 符號輸入方式
• 讓 magic-racket 可以開啟 macro 展開過程的互動 GUI 用來除錯
• racket-langserver 的維護，今年底突然獲得管理權限xd

然後我下定決心研究了 epub 檔案格式，讓我更清楚可以對這些書籍檔案做什麼xd。因為年初我自己立的目標是看懂 mirror symmetry，數學我今年大致上學了

• mirror symmetry 的表示論前提

  • $\mathbb{k}$-linear category
  • cochain complex: 一系列 vector spaces $C^i$（或是 graded vector spaces）加上一個 degree 1 的 linear map $d$
  • cohomology: $d$ 按組成取 $\frac{\text{Ker}\ d}{\text{Im}\ d}$ 也是一個 graded vector space，這就是 cohomology 了
  • $A_\infty$ algebra 與 category
  • Twisted complex

  另外從微分幾何的方向看了一點物理學的對稱性怎麼用來描述費米跟玻色場。不過這些內容的意義為何？要解決什麼問題？似乎又回到需要代數幾何的基礎上，因此這裡得先放著了。

• preadditive/abelian category
• 一點 commutative algebra
• 一點 Lie algebra

今年末尾嘗試寫了各種 agda，讀了點 HoTT 中的 higher inductive types 跟 synthetic geometry，結合上面需要代數幾何的部分，讓我想往 synthetic geometry 的方向試試，或許先看看幾篇相關論文的未來研究方向跟未解問題？

技術性的東西其實比較好寫，做到哪裡就說什麼。今年六月的時候去台中找朋友，雖然大罷免沒有成功，但很高興台灣有這麼一群人，民主的重點從來都不是政黨，而是表達意願、付諸行動的公民。台灣的未來、人類的未來，目前看起來都比較灰暗，我不會指望明年就會有什麼差別，但願我們能學會不輕視人文、理解不同的文化、解決共同的難題。

參考 https://github.com/AndrasKovacs/elaboration-zoo/tree/master/06-first-class-poly

In type theory

A universe is impredicative if function types whose codomains are in the universe are always in the universe, regardless of their domain types.

如果 $\text{foo} : U_k$ 可以通過檢查，這個 Universe $U_k$ 就是 impredicative 的，有 impredicative universe 存在的類型理論就叫做有 impredicativity。像 Rocq 或是 Lean 都有特殊的 Prop universe 有這樣的特性。

In Elaboration algorithm

An elaboration algorithm is impredicative if it is able to solve metavariables to implicit function types.

最近在研究 Shrubbery Notation 怎麼實現 operator 優先序的過程中（卡關中），又發現 Rhombus 的 meta 功能中有不少有趣的東西，比如現在要介紹的功能：標記運算。要使用這個功能，必須在開頭宣告

#lang rhombus/and_meta

或是

#lang rhombus/static/and_meta

語言。接著定義

annot.macro 'AscendingIntList':
  'converting(fun (ints :: List.of(Int)) :: List: ints.sort())'

這會在我們寫下

[3, 1, 2] :: AscendingIntList

時，得到 [1, 2, 3] 而不是 [3, 1, 2]，因為這個標記會自動進行排序運算！

simplex 要怎麼跟幾何扯上關係？這是因為 up to homotopy，我們可以把幾何形狀變形成用一群三角形（確切的來說是一些 simplex）表示的形狀。這裡要講的案例 Torus 是一個二維度的幾何曲面，一般定義成 $S^1 \times S^1$ 並畫成

要怎麼三角化呢？通常會簡化成

這怎麼變成幾何形狀的？注意到標為同一個名稱的那些線，那表示那其實是同一條線。這需要定義一個 simplicial set $\mathcal{S}$（Hint: 根據定義是個 contravariant functor），其資訊如下：

視為其幾何實現（geometrical realization）：

每個 topological space $\mathbb{X}$ 都導出一個 simplicial set $\mathcal{X}$，每個 $k$-simplex 都是 $\text{Simp}_k$ 到 $\mathbb{X}$ 的連續函數：

每個連續函數，都給出了連續變形的過程；第二部分則是取 restriction，保持邊界關係。我下面展示如何逐漸變形來解釋其意義：

接著把管子對接

這確實是 Torus 的模型。

editor.js is a free, block-style (composable) editor with universal JSON output. Hence, it's a nice foundation for building your own rich-text editor.

mathlive is a math editor for the Web, specifically a custom HTML element with functionality to edit math formulas:

<math-field>
  x^2 + y^2 = 1
</math-field>

editor.js is extensible. Specifically, when creating an editor.js instance, one can provide customized tools to it:

new EditorJS({
  holder: editorContainer,
  autofocus: true,
  tools: {
    header: Header,
    underline: Underline,
    strikethrough: Strikethrough,
    list: List,
  }
})

These tools are node packages you need to install. As you can see, editor.js is highly modular, which is good because I'm going to add a new tool here. I'm going to show how to build a mathlive tool called Formula for editor.js (and perhaps I'll extract it as a package in the future).

A custom tool requires some basic setup, which is common to all tools

class Formula {
  static get toolbox() {
    return {
      title: "Formula",
      icon: "...",
    };
  }

  constructor({ data }) {
    this.data = data;
    this.wrapper = undefined;
  }
}

1. A tool is a JS class
2. In toolbox we can configure the title to show and the icon (which is a string of svg syntax)
3. We need to restore from data when constructing the tool (when loading from existing JSON!)
4. and we need a wrapper (a HTML element) to store the UI of this tool

Then we need to define how to store data into the output JSON, so we define save method

save(blockContent) {
  return {
    latex: blockContent.value,
  };
}

The blockContent is what the render method returns. We'll look at that part now

render() {
  this.wrapper = document.createElement("math-field");
  this.wrapper.setValue(this.data.latex);

  this.wrapper.macros = {
    RR: "\\mathbb{R}",
  };
  this.wrapper.mathVirtualKeyboardPolicy = "sandboxed";
  this.wrapper.addEventListener("focusin", (evt) =>
    window.mathVirtualKeyboard.show()
  );
  this.wrapper.addEventListener("focusout", (evt) =>
    window.mathVirtualKeyboard.hide()
  );
  this.wrapper.addEventListener("keydown", (e) => {
    const navigationKeys = [
      "ArrowLeft",
      "ArrowRight",
      "ArrowUp",
      "ArrowDown",
      "Home",
      "End",
      "Backspace",
      "Delete",
      "Enter",
      "/",
    ];
    if (navigationKeys.includes(e.key)) {
      e.stopPropagation();
    }
  });

  return this.wrapper;
}

This function is quite long, but let's break it down

1. We assign the HTML element math-field to the wrapper
2. Set the value of the math-field to the LaTeX formula loaded from data (which can be undefined)
3. Define macros for LaTeX input
4. Configure the policy and focusin/focusout event handlers to automatically open the virtual keyboard when the user focuses on the math-field
5. Add an event listener to intercept keys that would otherwise cause you to lose focus on the math-field (remember that editor.js is an editor, and those keys would trigger other operations in the background editor)
6. Finally, we return the wrapper, this HTML element will be the UI element of this tool

At the end, remember you also need to import css of mathlive in HTML

<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/mathlive/mathlive-static.css" />

How to package Mathlive JS code depends on your bundler - that's an entirely separate issue that I won't cover here.

Now that the technical details are covered, I can discuss the motivation. Basically, most editors split math formula input into two phases: When you focus on it, it show the original LaTeX syntax so you can edit it. When you focus out, it use KaTeX to render the formula result. But that's messy!

This model makes it easy to miss small problems, that's why there are many small typos in complicated formulas. WYSIWYG is the tool to solve this, and mathlive is such editor I need.

The full plan - though I'm not sure if I'll actually do it - is a complete note-taking system for academic knowledge. Some great tools include forester, Heptabase, Obsidian, etc. However, they all have some rough edges for example

1. forester has no editor part (there are some external editor projects though)
2. I can't contribute to codebase of Heptabase
3. Obsidian's format in long period is problematic
4. An Obsidian editor extension can't be ported to non-markdown formats, so notes taken here can't be ported to forester, for example

I have to say these aren't problems with the tools themselves, but I do want a tool that has WYSIWYG + portable format (JSON is good enough) + searchability.

Of course, to keep learning progress of mine, I can't spend all the time on a tool - working on problems and reading papers are much more important for learning.

sauron now supports find references of a definition in a whole project scope at commit: 3f78957a. This is a final piece of my IDE development for Racket, I had this idea three years ago, but get completed till now. This is because the resource stability of Racket get a huge improved, make this possible, I don't have detailed number, but the same program three years earlier will take down DrRacket.

After the above nonsense, I should quickly explain the idea, it can be break to a few steps

1. Everytime the project-directory is change (this is a configuration item), send update command to files' maintainer

2. In each collector, record entries of reference like this: key is filename of definition and identifier of definition, value is the binding location (filename, start, and end position)

3. When user use Cmd+B/Click, check the cursor is on a definition or on a binding. If cursor is on the later, open list-box to pick a reference/binding, and the selection will bring user to a new location

Now, let's look at the result: a definition in a.rkt, a provide and a local reference/binding, and a reference from another file b.rkt. Three references are showed in the list-box

After click the item, the frame move to binding location at b.rkt.

Anyway, this is a nice end for this project, in the future I will more focus on racket-langserver because it can help more users.

最近因為朋友提及，所以真正嘗試了 TeXmacs https://www.texmacs.org/ 這個軟體，感受到什麼是所見即所得應有的樣貌，於是想寫下一點介紹。由於 TeXmacs 做的特別好的是數學公式編輯，所以我們集中在這件事上。在 TeXmacs 中輸入 $ 就會立即創造一個 math 區塊，用 Ctrl + $ 則會創造置中的 math 區塊（$ 係指 Shift + 4，本文的快捷鍵皆為 MacOS 上的情況，在其他系統需注意差異）。

cursor 的所在區塊會被淺藍色框標記，範例如下

被選擇的區塊，會用紅色標記。用鍵盤或是滑鼠都可以選取

在 math 區塊中輸入分數時，鍵入 \frac 然後按下 Space，就會出現上下兩個區塊

其中紫色的是 cursor，可以用上下鍵切換要在哪個區塊繼續輸入

次方也是同理

對於等號，也有特殊的操作可以使用，比如選擇等號後按下 Ctrl + A，就會在正上方出現輸入區塊

最後，還有一些數學常見的段落，都已經寫成樣板可以直接插入：

插入結果

My exploration (around April, 2025) of Borsuk-Ulam theorem began with trying to prove the Lyusternik-Shnirel'man closed theorem for $S^1$ and $S^2$. While I could grasp it intuitively, constructing a rigorous proof proved elusive.

This led me to tackle the Borsuk theorem directly: For every continuous function $f : S^n \to \mathbb{R}^n$, there exists a point $x \in S^n$ such that $f(x) = f(-x)$.

The Failed Stereographic Approach

My initial idea was to decompose $f$ using North/South stereographic projections—the natural atlas for $S^n$. This approach not quite work here: the N/S maps send the projection point to nowhere (or must change codomain to one-point compactification), making any function decomposed this way necessarily discontinuous.

Refinement: Finite Projections

I then considered pulling the projection point outward along the N-S axis, forcing projections into finite regions to maintain continuity. This insight—that continuity constraints force us to work in bounded regions—became crucial to my understanding.

Following this idea to examine the N/S map decomposition, after compressing infinity back to $\mathbb{R}^n$, the continuity requirement also necessitates pulling back the neighborhood, leading to the same conclusion as the outward projection: the region must be finite.

At this moment, I learn the relations between different description of Borsuk-Ulam (Some applications of the Borsuk-Ulam Theorem).

The Breakthrough

My proof strategy ended up opposite to the classical development. I first established a lemma:

Lemma: Let $f : S^n \to \mathbb{R}^n$ be continuous and antipode-preserving. Then there exists $x \in S^n$ such that $f(x) = 0$.

The details can be found here, the key is $f(E) : S^{n-1} \to S^{n-1}$ bound an open set of $\mathbb{R}^n$ that contains $0$ and is the image of rest two open sets on $S^n$. Hence, $f(x) = 0$ for some $x$

The Proof

For the main theorem, define $g(x) = f(x) - f(-x)$. Two key observations:

1. $g$ is continuous
2. $g$ is antipode-preserving: $g(-x) = f(-x) - f(x) = -g(x)$

Applying the lemma: there exists $x$ such that $g(x) = 0$, which means $f(x) - f(-x) = 0$, hence $f(x) = f(-x)$. Proof complete.

The "wrong" approach turns out is useful in lemma, and provides a more concrete view about the problem.

After this, I also found Borsuk-Ulam Implies Brouwer: A Direct Construction, which is the same approach, and use cube version.

從矩陣非常難看出 determinant 的意義，但它其實具備幾何的意涵：對 $n$ 個向量張出的高維平行體的體積影響。

矩陣 $A$ 可以視為張量 $V \otimes V^*$，向量張出的高維平行體可以表示為 exterior product $v_1 \wedge \dots \wedge v_n$。因此定義 $\det A$ 如下：

這表示 $A$ 把 $v_i$ 映射到 $A v_i$ 所得的新高維平行體的體積相對於先前的高維平行體的比例（可能會正負轉換）。

補充：當 $\dim V = N$ 時。$N$ 階 skew-symmetric tensor 的空間 $\Lambda^N V$ 很明顯只有一個維度，這個空間在 Lectures on the Geometry of Manifolds 中叫做 Determinant line of $V$。此時 $\Lambda^{N+1} V$ 全都是 trivial space（只有 $0$ 元素）。

最近終於自己寫了個 site generator tr，這套機制確實是解決我很多問題，所以就開始遷移舊的部落格了。原則上大部分文章或是筆記都不會跟過來，因為這也是趁機丟掉一些已經過時/太簡單的筆記的機會，tr 讓我可以直接嵌入 wiki/nLab 來取代解釋基礎的定義。

這是今天遇到的問題，更新系統時它提示 /boot/ 的空間不足以安裝 efi 檔案了，直接砍 /boot/EFI/nixos/ 裡面的檔案是沒有用的，因為 NixOS 的 generations 會重新生成這些資料。所以正確的作法是先執行下面的指令

cd /nix/var/nix/profiles

裡面會有很多像是 system-數字-link 這樣的 soft links，每一個對應一個 NixOS 的 generation。把太古老的 generations 刪掉，執行

nix store gc

這會跑一段時間（如果你跟我一樣太久沒有清理就需要很久），結束之後再次更新系統就可以了。

elaboration 指的是轉換沒有語意的表面語法（surface syntax 或是說 source code）到有語意的語言表示（language representation）的過程，這樣講可能有點抽象，所以需要一些例子。試問 foo(a, b) 這段 Go source code 有語意嗎？事實上是沒有，因為只有在 Go compiler 經過

1. 讀取文字
2. 解析語法取得語法樹
3. 型別以及其他檢查

現在這段程式碼才會在 Go compiler 內部用某種資料結構表示，而 Go compiler 可以相信這段程式碼是滿足 Go 規範的程式，這樣才是有語意的語言。這個觀點一開始對你來說可能蠻怪異的，但我們可以仔細來看這樣定義的好處

1. 有些語言如 Fennel https://fennel-lang.org/ 刻意把自己變成另一個語言 Lua 的另類文法，在語言表示層面要求共用一樣的語意。Fennel 還支援了 macro 系統
2. 語法可以作為片段，嵌入到任何位置，只不過後續的檢查階段可能拒絕嵌入後產生的語法，因為這樣產生的程式依然可能是語法或是語意不正確的，比如使用 C 語言的 preprocessor 寫程式就經常會遇到這樣的問題。能把語法記錄下來並在別的地方展開的程式就叫做 macro，LISP 的 elaboration 經常叫做 expander

elaboration 前對語法樹進行操作的能力就是 LISP 最大的特徵，這使語言使用者可以自行發展他想要的語法，Clojure 做得比傳統 LISP 更好的地方就是這裡它採用的 edn 能表示比 S-expression 更多的資料，如 hashmap。

subroutine 在 C 語言被稱為 function，Fortran 中則分出 function 或是 subroutine，剩下還有一些語言使用 procedure 這個名稱。

Fortran offers two different procedures: function and subroutine. Subroutines are more general and offer the possibility to return multiple values whereas functions only return one value. https://fortranwiki.org/fortran/show/procedure

我把定義 subroutine 為一個指令語言編寫程式的模式，在組合語言裡面，我們並沒有函數名稱這種東西，相對的，其實只有指令的位址，所以組譯語言通常會提供區塊名稱來標記位址，比如 a:，那你可能已經想到了，如果我跳轉到 jump a 是不是就能執行 a 的內容了！是，但你要怎麼跳回來呢？所以 subroutine 就被發明了：找個 register 放一下要跳轉回來的位址就好啦！於是一個 a 呼叫 b 的程式就寫成

a:
  store ret (here+1)
  jump b
  ...
b:
  ...
  jump ret

(here+1) 是為了跳過 jump b 這個指令，而 ret 就是一個特殊保留的 register，專門用來讓 subroutine 使用。你會發現，ㄟ這樣是不是沒有傳遞參數？沒錯，所以更完整的故事是，CPU 會乾脆設計一整套傳遞參數應該用哪幾個 registers 跟 stack 偏移的慣例，叫做 calling convention。

這就是所謂的現代 CPU 是為了 compiler 設計。不遵守這些慣例你的程式還是能動，但你的程式就會跟其他 compiler 為這個 CPU 吐出來的程式很難溝通。

在一些非常簡單的作業系統實現裡面，會乾脆讓 user process 自己決定要不要讓出 CPU，怎麼讓？就是把自己當前的 stack pointer address 以及 registers 狀態儲存到記憶體裡面去，通常是 kernel 提供的一個 struct，然後跳轉到另一個 process 去。

這樣的話這是 user process 自己決定讓給誰，一般其實也不是這樣實現的，而是 user process 只有呼叫 yield 把自己暫停，下一步轉移給誰交給 kernel 決定。比如 Linux 就有

int sched_yield(void)

這個函數。

但要是 user process 不小心陷入無限迴圈怎麼辦？所以更常出現的是所謂的搶佔式排程，kernel 分配 time slice 並且封裝 process，並且設定計時器硬體中斷來確保自己可以定時查看狀態，這樣 process 在 slice 用光之後（或是它的指令執行完畢）就可以被切斷。

Manifolds and Differential Geometry

Let $e_1, e_2, \dots, e_n \in V$ be a basis of vector space $V$, and let $e^1, \dots, e^n \in V^*$ be a basis of dual space $V^*$. Now if $\bar{e}_i = C^k_{\ \ i} e_k$ is another basis of $V$, then there is an induced basis $\bar{e}^i = (C^{-1})^i_{\ \ k} e^k$ for dual space $V^*$.

Proof

By Kronecker-delta $1 = \delta^i_{\ i}$

can see that if $\bar{e}^{i} = e^{k} (C^{-1})^i_k$ then the equality is hold. We can use Penrose notation to show the idea.

程式語言為了讓使用者省略不必要的輸入，必須為使用者推導內容，這種需求催生了合一這種類型的演算法。比如很多程式語言允許泛型，比如下面的 OCaml 程式碼

let id (x : 'a) : 'a = x

Elaboration zoo 這個教學專案，它的程式碼要解決的，是一類更複雜的程式語言，叫做 dependent type 的系統中的合一問題，這類系統最重要的特性，就是類型也只是一種值，值也因此可以出現在類型中，但這就比較不是本篇的重點，有興趣的讀者可以閱讀 The Little Typer 來入門。在解釋完它的合一之後，我會介紹它隱式參數的解決方案

let id {A : U} (x : A) : A := x
let id2 {B : U} (x : B) : B := id _ x

let id {A : U} (x : A) : A := x
let id2 {B : U} (x : B) : B := id _ x

這時候跳回去看「contextual variables 是 $?0$ 能看到且實際內容未知的變數」就更能了解其理由了，因為已經能明確知道其內容的變數，如

let x = t

x 就是指向 t 的情況，若右手 term 是 x，其實也會是 t 去進行 unify。若右手 term 已經是 rigid form 又可參照，就更不需要成為 contextual variables，因為其 solution 就是把右手 term 原封不動放入，在反轉 map 的時候，只要記得這個 rigid 是非 contextual，就可以為它寫一個 identity mapping。

相關：higher-order-unification/explanation.md at master · jozefg/higher-order-unification --- github.com

一個 effect system 大概做了什麼，我們從 effekt 語言 (https://effekt-lang.org/) 這個案例著手

• 一個簽名 effect yield(v : Int) : Bool
• 一個 handler try { ... } with yield { n => ...; resume(n < 10) }
• 在 try 區塊中調用的函數 f 可以用 do yield(k) 來調用 handler
• 當 f 執行到 do yield(k)，就會跳轉到 with yield 中繼續進行，並且 n = k
• 當程式執行到 resume 就會跳回去 f 之後的 do yield(k) 的續延繼續執行

因此 exception 系統也可以被視為，沒有調用 resume 的 effect handler，讀者或許也想出數種使用方法了吧？這正是 effect system 的價值。而 racket 擁有比 effect handler 更複雜的機制（continuation with marks），不過 effect handler 機制具有保障使用者不容易出錯的好處，因此在 racket 中模擬一套 effect system 依然有意義，也是有趣的挑戰。

(call/prompt f tag handler args ...)

(with-handler [tag handler]
  (f args ...))

(abort/cc tag vs ...)

(handler vs ...)

要想實現 exception 目前的程式已經完全充分了，只要寫下

(define (f params ...)
  (abort/cc tag "cannot read file ..."))
(call/prompt f
             tag
             (λ (err)
               (printf "got err ~a~n" err))
             args ...)

即可。事實上 racket 自身的的 exception 也是這樣實作的，要考慮的問題是，前面我們看過 resume 可以跳回去被呼叫的函數！這是如何做到的？

(* 2 1)

(* 2 (call/cc (λ (k) (k 1))))

(define (f params ...)
  stmt1
  ...
  stmtn)

(define (f params ...)
  ...
  (call/cc (λ (k) ...))
  stmtk
  ...)

stmt1 ... stmtn

(begin stmt1 stmt2 ...)

我們正是需要使用 call/cc 來做出 resume 的效果。

(define (f params ...)
  (call/cc (λ (k) (abort/cc tag k ...))))

(define (f params ...)
  (call/cc (λ (k) (abort/cc tag k ...)))
  ...)
(call/prompt f
             tag
             (λ (resume ...)
               ...
               ; 跳回 f 繼續
               (resume))
             args ...)

到這裡我們已經有了運行的基礎，要改善有幾個方向可以參考

1. 用 macro 包裝語法
2. 放到 typed/racket 中加上 effect 類型檢查確保使用者沒有漏掉 handler：typed/racket eff
3. 支持 finally handler，保證任何退出行為都會被這個 handler 攔截（考慮 racket 的函數 dynamic-wind）

由於很多 TLA+ 入門教學似乎都沒有談到實務上要從哪裡開始使用 TLA+，所以這裡我想介紹實際上要怎麼做。一個 TLA+ 的檔案以 .tla 為副檔名，其中由 --- MODULE name --- 開頭，由 === 結尾，例如

---- MODULE plustwo ----
=====

在其中可以引用模組，寫成 EXTENDS xxx, yyy, ...

---- MODULE plustwo ----
EXTENDS Integers
=====

---- MODULE plustwo ----
EXTENDS Integers

CONSTANT Limit

(* --algorithm plustwo
variables x = 0;
begin
    while x < Limit do
        x := x + 2;
    end while;
end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "3f62e9ff" /\ chksum(tla) = "239a9ecd")
\* END TRANSLATION
=====

上面的 CONSTANT Limit 可以在 model 的設定檔 .cfg 中指定，這是為了避免把常數寫死在 TLA+ 主程式中，好在檢查前可以進行修改。

Even(x) == x % 2 = 0

IsInc == x >= 0

Inv == IsInc /\ Even(x)
THEOREM Terminated == Spec => Termination

這裡介紹了 TLA+ 如何運作，TLA+ 對現實程式的幫助會體現在編寫非同步的程式時，TLA+ 擅長對只有有限狀態、可以使用經典邏輯推導的程式進行檢查，主要可以發現死鎖與違反不變式等錯誤。對 TLA+ 所使用的數學方面的學習可以參考 Lamport 本人寫的 A Science of Concurrent Programs。

Each web page should provide the following content (use my site dannypsnl.me as example) in

<link href="https://dannypsnl.me/webmention-endpoint" rel="webmention" />

However, hosting a receiver can be annoying, so we should build on the top of some existed tools.

metric 就是在測量長度。不過在歐式空間裡面討論嵌入其中的曲面時，曲面有外部空間切向量，也就是歐式空間的向量可以使用。如果曲面沒有外空間，就需要自己做一個出來，這就引出了 Riemann metric 的想法：對可微分流形 $M$ 的每一點 $p$ 考慮抽象的切空間 $T_pM$（不考慮 $T_pM$ 到底是什麼），重點是隨點附上內積函數 $g : T_pM \times T_pM \to R$，因為是模仿內積所以有 bilinearity, positive-definiteness, symmetry 等性質

現在考慮曲線 $y : [0, 1] \to M$，在每一點度量 $T_pM$ 向量並積分（加起來）即是曲線長度。又隨著區間 $t : [0, 1]$ 改變，會有對應變化的 $p$ 點，因此模仿並定義

$\sqrt{g(\frac{dy}{dt}, \frac{dy}{dt})}$ 是 norm 的定義，積分因為是跟著 $t$ 變化，因此依賴 $y$ 的參數 $t$ 來定義。如此一來就可以問下一個問題：根據 $g$ 是從 $a$ 到 $b$ 的最短曲線是誰，這就是曲面上的直線的概念（然而，全域與局部最短線，是不一樣的問題，考慮整體將會複雜許多）。

https://qi.bookwar.info/pi-day-special-manifold 對 Manifold 這個想法的高層次概念進行介紹。

1. Classical logic's soundness says, if $\vdash_{cl} \alpha$, then $\alpha$ is classically valid.
2. Classical logic's completeness says, if $\alpha$ is classically valid, then $\vdash_{cl} \alpha$.

可以看到，要用 soundness 與 completeness 時，是在關心特定屬性 p，我們說一個系統 sound 就是在問「系統能導出的結果是否滿足 p」；我們說一個系統 complete 則是在問「滿足 p 的結果是否皆能從系統導出」。

To understand $F$-algebra, we will need some observations, the first one is we can summarize an algebra with a signature. For example, monoid has a signature:

or we can say ring is:

The next observation is we can consider these $m$ as objects in a proper category $C$, at here is a [cartesian closed category](math-000D). For example

• monoid is a $C$-morphism $1 + m \times m \to m$
• ring is a $C$-morphism $1 + 1 + m \times m + m \times m + m \to m$

Now, we generalize algebra's definition.

Definition. $F$-algebra (algebra for an endofunctor) [math-000F]

• 2023-10-24

With a proper category $C$ which can encode the signature of $F(-)$, and an [endofunctor](math-001T) $F : C \to C$, the $F$-algebra is a triple:

$$(F, x, \alpha)$$

where $\alpha : F \; x \to x$ is a $C$-morphism.

With the definition of $F$-algebra, $F$-algebras of a fixed $F$ form a category

Definition. category of $F$-algebras [math-000G]

• 2023-10-24

For a fixed endofunctor $F$ in a proper category $C$ (below notations omit fixed $F$),

1. the F-algebras $(x, \alpha)$ form the objects of the category,
2. morphisms are homomorphisms of objects $(x, \alpha) \xrightarrow{F\;m} (y, \beta)$, composition is given by functor laws.

A homomorphism is a $C$-morphism $m$ makes below diagram commutes.

We can extra check identity indeed works.

There is a theorem about the initial object of the category.

Theorem. Lambek's [math-000H]

• 2023-10-24

The evaluator $j$ of an initial algebra $(F, i, j)$ is an isomorphism.

Proof

Let $F\;i$ be an initial in the $F$-algebra category, the following diagram commutes for any $C$-object $a$

Now, replace $a$ with $F\;i$, we have commute diagram

Then we consider a trivial commute diagram by duplicating the path $F\;i \to i$

Combine two diagrams, then we get another commute diagram

By definition now we know $j \circ m$ is a homomorphism, and since $F\;i$ is an initial, we must have

$$F\;j \circ F\;m = 1_{Fi}$$

Therefore, we also have

$$j \circ m = 1_i$$

so $m$ is the inverse of $j$, proves $j$ is an isomorphism.

catamorphism [math-000I]

• 2023-10-24

The theorem actually proves the corresponding $C$-object $i$ of initial algebra $(F, i, j)$ is a fixed point of $F$. By reversing $j$ with its inverse, we get a commute diagram below.

In Haskell, we are able to define initial algebra

newtype Fix f = Fix (f (Fix f))

unFix :: Fix f -> f (Fix f)
unFix (Fix x) = x

View $j$ as constructor Fix, $j^{-1}$ as unFix, then we can define m = alg . fmap m . unFix. Since m :: Fix f -> a, we have definition of catamorphism.

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unFix

An usual example is foldr, a convenient specialization of catamorphism.

anamorphism [math-000J]

• 2023-10-24

As a dual concept, we can draw coalgebra diagram

and define anamorphism as well.

ana :: Functor f => (a -> f a) -> a -> Fix f
ana coalg = Fix . fmap (ana coalg) . coalg

I mostly learn F-algebras from Category Theory for Programmers, and take a while to express the core idea in details with my voice with a lot practicing. The article answered some questions, but we always with more. What's an algebra of monad? What's an algebra of a programming language (usually has a recursive syntax tree)? Hope you also understand it well through the article and practicing.

The proposition says a space is Hausdorff if and only if its diagonal map $\Delta : X \to X \times X$ to product space is closed, which given an alternative definition. Notice that close means its complement $\Delta^\complement$ is open. The definition of $\Delta$ is

Not hard to see below argument also applies to all finite $X$-product spaces.

Proof

(Hausdorff => diagonal map is closed) Hausdorff means every two different points has a pair of disjoint neighborhoods $(U \in \mathcal{N}_x, V \in \mathcal{N}_y)$, where $x \in U$ and $y \in V$. Therefore, every pair $(x, y)$ not line on the diagonal has $U \times V$ cover them. The union of all these open sets $U \times V$ covers $\Delta^\complement$, so $\Delta$ the complement of the union is closed.

(diagonal map is closed => Hausdorff) Since

is open, which implies for all $x, y$ the pair $(x, y) \in \Delta^\complement$. Since $\mathcal{N}_{(x, y)} = \mathcal{N}_x \times \mathcal{N}_y$, this implies the fact that $\Delta^\complement \in \mathcal{N}_x \times \mathcal{N}_y$.

Also, for all $U \in \mathcal{N}_x$ and $V \in \mathcal{N}_y$, it's natural that $U \times V \subseteq \Delta^\complement$, since the open set $U \times V$ at most cover $\Delta^\complement$.

Consider that reversely again, that means for all $(x, x) \in \Delta$, pair $(x, x) \notin U \times V$ (i.e. $U \times V$ will not cover any part of diagonal), that implies $U \cap V = \emptyset$ as desired.

這篇文章試著介紹 Lawvere's fixed point theorem 的意義與應用

Theorem. Lawvere's fixed point [math-0006]

• 2023-10-11

DIAGONAL ARGUMENTS AND CARTESIAN CLOSED CATEGORIES

在一個 cartesian closed category 中，如果 $A \xrightarrow{\phi} B^A$ 是 point-surjective，則所有 $B \xrightarrow{f} B$ 都存在不動點 $1 \xrightarrow{s} B$（滿足 $f \circ s = s$）。

Proof

首先畫出交換圖

其中 $\delta$ 的定義是 $c \mapsto \langle c, c \rangle$，所以對 $1 \xrightarrow{p} A$ 來說 $\delta \circ p = \langle p, p \rangle$。沿著這個定義，我們知道 $(\phi \times 1_A) \circ \delta \circ p = \phi\circ \langle p, p\rangle$。根據 point-surjective 我們知道 $\phi \circ p$ 對每個 $p$ 來說都是唯一確定的。現在把往下方 $B$ 的 $ev$ 也畫出，即可得出等式：

$$f \circ ev \circ \phi\circ \langle p, p\rangle = ev \circ \phi\circ \langle p, p\rangle$$

換句話說 $B \xrightarrow{f} B$ 的不動點即是

$$ev \circ \phi\circ \langle p, p\rangle$$

這個定理也可以用到 Gödel incompleteness、Tarski definability 等等問題上。論文 Substructural fixed-point theorems and the diagonal argument: theme and variations 更進一步的簡化了前置條件。

這個文章源自下面的問題

不過想問問專業的⋯⋯Golang 都有 interface 這種東西，提供泛型的必要性是什麼啊?

這是個常見的誤解，因為大部分語言不會多認真跟你講清楚到底啥是啥，看來好像都能接受多種不同的類型輸入不是嗎？所以這裡我們就來看各種機制的定義跟差別。

type Abser interface {
        Abs() float64
}

type A interface {
        F(C) D
}
type B interface {
        F(C) D
}

interface Comparable {
  int compareTo(T other);
}

<S extends Comparable> S min(S a, S b)

interface 是一種子類型關係，換句話說當 $T$ 實現 $A$ 我們就說 $T \le A$，在每個要求 $A$ 的位置都可以用 $T$ 取代。

多型的本體是一個型別等級的參數！在語意學上，上面的簽名可以改寫成 $f : \Lambda S. S \times S \to S$，當你寫下

的時候，乍看之下是一個完整的呼叫。實際上編譯器會先推導 $k$ 的類型，記作 $\uparrow k$，譬如假設 $k : C$ 則 $\uparrow k = C$，這時候就可以做型別替換 $(\Lambda S. S \times S \to S) C$ 得出 $C \times C \to C$。因此真正的呼叫程式碼是

子類型規則並不能取代替換這個語意。在 Java 的 $f : (S \le A) \Rightarrow S \times S \to S$ 規則下，僅是多檢查了 $C \le A$ 是否為真，子類型與多型仍然是不同的規則。

哥德爾不完備定理是一個相當有趣的邏輯學發現，要了解他的意涵，要先考慮哥德爾的編碼

哥德爾數（Gödel number）是一種編碼方式，在一個算術系統裡面，當我們把每個字符都排成一個有限的列，我們可以幫每個字符都指定一個自然數。具體來說，我們可能會寫下

1. $\neg$ 是 $1$，其後設意義為「否定」
2. $\lor$ 是 $2$，其後設意義為「或」
3. $\lor$ 是 $2$，其後設意義為「且」

當有符號 $s_i (i \in \N)$，其對應的哥德爾數為 $n_i$。我們並不是真的關心具體的每個符號，我們做這件事的理由是為了表示哥德爾編碼。所以這裡要開始定義哥德爾編碼，首先先看一個簡單的例子：當有系統的公式符號排列 $s_1 s_{10} s_4$，我們說公式的哥德爾編碼為 $2^{n_1}\cdot 3^{n_{10}}\cdot 5^{n_4}$。

因此用函數 $\alpha(i)$ 指示一個公式的每個位置 $i$ 符號的 Gödel number，則哥德爾編碼確切的定義是

，也就是將質數以每個符號對應的哥德爾數為指數，將它們全部乘起來。這個辦法只是為了迫使每個公式有對應的編碼存在。我們用 $\overline{G}$ 記號表示公式 $G$ 的哥德爾數。

$\alpha$ 函數給出第 $i$ 個出現符號的在表中的位置。

在承認前述的系統 $P$ 下，可以開始描述。

因此在 The Blind Spot: Lectures on Logic 中可以看到其陳述更加關注核心：對一個足夠編碼自己又一致的系統

• 存在一個真確的公式 $G$ 不可決定
• 系統證明自己具有一致性會連帶證明這個不可決定的公式，所以系統無法證明自己的一致性

換句話說，要關心的並不是具體如何構造上面陳述的編碼，而是這類系統編碼系統自身的普遍性問題。

不久之前看到fizzyelt 的文章，所以我前幾日開始研究自己以前寫的 strictly positive 筆記，因此找到了 Andrej Bauer 在 stackexchange 的回答，整理後寫了這篇文章解釋何謂型別的大小

def foo (t : T) : T :=
  match t with
  | c f => f t

def fib : Nat → Nat
  | 0   => 1
  | 1   => 1
  | n+2 => fib n + fib (n+1)

inductive Fib (a : Type) : Nat → Type where
  | z : a → Fib a 0
  | o : a → Fib a 1
  | s : Fib a n → Fib a (n+1) → Fib a (n + 2)

def expr : Parsec E :=
  let l <- expr
  match '+'
  let r <- expr
  return E.add l r

mutual
  def term := parse_int <|> parens expr
  def expr : Parsec E :=
    let l <- term
    match '+'
    let r <- term
    return E.add l r
end

def infixL (op : Parsec (α → α → α)) (tm : Parsec α) : Parsec α := do
  let l ← tm
  match ← tryP op with
  | .some f => return f l (← tm)
  | .none => return l

mutual
  def factor : Parsec Expr

  def expr : Parsec Expr :=
    factor
    |> infixL (parseString "*" *> return Expr.mul)
    |> infixL (parseString "+" *> return Expr.add)
end

def infixL (opList : List (Parsec (α → α → α))) (tm : Parsec α)
  : Parsec α := do
  let l ← tm
  let rs ← many do
    for findOp in opList do
      match ← tryP findOp with
      | .some f => return (f, ← tm)
      | .none => continue
    fail "cannot match any operator"
  return rs.foldl (fun lhs (bin, rhs) => (bin lhs rhs)) l

我希望這次有成功解釋怎麼從規則對應到 parser combinator，所以相似的規則可以抽出相似的 higher order function 來泛化，讓繁瑣的規則命名變成簡單的函數組合。這個技巧當然不會只有在這裡被使用，只要遇到相似形的文法都可以進行類似的抽換，相似的型別簽名可以導出通用化的關鍵。

partial def infixR (opList : List (Parsec (α → α → α))) (tm : Parsec α)
  : Parsec α := go #[]
  where
  go (ls : Array (α × (α → α → α))) : Parsec α := do
    let lhs ← tm
    for findOp in opList do
      match ← tryP findOp with
      | .some f => return ← go (ls.push (lhs, f))
      | .none => continue
    let rhs := lhs
    return ls.foldr (fun (lhs, bin) rhs => bin lhs rhs) rhs

def «prefix» (opList : List $ Parsec (α → α)) (tm : Parsec α)
  : Parsec α := do
  let mut op := .none
  for findOp in opList do
    op ← tryP findOp
    if op.isSome then break
  match op with
  | .none => tm
  | .some f => return f (← tm)

def «postfix» (opList : List $ Parsec (α → α)) (tm : Parsec α)
  : Parsec α := do
  let e ← tm
  let mut op := .none
  for findOp in opList do
    op ← tryP findOp
    if op.isSome then break
  match op with
  | .none => return e
  | .some f => return f e

當一個語言逐漸成熟，開發者常常會有一個想法就是用自己開發的語言寫這個語言的編譯器，但是這個決策會導致程式庫中有兩套目標一樣但是實現語言不同的編譯器程式。其一是本來的實現，另一個是用語言自身新寫的。一來這樣開發任何新功能的時候都需要寫兩次；二來這會減少可能的參與者人數，因為這下他得要熟悉兩個語言才行！解決這個問題的辦法就是啟動編譯器，通常是一個在多平台上可以直接執行的檔案。

有了這些概念，我想你已經有能力為自己的語言寫出啟動編譯器了！那麼剩下的篇幅我就可以來寫點 murmur，我覺得這個概念可以進一步推升到選擇一個夠容易編譯出來，也夠容易寫出通用最佳化編譯器的語言來達成。我個人是很看好 wasm，因為它確實容易當目標、最佳化，只可惜現在還有不少重要的功能都沒有定案。llvm 的 bytecode 確實也是一個方案，寫一個把 llvm bytecode 編譯成 executable 的 python 檔案並不困難，但 llvm 的連結性自己就是一個天殺的大麻煩所以這個方案我很少看到有人使用。Java bytecode 則是讓那些本來就預計只在 JRE 生態系內部的語言從一開始就沒有這個問題，微軟的 CLR 也是類似的狀況，缺陷是最後語言受制於 runtime，這個問題會有多大條取決於語言的目的是什麼。

好像是今年最後一天了，祝你不是在今天看到這篇文章的！

在傳統的 ML 或是 Haskell 裡面，有一個型別表現的特別醜陋，就是 data type 表示的 disjoint。 這是因為無論如何，disjoint 就是會需要執行期時有要處理哪個分支的資訊。 因此語言中都設計有 constructor 這麼一個特殊的存在，其中每個 case 都有對應的執行期標籤。 舉例來說，

type bool = false | true

這裡 false 可能就是 0 而 true 是 1。

type nat = z | s of nat

這裡 z 可能就是 0 而 s 是 1 並且接有一個 tuple 放 nat 。

要是這種 disjoint 語義想要完美對應 category theory 的 coproduct，那就需要引入真正的 union type。 要注意到這跟 C 語言的 union 略有不同，C 語言事實上仰賴了開發者完全知道自己在做什麼作為前提， 要求開發者對 union 正確的操作。要是要求 C 語言一樣要能處理不同型別的輸入的話，一樣要放置一個標籤欄位才能解決。 union type 在型別上是很優美，沒有 多餘 的標籤，在 typed/racket 裡面可以記成 (U Integer Boolean String) 之類的。但這個方案遠非毫無缺點，之所以可以這麼做，事實上是因為 racket（以及早期的諸多 functional languages）採用了 universal object 編碼。

Universal object 就是指對每一個執行期的物件，都把型別囊括在內。 這樣一來當然就不需要另外給標籤，因為每個物件本來就都有標籤了。 可想而知，這個方法缺點就是針對需要緊密排列的運用場景效果不佳。 所以 racket 要是需要操作 vector float 這種資料，再怎麼編譯都還是會慢 C 語言一線， 主因就是沒有用最緊密的方式排列資料（多了標籤），相較於 C 沒有利用到當代硬體特性。 但反過來說就沒有 ad-hoc 的編譯難題，因為本來就是需要 runtime 解決的問題就推到 runtime 解決。

那麼可想而知，後來為了適當壓縮物件，ML 跟 Haskell 都走上混合的解決方案。 針對小物件（通常是指小於等於該平台的一個 word 的資料型別）就會盡可能不要包起來，反之就採用 universal object， 在實務上表現也確實不錯。

所謂的使用參考等價性，是指在某些語言裡面，兩個物件是否相同是通過參考而非內容決定的。 舉例來說， racket 裡寫下一個空結構，然後生成一些實例

(struct id ())

(define a (id))
(define b (id))
(define c a)

我們可以用一些 eq? 運算來檢查

> (eq? a b)
#f
> (eq? a c)
#t
> (eq? c a)
#t
> (eq? b c)
#f

這樣就可以生成一連串在運行中的程式內唯一的資源標示。

但要小心你用的語言的特性，比如要是我把上面的 (struct id ()) 變成 (struct id () #:transparent) 並改用 equal? 運算， racket 就會改用內容而非參考去判定相等。

應用場景

那麼這種技巧可以用在哪些地方呢？首先要注意到這絕對不可以用在序列化上！每次程式重新啟動，同一個宣告都會被重新分配到不同的參考，所以這不能超出程式運行的範疇。 所以合適的用法應該是在程式終止之後就不會再仰賴這個資源唯一性的。

1. Racket 自己 Sets of Scopes：在 Matthew Flatt 的 Let's Build a Hygienic Macro Expander 裡， scope 就是一個空結構。
2. 型別檢查裡面的自由變數也可以用這個方式生成（這樣我們就不用維護一個 free variables counter）。
3. Threading ID: 共時結構要是需要唯一標示的時候，這個技巧就很方便，因為沒有正確運作的記憶體配置器會把物件分配到同一個地方。

這樣的小技巧非常方便，當然也需要注意其限制以及程式語言的實際運作方式。 在使用前最好真的去讀你的語言對參考的處理方式，確保這些程式仰賴的環境假設正確無誤，才不會出現出乎意料的問題。

data Bad
  bad : (Bad → Bottom) → Bad

notBad : Bad → Bottom
notBad (bad f) = f (bad f)

isBad : Bad
isBad = bad notBad

absurd : Bottom
absurd = notBad isBad

data Term
  abs : (Term → Term) → Term

app : Term → Term → Term
app (abs f) t = f t

w : Term
w = abs (λ x → app x x)

loop : Term
loop = app w w

文章到這邊告一段落，也解決了我這一年來對證明器實作的最大疑問之一，進一步的解答可以參考 https://cs.stackexchange.com/questions/55646/strict-positivity/55674#55674

很久以前就曾經想過要不要寫下這種經驗文，這念頭出現到現在轉眼就過了兩年了 XD。期間真的發生了太多事，現在又到了人生的十字路口所以決定記錄一些東西，希望這篇文章或許能夠啟發一些像我一樣迷惘的人。

大學教育

我接觸程式的時間不是特別早，到了大學才第一次”使用”電腦。那時真的蠻好笑的，我選了這裡的原因是因為我覺得這系名好長好有趣就填在指考志願第一個位置(而我當時也沒有試圖弄懂志願序的用途 XD)，亂填的下場就是我爸差點沒氣死。當時幾經考慮，然而最後我還是決定不重考了。因為前進後或許不是一條好的道路，但到時候再後悔就好了，而不前進就必然要耗費一年也未必真的有什麼結果。到了學校，基礎程式課就立刻深深吸引了進了不知道能幹嘛的科系、對未來毫無想法的我。從此我每天從中午 12 點寫程式寫到半夜 3 點，每個禮拜只出現在程式課、書店、圖書館跟房間，搞到很多科都超低空飛過(雖然我也不在意)。印象特別深刻的是當初印出 99 乘法表的作業我硬是搞不懂 loop 的用途，死纏著學長問了 2 小時才寫出來。現在想想，真是佩服學長沒有從此不鳥我呢 XD。大一就在不太懂什麼檔案 IO、資料庫的情況下寫出了人生第一個能夠算是應用程式的程式：課堂的最終測驗，寫出一個運作在 CLI 下的 ATM(當時也不知道什麼是 CLI XD)。大二的資料結構與演算法課程中，小組討論促進了很多有趣的發想跟對演算法的理解(可惜整個科系就只有該門課程的教授這樣上課)。這門課讓我知道很多同學其實都能講出非常有見解的解法，即使他們後來未必會走上開發者這條道路。該課程結束後我跟學長(對，被我纏了 2 小時的那位)更常單獨討論他們當時的專題：為醫療領域優化的搜尋引擎。這個專題重點擺在如何針對特定領域優化搜尋結果，減少搜尋到農場文當然是非常重要的目標之一。由於當時對爬蟲的討論，我開始接觸 Erlang 與 Go 這兩個語言，接著幾個月都在不斷的優化寫好的爬蟲，讓它能夠在最短時間內處理最多的頁面。最後還不小心翻開龍書踏入了 Compiler 的奇妙世界。快樂的時光總是短暫，由於一些經濟因素，我決定休學走上工作的道路。

工作

第一份工作我靠著一個類 python 語言的直譯器說服了老闆為什麼雇用一個高中學歷的人也沒問題 www。現在回想這間公司真的很不錯，只要工作做完就完全不干涉你要做什麼，所以我在這裡寫了不少 Compiler 的程式，還把 redux porting 到 Go 裡面(雖然我到現在也沒弄懂這有什麼意義 XD)。當時朋友都在台北，也因為在家住膩了(結果現在又想回家住了)，決定上台北找工作，就在台北待到了現在。剛上台北找工作時有一次很有趣的面試，當時我英文不好(連 Algorithm 都沒聽懂是什麼)、技能樹只往 Compiler 上點，面試官還願意一個一個跟我解釋我的問題在哪裏，最後還鼓勵我有學會的東西都記得很熟練，人真的超好 :)，現在還是很感謝他。工作幾年下來，其實慢慢覺得工作帶來的成長不存在了，這也讓我有了想轉換人生跑道的想法，後面會再提。

認識 PLT

在台北工作的兩年多裡慢慢開發著自己的程式語言，隨著得到更多的開發經驗和學習了更多的語言，我逐漸意識到我似乎有什麼根本性的東西根本沒有學到。就像當初我總覺得 Design Pattern 有點怪異、Go 開發者宣稱的簡單似乎不大對一樣的直覺，我發現了 PLT 這個以前從來沒有碰過的領域。從此開始入天坑：lambda calculus -> second order logic -> hindley-milner -> dependent type -> calculus of construction -> MLTT，現在正在讀 cubical type, inductive construction(CIC), HoTT 等。我認為學習 PLT 真的有很大的好處，會逐漸超出單個語言的見解，分解出是什麼讓程式變得好寫而什麼不是。也是對 PLT 的學習讓我終於弄懂為什麼 Go 的設計其實並沒有帶來簡單性、為什麼 Design Pattern 其實沒有必要背誦(甚至沒必要特意學習)。只是隨著了解的深入，我也更不想設計新的程式語言了 www(但又不想廢棄寫很久的專案)。但我不建議對上面的一切沒有興趣還硬讀，cs 有很多事情能做，絕對不只是 PLT。

避免崇拜

我覺得一路走來，最重要的教訓就是不要盲目的崇拜，不只是技術上，在生活中也應該檢視自己是不是做了什麼假設，而不是盲目的用被假設影響後的觀點看待事物。以我個人而言，崇拜過 Go, UNIX 等專案的作者和所謂的 hacker 就是該怎樣，進而導致了很多不良的選擇，例如：硬要用 vim 而不是 IDE、硬要用 CLI 而不是 GUI、明明有現成方案卻要從頭打造整個專案。這不是說用 vim 不對，很多時候我都用 vim。當環境上只有 terminal 或是只是要小改幾行時，我不否認它的編輯能力非常高效，但如果要說起跟 debugger 的整合性、移至定義的精準度、重構的方便度、閱讀其他人的程式碼等等，用 IDE 真的會好很多。關鍵是不要只因為某個看法就放棄對其他可能性的探索。對，就算我推薦 IDE，你還是該學看看 vim 或 emacs，說不準什麼時候就用到了。這也連結到怎麼選擇要學習什麼，只要避免崇拜，就較能以客觀的角度選擇合適的工具。

歸類知識

對知識進行分類是有好處的，記住生命週期長的資訊，而對有生命週期短的資訊不要耗費太多時間。例如說「理解演算法」就比「記住 vim 的 101 個指令」生命週期長的多。這裏，並不只是指事物本身的生命週期，要說起來 vim 活得超久，可能比很多演算法更久，但 vim 是容易過時的，你可能會遇到某些情況 vim 就是沒有 plugin 能用，這時候該做的恐怕不是自己刻個工具而是找替代方案，因為我們通常沒有時間，比起 vim 我更關心我想處理的問題，所以 agda 我用 atom 編輯，因為有方便的套件能用。而演算法就算不是最快的，其發想思路還是有相當的價值。同理對程式語言其實沒有必要花時間掌握語法到能夠「寫出最好的寫法」，因為我們關心的是程式碼解決的什麼問題，不是用什麼程式語言。關鍵是不要為了「非核心」的知識耗費大量心力，若這個「非核心」的知識不是你的興趣也不是你的工作職責。沒錯，如果就是喜歡玩 vim，開發 vim 的 plugin 就是樂趣根源那就去做吧，人類社會之所以能夠運作就是因為每個人是不一樣的。就像 PLT 知識對目標是寫個作業系統的人而言只是「非核心」知識一樣，每個人需要學習的知識都不一樣，所以也沒必要羨慕什麼「大神」，說不準人家還羨慕你能睡好覺，who knows。

下一個階段

雖然我被我講得好像我已經沒有迷惘了似地 XD，但完全不是這樣，我也在考慮去考在職碩士然後出國讀博士走學術這樣的路。人生沒有所謂的成功，有個笑話就說「窮人想有錢，有錢後被權貴欺負，就想著要有權，成官之後整天鬥爭，想想還是平淡的生活好，又成了窮人」，笑話是笑話，但人生沒有最佳解卻是事實，所以就算選了之後後悔也沒關係，需要的只是弄清楚自己接著想做什麼，然後去做。

世界上只有一種真正的英雄主義，那就是在認識生命的真相後，依然熱愛生活。

雖然我說的好像自己什麼都知道了，可惜就算是此時此刻我也搞不清楚我想幹嘛 w，但我還是會繼續學習我有興趣的知識、嘗試看看學術生涯是什麼樣子、體驗不同國家生活的風景。不知不覺就 23 歲，寫了 5 年程式，工作了 3 年，這世上唯一不缺的…大概就是時間不夠的感嘆，希望接下來 3 年也是有趣的人生。

人生不是只有程式碼

最後，人生不是只有程式碼，記得停下來看看那些幫助自己的人，我曾經沒有看清這麼簡單的事實。回憶過往，人生總是在受他人的幫忙，高中時帶給我人生樂趣的數學老師、嘴上抱怨但還是支持我的各種任性決定的父母、大學我整天吃吐司時請我吃飯的同學跟二話不說就借我幾千元的朋友、當初幫我跟老師求情不要當我的同學 www、工作時遇過的同事、在我低潮時聽我講抱怨的廢話的人們，只能再三感謝。這些才是讓我不用擔心，專心開發的支柱，如果有人讀完真的覺得自己沒有這樣的支柱，那也可以寄信給我，雖然我不見得能給什麼建議，保證沒辦法解決問題，但我可以好好聆聽，因為也有曾經願意聽我訴說的陌生人，雖然最後好像跟 programming 根本沒什麼關係 www，但還是希望這篇文章能夠幫助到一些人。話說回來，這部落格真的有讀者？

Recently we are working on a new feature is about filter packets by HTTP header for our router. This is the concept, we read the header by rules, rules are just some key/value pair. If key missing or value isn't matched, then we drop the packet.

When a connection end, we would remove this connection from allowing pass map.

Anyway, we found a bug is, we use FIN flag to say this packet is the end of the TCP connection, but we know a connection end is a:FIN -> b:ACK -> b:FIN -> a:ACK, a/b is client/server here. So except the first packet, following packets won't pass our router, then connection would never end until timeout, LOL.

Do you know what can Go's package reflect do?

Whatever you had use it or not. Understanding it is not a bad thing.

A well known thing is Go don't have generic, I'm not going to tell you we have generic, I'm going to tell you some basic trick to have the result like generic.

Take a look on the type Stack

type Stack struct {
    stack  []interface{}
    limitT *reflect.Type
}

limitT is a *reflect.Type, the reason that it's a pointer to reflect.Type rather than reflect.Type is because of we may do not spec it.

We add the Stack by invoke WithT.

func (s *Stack) WithT(v interface{}) *Stack {
    t := reflect.TypeOf(v).Elem()
    s.limitT = &t
    return s
}

Why is reflect.TypeOf(v).Elem()? Because we can't really get an instance that type is an interface! Instead of that, we can get a type is pointer to an interface!

We have a common idiom is using (*SomeInterface)(nil) to get pointer to interface instance.

Now we know that user code can be

type AST interface {
    Gen() llvm.Value
}

// main
s := stack.New().WithT((*AST)(nil))

After we do that, user can't push a value do not implement AST. So, how we do that? We do a check at Push

func (s *Stack) Push(element interface{}) {
    if s.limitT != nil {
        if !reflect.TypeOf(element).Implements(*s.limitT) {
            panic(fmt.Sprintf("element must implement type: %s", *s.limitT))
        }
    }
    s.stack = append(s.stack, element)
}

If limitT is not nil, means we do not limit the type, just keep going on. But if we limit the type, we check that element implements limitT or not. If not, we panic the process. Now we have a stack can promise type safe at runtime.

I think most Gopher had read error-handling-and-go. Has anyone had watched Go Lift? Let's getting start from Go Lift! The point of Go Lift is: Error is Value. Of course, we know this fact. Do you really understand what that means? In Go Lift, John Cinnamond mentions a trick about wrapping the error by command executor. For example, we create a connection to server:6666 by TCP.

conn := net.Dial("tcp", "server:6666")

Can we? Ah…, No! The correct code is:

conn, err := net.Dial("tcp", "server:6666")
if err != nil {
    panic(err)
}

Then we write something through the connection.

nBtye := conn.Write([]byte{`command`})

We want that, but the real code is:

nBtye, err := conn.Write([]byte{`command`})
if err != nil {
    panic(err)
}
// using nByte

Next, we read something from server:6666, so we create a reader.

reader := bufio.NewReader(conn)
response := reader.ReadString('\n')

No! We have to handle the error.

response, err := reader.ReadString('\n')
if err != nil {
    panic(err)
}
// using response

Howver, the thing hasn't ended yet if we have to rewrite the command if response tells us the command fail? If we are working for a server, we can't just panic? So Go Lift has a solution:

func newSafeConn(network, host string) *safeConn {
    conn, err := net.Dial(network, host)
    return &safeConn{
        err: err,
        conn: conn, // It's fine even conn is nil
    }
}

type safeConn struct {
    err error

    conn net.Conn
}

func (conn *safeConn) Write(bs []byte) {
    if conn.err != nil {
    // if contains error, do nothing
        return
    }
    _, err := conn.Write(bs)
    conn.err = err // update error
}

func (conn *safeConn) ReadString(delim byte) string {
    if conn.err != nil {
        return ""
    }
    reader := bufio.NewReader(conn.conn)
    response, err := reader.ReadString("\n")
    conn.err = err
    return response
}

Then usage will become

conn := newSafeConn("tcp", "server:6666")
conn.Write([]byte{`command`})
response := conn.ReadString('\n')

if conn.err != nil {
    panic(conn.err)
}
// else, do following logic

Can we do much more than this? Yes! We can have an error wrapper for executing the task.

type ErrorWrapper struct {
    err error
}

func (wrapper *ErrorWrapper) Then(task func() error) *ErrorWrapper {
    if wrapper.err == nil {
        wrapper.err = task()
    }
    return wrapper
}

Then you can put anything you want into it.

w := &ErrorWrapper{err: nil}
var conn net.Conn
w.Then(func() error {
    conn, err := net.Dial("tcp", "server:6666")
    return err
}).Then(func() error {
    _, err := conn.Write([]byte{`command`})
})
Wait! We need to send the connection to next task without an outer scope variable. But how to? Now let's get into reflect magic.

type ErrorWrapper struct {
    err         error
    prevReturns []reflect.Value
}

func NewErrorWrapper(vs ...interface{}) *ErrorWrapper {
    args := make([]reflect.Value, 0)
    for _, v := range vs {
        args = append(args, reflect.ValueOf(v))
    }
    return &ErrorWrapper{
        err:         nil,
        prevReturns: args,
    }
}

func (w *ErrorWrapper) Then(task interface{}) *ErrorWrapper {
    rTask := reflect.TypeOf(task)
    if rTask.NumOut() < 1 {
        panic("at least return error at the end")
    }
    if w.err == nil {
        lenOfReturn := rTask.NumOut()
        vTask := reflect.ValueOf(task)
        res := vTask.Call(w.prevReturns)
        if res[lenOfReturn-1].Interface() != nil {
            w.err = res[lenOfReturn-1].Interface().(error)
        }
        w.prevReturns = res[:lenOfReturn-1]
    }
    return w
}

func (w *ErrorWrapper) Final(catch func(error)) {
    if w.err != nil {
        catch(w.err)
    }
}

Now, we're coding like:

w := NewErrorWrapper("tcp", "server:6666")

w.Then(func(network, host string) (net.Conn, error) {
    conn, err := net.Dial(network, host)
    return conn, err
}).Then(func(conn net.Conn) error {
    _, err := conn.Write([]byte{`command`})
    return err
}).Final(func(e error) {
    panic(e)
})

For a given function $f : X \to Y$, the following are two correct definitions of f is an equivalence.

{-# OPTIONS --safe --without-K #-}
module ag-000T where

open import MLTT.Spartan hiding (fiber)

fiber : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → Y → 𝓤 ⊔ 𝓥 ̇
fiber f y = Σ x ꞉ domain f , f x ＝ y

is-equiv : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (f : X → Y) → 𝓤 ⊔ 𝓥 ̇
is-equiv f = ∀ (y : codomain f) → Σ σ₀ ꞉ fiber f y , ∀ (σ : fiber f y) → σ ＝ σ₀

{-# OPTIONS --safe --without-K #-}
module ag-000U where

open import MLTT.Spartan
open import UF.Base
open import UF.Sets
open import UF.Sets-Properties