Lîm Tsú-thuàn

BlogBlog.Club 名單自動收錄·資料來源與計算方式 ⓘ

收錄文章: 76篇

部落格資料

名稱: Lîm Tsú-thuàn
原站: https://dannypsnl.me/ ↗
最後發文: 2026/9/1 00:00
抓取成功: 2026/10/29 05:18
發文頻率: 約每 6 天
檢查頻率: 每 6 小時檢查 RSS

內文來源

狀態: 已取得內文
取得方式: RSS 全文
平台: WordPress
最近成功: 2026/10/18 17:19

各來源

RSS 全文已取得內文 · 完整76 篇

使用的技術

成功觀測: 2026/10/25 06:37
觀測來源: https://dannypsnl.me/ ↗

在網站雷達查看詳細結果 ↗

主機與 CDN（低信心）

CloudflareCDN
信心
低
規則
wappalyzer:cloudflare
證據
- 回應標頭：response header rule
觀測於
2026/10/25 06:37

使用的技術

正在讀取技術觀測…

網站流量Similarweb · 2026 年 9 月

網域 dannypsnl.me · 已取得

每月約 2,376 次造訪

來源國家（前五）

墨西哥51.8%
美國25.2%
印度23%

印度排名: 第 646,813 名
全球排名: 第 7,438,666 名

取得：2026/10/22與其他部落格比較 →

近 90 天話題

共同關鍵字

近 90 天話題

共同關鍵字

正在載入話題文字雲…

最新收錄

本頁 50 篇

從有限元素中隨機取未使用的元素
元素集合可以轉換為正整數集合，因此問題可以寫成：給定範圍 [0,N)[0, N)[0,N)，已使用之數字集合為 UUU，最簡單的演算法就是排除 UUU [0,N)∖U[0, N) \setminus U[0,N)∖U 從中隨機取一個元素問題 [local-0] 然而排除已使用元素是固定成本，在已使用元素會變多的情況下更是越來越大的成本。隨機抽一個，再查看有沒有撞上已經使用的位置反而更有效。但這樣做的界線到底在哪裡？幾何分布 [local-1] 對於空間大小 NNN 與已使用的 UUU，隨機抽一個位址命中未使用元素的機率是 p=N−∣U∣Np = \frac{N - |U|}{N}p=NN−∣U∣ 假設每次抽樣互相獨立，那「抽到第 kkk 次才第一次成功」服從幾何分布 (1−p)k−1p(1-p)^{k-1} p(1−p)k−1p 連續 kkk 次都失敗（選到已使用的位置）的機率是 (1−p)k(1 - p)^k(1−p)k，期望次數是 1/p=NN−∣U∣1/p = \frac{N}{N - |U|}1/p=N−∣U∣N 所以我們可以看到 ∣U∣|U|∣U∣ 只佔 NNN 一小
2026/9/1 00:00https://dannypsnl.me/tr-D6VS
部落格作為一個fediverse帳號
延續部落格問題挑戰的規劃，我研究了怎麼讓blog作為fediverse帳號存在。我希望部落格文章會得到一個fediverse post，有人在fediverse上跟post互動時，可以在部落格本體看到變化。這樣就等於借用了fediverse作為留言系統這個專案公開端點是 https://fedi.dannypsnl.me，借用大量的Cloudflare（CF）功能與Fedify完成： D1：跟隨者、貼文、互動 KV：Fedify的快取 Queue：投遞跟收信 R2：貼文附圖的儲存 ActivityPub需要什麼？ [local-0] 一個fediverse帳號是一個HTTP服務，要能回答這幾件事： /@blog：actor，帳號本身 /@blog/inbox：別人寄東西來的地方 /@blog/outbox、followers、following：這個帳號的公開集合 /.well-known/webfinger：把 @[email protected] 這個名字換成上面那個actor的網址這些都能用Fedify處理，因為要簽HTTP Signatures，這塊很麻煩所以要盡
2026/8/30 00:00https://dannypsnl.me/8664
部落格問題挑戰
看ltlnx的部落格時看到這個挑戰，剛好也想寫點什麼所以就來寫吧！你當初為什麼開始寫部落格？你使用什麼平台來管理你的部落格？為什麼選擇它？你之前有在其他平台上寫過部落格文章嗎？你如何撰寫文章？例如，使用本地編輯工具，還是在部落格的後台／控制面板中編寫？你什麼時候最有寫作靈感？你會在寫完後立即發布，還是會先存成草稿醞釀一下？你部落格上最喜歡的文章是哪一篇？你對部落格有什麼未來計畫嗎？例如重新設計、搬到另一個平台，或是加入新功能？你當初為什麼開始寫部落格？ [local-0] 當初只是想紀錄一些學習上的問題，因為那時候看到「學東西最好的方式就是教別人」，所以就順便把筆記變成部落格你使用什麼平台來管理你的部落格？為什麼選擇它？ [local-1] 我用自己開發的靜態網站產生器tr-notes，工具的網站 https://tr-notes.srht.site/ tr-notes的起源是我使用forester的時候一直遇到breaking changes，但大抵上來說我覺得這種軟體很好用（可以讀 https://www.forester-notes.org/QHXS/inde
2026/8/18 00:00https://dannypsnl.me/MNIW
To CPS or not to CPS：編譯理論之爭
在什麼是CPS？我們討論過CPS是怎樣的程式風格，以及編譯器可以怎麼利用這種風格。但我們該不該使用CPS呢？這曾經引發一系列的爭論編譯理論之爭 [local-0] 1978 RABBIT: A Compiler for SCHEME，據說這是最早採用CPS的編譯器 1992 Compiling with Continuations，Appel整理並提供了完整的ML CPS風格編譯器 1993 The essence of compiling with continuations，形式化並辨識出ANF，認為direct style (ANF) 在local control flow上提供了更簡單的工作方式 1997 A reflection on call-by-value，這篇正式的討論了direct style在什麼時候可以替代CPS編譯器 2007 Compiling with continuations, continued，Kennedy認為CPS在functional language上有勝過ANF或是monadic IR的地方，主要爭點就是inline會導致ANF需要re
2026/7/29 00:00https://dannypsnl.me/ASEH
色彩繽紛的範疇論
我在這裡想要用範疇論（category theory，又稱抽象廢話）展示跟大家印象中不一樣的數學，有興趣深入學習的讀者可以在最後找到進一步的學習資源。範疇論是從代數拓樸、代數幾何等領域的發展中自然出現的概念，主要的用途是用來高效地描述物之間的關係、用一種抽象的視角觀察整體性質。下面舉一些例子幫助你大致理解一下範疇論在數學領域的定位，看不懂或是想跳過都沒差，並不影響後續閱讀 Example 數學中的Categories與Functors [local-0] 我們有所有集合與函數的範疇 Sets\text{Sets}Sets、所有群與群態射的範疇 Groups\text{Groups}Groups Monoid MMM 的Actions可以改寫成functor Mop→SetsM^{op} \to \text{Sets}Mop→Sets（事實上這類functor有個特殊名稱，叫做presheaf）拓樸空間 XXX 的所有開集之間的包含關係構成一個category Open(X)\text{Open}(X)Open(X) 遺忘functor，比如 Groups→Sets\text{Grou
2026/7/15 00:00https://dannypsnl.me/Z00L
J-sheaf 的直覺
JJJ-sheaf 的概念有點難解，這個定義是在模擬從小的opens（局部）往大的opens（整體）前進的時候，每個在整體上的定義都可以分成局部的定義，而局部的定義黏起來會得到整體的定義這樣的匹配性，而且局部之間的交疊必須匹配。對於具體的sheaf，可以參考這裡從topological space的opens構成的locale抽象化到category之後，我們就從opens變成操作objects；coverings變成sieves；在open XXX 上定義的某類函數抽象化成presheaf，因為我們想讓框架適用於所有類型的函數，而且我們發現函數並不是必要的條件，我們只需要這些東西在某個意義上表現的像函數，因此presheaf僅僅是說，對於object XXX 會有一個對應的集合，並且在morphism上我們contravariant（以符合幾何的直覺）。JJJ-sheaf也因此等於在問，對於這樣抽象的 topology 與「函數」，什麽算是在交集處互相同意對方的值？ category中沒有交集的概念，sieve的composition closure確保了如果 f∈Sf \in S
2026/7/10 00:00https://dannypsnl.me/LPLF
Brid.gy cross-post 的使用方法
Brid.gy cross-post 的使用方法2026-06-23Lîm Tsú-thuànbridgy cross-post 的使用方法因為我無法記住兩年前怎麼設定的 brid.gy，所以再次調查怎麼做然後寫下來。brid.gy 的首頁長這樣，像我是需要貼到 mastodon 所以就按 mastodon 按鈕接著會出現兩個選項我們這種用法要選的是 Cross-post to a Mastodon account @[email protected] 輸入你的 mastodon instance，取得授權之後，你的文章裡面只要有 microformat 應該就能用用來發佈了
2026/6/23 00:00https://dannypsnl.me/CIEP
Soufflé 入門
Soufflé是高效能的Typed Datalog引擎，能把宣告式規則編譯成C++，或用直譯器模式執行 fact 與 rule [local-0] fact（已知的事實）與 rule（能從事實推導新事實的規則）。先宣告一個輸入關係，代表「模組a直接相依於模組b」 // 代表 a 直接 import b .decl depends(a: symbol, b: symbol) .input depends .decl 宣告關係的名字與各欄位型別（symbol 是字串，另一個常用型別是 number）。.input 表示資料從外部讀入：預設是從同名的 depends.facts 檔案，每行一筆、以 Tab 分隔。接著我們定義第一條規則：模組若被任何人相依，就是「被使用的」 .decl used(m: symbol) used(m) :- depends(_, m). 讀法是「對任意 m，若存在 depends(_, m)，則 used(m) 成立」。:- 右邊是body（前提），左邊是head（結論），_ 是 wildcard，表示「有就好、是誰都可以」。開發者不用管理控制流程：規則評估結果
2026/6/21 00:00https://dannypsnl.me/programming-0TXN
日本北陸之旅 2025/10 能登
因為《放學後失眠的你》裡面的夜景（真脇遺跡）太漂亮了，所以我一直想要去能登一次想不到再來發生了能登半島地震，直到這次旅程，能登半島沿途大部分的道路都還在整修中，有臨時紅綠燈跟工程人員管制（單側輪流通行），隨處可見大災難的痕跡第一日（飛機/住宿） [hokuriku-day1] 在桃園機場隨意吃過午餐，坐上 12:10 起飛、往日本海岸線去的班機在降落小松之前在日本海上轉向，往陸地飛去，經過軍機場之後 16:05 降落在小松機場。小松並不大，主要都在等過海關，下了樓之後因為接駁車等待人數不少，擔心可能要再等一班，於是坐計程車去小松車站，買了類似台灣區間車的車票做到金澤站這台火車的座椅很有趣，有一個機械結構，乘客可以把座椅調整成對向四人座，或是兩人座。飯店 checkin 完畢再去找晚餐，這時候市場已經快關了，而且很多店大排長龍，就隨便找一間吃第二日（能登第一日） [hokuriku-day2] 這天的目標是先去 ORIX 取車，然後開去千里濱凪沙道路，取車前還有一點時間，先跑去看鼓門這一整日都陰雨綿綿，在取車之後在市區開了大概一個多小時之後來到千里濱，才發現因為海嘯的緣故，下
2026/6/19 00:00https://dannypsnl.me/VW5V
善與善的對抗
討厭推薦演算法、討厭廣告、討厭 AI、討厭生活壓力、討厭別人、討厭自己但行好事，莫問前程願自己不要原地踏步。但善與善的對抗之中，什麼是好事？
2026/6/15 00:00https://dannypsnl.me/BF9W
violet literate programming 支援
之前其實就有弄過一次但效果很不好，現在 LSP server 已經建立，基於 interaction 抽象層讀取資料產出 html 效果就好上很多 Example 初步實驗的效果 [violet-0000]2026-06-13 目前是用 violet weave 從一個 .vt.scrbl 編譯。程式碼區塊由 violet 前處理：@vt|{…}| 的內容會被抽出、型別檢查，轉成帶標記的 HTML。其餘內容原樣交給 tr-notes 把游標移到 identifiers 上時可以看到型別；調用部分連結到它的定義；?here 這樣的 goal 會顯示 context 與 target \universe US U \let id(A : universe U) -> (_ : A) -> A (Auniverse U : Uuniverse S U) : Auniverse U -> Auniverse U \where xA \let ex(A : universe U) -> (_ : A) -> A (Auniverse U : Uuni
2026/6/14 00:00https://dannypsnl.me/D1AX
轉移控制權作為 effect：coroutine 與排程器
這是 effect 系列的第三篇，這篇要解釋怎麼用 effect 攔截 coroutines 的 yield 並重新排程。所謂的 coroutines，就是一些互相約定好會主動讓出執行權利，互相「協作」的函數。是 continuation 極其常見的使用案例，首先我們先設定 abort 部分： (define sched-tag (make-continuation-prompt-tag 'sched)) (define (yield) (call/cc (lambda (k) (abort/cc sched-tag k)))) 可以看到 yield 就是預設外部會有一個 prompt (effect handler) 等著自己，於是它就把自己的 continuation 捕獲起來丟出去給 handler 我們需要一個地方存放還沒有做完的任務，所以定義了一個 queue tasks spawn 單純就是把任務推入 queue 中排隊 continue 的目的是提供 handler 等待 thunk 的 yield 再次把執行權釋出 (define tasks (make-queue)
2026/5/20 00:00https://dannypsnl.me/Y7OR
violet 的一點新進展
申請了 domain https://violet-lang.org/ 給 violet 使用。比較大的變化是 Inductive types 可以生成相應的 eliminator 的類型與計算重新設計了 constructors 的 namespace，@ice1000 說的是對的，constructors 被放到 namespace 之下其實影響不大，要用時再打開，或是設計表面語法就可以了提供 \operator 讓開發者自己定義需要的運算式語法，比如 \operator "\x + \y" => add x y \associativity: \left 模組現在預設是 private，並新增 \export 關鍵字建立了 project 概念，現在可以用 info.vt 管理專案依賴，進一步可以參考 https://github.com/violet-prover/std kernel 加入內建的 record 下一步？ [local-0] 現在的 <= \elim 並不處理有任何帶有非純變數參數的 elimination target，因為這會導致 eliminator
2026/5/17 00:00https://dannypsnl.me/ILIG
用 effect system 實現直釋器
這是 effect 系列的第二篇，這篇要展示的是用 effect 攔截對 environment 的查詢。所以第一步我們要定義一個攔截 effect (define lookup-tag (make-continuation-prompt-tag 'lookup)) (define (lookup x) (call/cc (lambda (k) (abort/cc lookup-tag k x)))) 第二步我們建立執行函數 EVAL，但我們建立一個 go 輔助函數，讓最上層負責攔截找不到 variables 時的查找，並提供沒有該 variable 的錯誤訊息。這裏跟一般直譯器實現的主要差異就是我們不需要傳 env 這樣的變數，這通常是某個 environment 實現（比如 hashmap 或是一些值構成的 list，由 de Bruijn indicies 參照）的實例 (define (go tm) (match tm [(? symbol? tm) (lookup tm)] [(? number? tm) tm] [`(+ ,@a) (apply + (map go a))]
2026/5/10 00:00https://dannypsnl.me/SW6P
正確處理單位的算術系統
在做物理或工程上的算術時，我們常常會在單位上出錯：把公尺加到秒上、把公斤乘進長度卻沒有標記，或是次方算錯，最後得到一個「數字看起來合理」但單位錯亂的結果。這些錯誤在紙筆運算時不容易被察覺，發現的時候往往已經是好幾步之後，回頭檢查非常的麻煩能不能讓工具替我們把關呢？如果單位本身就是型別的一部分，編譯器就能在我們把不相容的東西硬湊在一起時直接拒絕。我們可以用 Agda 來規範出這樣的一個系統用 Agda 實現單位正確的算術 [ag-OW40] {-# OPTIONS --safe --without-K #-} module ag-OW40 where open import MLTT.Spartan hiding (_+_) open import MLTT.Negation open import MLTT.List open import MGS.MLTT using (has-decidable-equality) open import Integers.Type open import Integers.Addition open import Integers.Multi
2026/5/7 00:00https://dannypsnl.me/S20M
以 effect 為合約：用 effect system 解耦遍歷演算法與存取點
我以前寫過一篇文章介紹 effect system，看過之後的回饋基本上有兩種哇靠這也太抽象了，到底在說什麼那 effect system 到底對我們日常的程式開發有什麼用？所以我打算利用零碎的時間寫寫各種應用範例，而這篇就是關於如何用 effect system 將遍歷演算法與 visit 處理分離。我想不重複 racket 中的有界續延如何實作 effect system 的功能？已經介紹過的各個 racket API，所以直接用程式案例說明。比如今天我們想要走訪 binary tree，以 inorder 走訪可以寫成 (define (dfs t) (match t [(list v L R) (dfs L) (visit v) (dfs R)] [v (visit v)])) 我們單純認定 (list root-value L-tree R-tree) 這樣的格式是 binary tree，這很可能不是最好的寫法，不過以這裡要講的概念來說，重點在 visit 是什麼，所以我們先看一下實現要記得用 (require racket/control) 引入 racket/c
2026/4/10 00:00https://dannypsnl.me/4Z05
RSS in emacs：elfeed
I've been trying some Emacs packages, including elfeed and meow, but the latter is not the topic of this post. I will briefly introduce elfeed package. I use straight.el to install packages: (use-package elfeed :custom (elfeed-feeds '("https://dannypsnl.srht.site/rss.xml"))) elfeed-feeds is where you configure the feeds. Here I use my personal site as an example. Use M-x elfeed to open a buffer of elfeed. In this buffer, pressing G will fetch and refresh the feeds. Once articles are listed, pres
2026/2/14 00:00https://dannypsnl.me/EHWW
Pattern Unification演算法理論部分
在這篇文章裡面我想要探討 Elaboration Zoo 裡面的 pattern unification 演算法怎麼算出來的，以及在什麼時候成立。主要是了解我們怎麼導出等式： ?α=?rhs′[spm−1] ?\alpha \overset{?}{=} \text{rhs}'[sp_m^{-1}] ?α=?rhs′[spm−1 ] 超越 Elaboration zoo 中的合一演算法與隱式參數僅是直覺的推理。在 Display map category 我們已經了解到，contexts 跟 substitutions 構成了一個範疇，而我們想要知道的是 epimorphism 的定義，所以 Kovacs 的第一步是把 epimorphism 定義改寫成更適合這個案例的定義 Definition Epimorphism [local-0] 我們說 Sub Γ ΔSub\ \Gamma\ \DeltaSub Γ Δ 是 epimorphism iff δ∘σ=δ′∘σ⇒δ=δ′A[σ]=A′[σ]⇒A=A′\begin{aligned} \delta \circ \sigma = \de
2026/2/13 00:00https://dannypsnl.me/F6C1
安裝 Guix
下載之後按照系統安裝文件描述的方式把 iso 燒錄到 USB or DVD，插入電腦開始安裝。基本上現在的引導介面已經跟 ubuntu 之類的老牌 distribution 相當了，只要按照螢幕上說的逐步回答就能設定完成。它的 root 跟一般帳號是明確分開的，密碼也不同，在設定完 root 密碼之後會要求建立至少一個一般帳號。partition 分成兩種，按照需求選擇就好。最後選介面時有很多選擇，Gnome、KDE、Sway 都有，這個也是習慣用什麼就選什麼就行了。這之後就會開始安裝，跑完之後重開機（boot 管理要記得切換到安裝好的系統才不會又跑進 installer）。到這裡就可以看 https://guix.gnu.org/manual/1.5.0/en/html_node/Getting-Started-with-the-System.html 文件開始編輯 /etc/config.scm 了。
2026/2/5 00:00https://dannypsnl.me/B4OI
2026 - Week 5
Racket 中的 concurrent programming [local-0] 想到就測試 rakka 跟 Racket coroutine thread 結果 native 還比較快XD，所以我就把 genserver 做成 Racket thread 封裝了 https://repo.dannypsnl.me/dannypsnl/erl。至於為什麼 coroutine thread 這麼快，我猜可能 CS 之後有很大改善，我之前沒有注意到這點 JIT [local-1] 延續上個禮拜的工作，用手搓的 JIT 實現 brainfuck 編譯器 brainfuck JIT Racket language server [local-2] racket-langserver 這個 PR 的目的是改善目前一團糟的測試體驗。現在的方式是啟動 subprocess 然後跟它的 stdio 互動，一來這意味著大量的系統資源需求，二來耦合這麼重就很難設計可以遠端連線的 server。所以第一步需要清理現在的設計，引入間接層讓測試只需要跟這個抽象部分互動就好 racket-llvm [loca
2026/1/28 00:00https://dannypsnl.me/2026-W5
2026 - Week 4
試著寫了 JIT 框架，研究了 JIT: Write XOR Execute policy 怎麼實現。目前放在 https://repo.dannypsnl.me/dannypsnl/still-compiling/src/branch/main/dynasm 中，目前還遠遠不成熟，可能做幾個 example 之後才會考慮釋出
2026/1/26 00:00https://dannypsnl.me/2026-W4
Rakka 使用初體驗
最近發現 racket 生態系裡面出現一個 Rakka 程式庫，它似乎把 Erlang 大部分一階抽象都做出來了，這是我個人想像很久的寫法，所以我當然很有興趣去嘗試。我的第一個實驗是針對的 sauron 內部程式庫 collector 進行重構。collector 原本就是模仿 Erlang 的訊息傳遞方式來抽象，使用 rakka 之後，我直接把這些抽象邏輯寫成 GenServer 的形式。結果發現效果非常不錯程式碼數量減少：collector 的程式碼量變成原來的大約三分之二。維護性提升：整體結構變得更好維護。所以之後遇到類似的需求，我就會考慮使用 rakka 處理，我就不用再寫處理訊息傳遞風格的樣板式重複程式碼了。而且它還實現了 EPMD protocol，可以跟其他 node 互動。
2026/1/9 00:00https://dannypsnl.me/GMYW
Display map category 捕捉了類型論的什麼面向？
要理解 Display map category 的定義（參考 Categorical Logic and Type Theory, Definition 10.4.1），我們需要理解它的動機跟捕捉問題的方式，因此我們要觀察一個個相繼式（我假設讀者已經熟練相繼式定義的類型論），並用範疇論（category theory）的語言重述。在用相繼式描述類型論時，公式 Γ⊢A type\Gamma \vdash A \text{ type}Γ⊢A type 表示 Γ\GammaΓ 可派生出類型 AAA。對於所有 Γ\GammaΓ 可派生的類型，我們用 Ty(Γ)Ty(\Gamma)Ty(Γ) 表示，所以我們也會用 A∈Ty(Γ)A \in Ty(\Gamma)A∈Ty(Γ) 來表示上面的相繼式。Display map category 捕捉的第一件事就是 contexts 構成一個 category，我們用 C\mathcal{C}C 記號表示這個範疇，並且我們要求 C\mathcal{C}C 有 terminal object ⋄\diamond⋄，用來表示空的 context。 cont
2026/1/6 00:00https://dannypsnl.me/tt-BBGG
現代 - 商業、科技與政治交織的空間
讓我們先從 LLM 開始談起，我認為 Context Widows 的觀點很適合開始理解問題在哪裡。問題不在 LLM 或是廣泛的 AI 領域有用或是沒用，正如 Context Widows 一文自己所說跟我從其他地方看到的，正面的產出確實存在，像是蛋白質折疊材料科學用壓縮映射模擬星系演變而可質疑的問題也一直存在：幻覺、缺乏理解。更不用說直接的負面影響氣候佔用能源（包含在天災時電網供電給計算中心而不是醫院）剽竊創意 Context Widows 真正要談的是，比起問 LLM 有沒有用，更恰當的問題是：LLM 能否有效地融入科學知識的創造、驗證和傳播過程中？ LLM 能否有效地融入科學知識的創造、驗證和傳播過程中？ [local-0] 由於一項技術的潛在用途並非其實際用途，而實際用途又取決於採用該技術的機構、機構試圖解決的問題以及機構用作衡量成功的既有指標。所以 Context Widows 認為探討 LLM 與科學的關係，等若詢問 LLM 出現之前，科學界已經運作著怎樣的體系？我們知道當代科學界的主導是引用體系，隨著時間發展，引用體系已經改變它本要量測的對象；科學家會調整
2025/12/30 00:00https://dannypsnl.me/U5YI
2025 年
今年開源的一點貢獻自己弄了個網站生成工具 tr 弄懂怎麼生成 induction principle 參與了一點 Yoxem 的 SICP 台語翻譯計畫 agda-mode-vscode 提示 unicode 符號輸入方式讓 magic-racket 可以開啟 macro 展開過程的互動 GUI 用來除錯 racket-langserver 的維護，今年底突然獲得管理權限xd 然後我下定決心研究了 epub 檔案格式，讓我更清楚可以對這些書籍檔案做什麼xd。因為年初我自己立的目標是看懂 mirror symmetry，數學我今年大致上學了 mirror symmetry 的表示論前提 k\mathbb{k}k-linear category cochain complex: 一系列 vector spaces CiC^iCi（或是 graded vector spaces）加上一個 degree 1 的 linear map ddd cohomology: ddd 按組成取 Ker dIm d\frac{\text{Ker}\ d}{\text{Im}\ d}Im dKer d
2025/12/28 00:00https://dannypsnl.me/2025
Rhombus 用標記運算自動排序資料
最近在研究 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]，因為這個標記會自動進行排序運算！
2025/12/15 00:00https://dannypsnl.me/programming-0005
具體的 simplicial set: Torus
simplex 要怎麼跟幾何扯上關係？這是因為 up to homotopy，我們可以把幾何形狀變形成用一群三角形（確切的來說是一些 simplex）表示的形狀。這裡要講的案例 Torus 是一個二維度的幾何曲面，一般定義成 S1×S1S^1 \times S^1S1×S1 並畫成要怎麼三角化呢？通常會簡化成這怎麼變成幾何形狀的？注意到標為同一個名稱的那些線，那表示那其實是同一條線。這需要定義一個 simplicial set S\mathcal{S}S（Hint: 根據定義是個 contravariant functor），其資訊如下： S[0]= {p}S[1]= {l0,l1,l2}S[2]= {a,b}Sδi(lj)= pSδi(a)= liSδi(b)= l2−i\begin{aligned} \mathcal{S}[0] =\ &\{ p \} \\ \mathcal{S}[1] =\ &\{ l0, l1, l2 \} \\ \mathcal{S}[2] =\ &\{ a, b \} \\ \mathcal{S}\delta_i(l_j) =\ &p \\ \math
2025/12/13 00:00https://dannypsnl.me/math-001J
Integrating Mathlive into editor.js and Thoughts on Note-Taking Systems
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: x^2 + y^2 = 1 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: He
2025/11/23 00:00https://dannypsnl.me/programming-0004
Impredicative
參考 https://github.com/AndrasKovacs/elaboration-zoo/tree/master/06-first-class-poly In type theory [local-0] A universe is impredicative if function types whose codomains are in the universe are always in the universe, regardless of their domain types. foo:(a:Uk)→…\text{foo} : (a : U_k) \to \ldotsfoo:(a:Uk )→… 如果 foo:Uk\text{foo} : U_kfoo:Uk 可以通過檢查，這個 Universe UkU_kUk 就是 impredicative 的，有 impredicative universe 存在的類型理論就叫做有 impredicativity。像 Rocq 或是 Lean 都有特殊的 Prop universe 有這樣的特性。 In Elaboratio
2025/10/12 00:00https://dannypsnl.me/tt-000V
sauron supports find references in project
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 Everyti
2025/9/11 00:00https://dannypsnl.me/programming-0003
TeXmacs
最近因為朋友提及，所以真正嘗試了 TeXmacs https://www.texmacs.org/ 這個軟體，感受到什麼是所見即所得應有的樣貌，於是想寫下一點介紹。由於 TeXmacs 做的特別好的是數學公式編輯，所以我們集中在這件事上。在 TeXmacs 中輸入 $ 就會立即創造一個 math 區塊，用 Ctrl + $ 則會創造置中的 math 區塊（$ 係指 Shift + 4，本文的快捷鍵皆為 MacOS 上的情況，在其他系統需注意差異）。 cursor 的所在區塊會被淺藍色框標記，範例如下被選擇的區塊，會用紅色標記。用鍵盤或是滑鼠都可以選取在 math 區塊中輸入分數時，鍵入 \frac 然後按下 Space，就會出現上下兩個區塊其中紫色的是 cursor，可以用上下鍵切換要在哪個區塊繼續輸入次方也是同理對於等號，也有特殊的操作可以使用，比如選擇等號後按下 Ctrl + A，就會在正上方出現輸入區塊最後，還有一些數學常見的段落，都已經寫成樣板可以直接插入：插入結果
2025/7/24 00:00https://dannypsnl.me/software-0008
My exploring Borsuk-Ulam Theorem
My exploration (around April, 2025) of Borsuk-Ulam theorem began with trying to prove the Lyusternik-Shnirel'man closed theorem for S1S^1S1 and S2S^2S2. 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:Sn→Rnf : S^n \to \mathbb{R}^nf:Sn→Rn, there exists a point x∈Snx \in S^nx∈Sn such that f(x)=f(−x)f(x) = f(-x)f(x)=f(−x). The Failed Stereographic Approach [local-0] My initial idea w
2025/7/1 00:00https://dannypsnl.me/math-000U
Determinant 的意義
從矩陣非常難看出 determinant 的意義，但它其實具備幾何的意涵：對 nnn 個向量張出的高維平行體的體積影響。矩陣 AAA 可以視為張量 V⊗V∗V \otimes V^*V⊗V∗，向量張出的高維平行體可以表示為 exterior product v1∧⋯∧vnv_1 \wedge \dots \wedge v_nv1 ∧⋯∧vn 。因此定義 det A\det AdetA 如下： det A(v1∧⋯∧vn)=Av1∧⋯∧Avn\det A (v_1 \wedge \dots \wedge v_n) = A v_1 \wedge \dots \wedge A v_ndetA(v1 ∧⋯∧vn )=Av1 ∧⋯∧Avn 這表示 AAA 把 viv_ivi 映射到 AviA v_iAvi 所得的新高維平行體的體積相對於先前的高維平行體的比例（可能會正負轉換）。補充：當 dim V=N\dim V = NdimV=N 時。NNN 階 skew-symmetric tensor 的空間 ΛNV\Lambda^N VΛNV 很明顯只有一個維度，這個空間在 Lectures
2025/6/17 00:00https://dannypsnl.me/math-000Q
部落格遷移
最近終於自己寫了個 site generator tr，這套機制確實是解決我很多問題，所以就開始遷移舊的部落格了。原則上大部分文章或是筆記都不會跟過來，因為這也是趁機丟掉一些已經過時/太簡單的筆記的機會，tr 讓我可以直接嵌入 wiki/nLab 來取代解釋基礎的定義。
2025/6/6 00:00https://dannypsnl.me/blog-0000
NixOS 需要定期清除 generations
這是今天遇到的問題，更新系統時它提示 /boot/ 的空間不足以安裝 efi 檔案了，直接砍 /boot/EFI/nixos/ 裡面的檔案是沒有用的，因為 NixOS 的 generations 會重新生成這些資料。所以正確的作法是先執行下面的指令 cd /nix/var/nix/profiles 裡面會有很多像是 system-數字-link 這樣的 soft links，每一個對應一個 NixOS 的 generation。把太古老的 generations 刪掉，執行 nix store gc 這會跑一段時間（如果你跟我一樣太久沒有清理就需要很久），結束之後再次更新系統就可以了。
2025/5/17 00:00https://dannypsnl.me/software-0000
何謂 elaboration？
elaboration 指的是轉換沒有語意的表面語法（surface syntax 或是說 source code）到有語意的語言表示（language representation）的過程，這樣講可能有點抽象，所以需要一些例子。試問 foo(a, b) 這段 Go source code 有語意嗎？事實上是沒有，因為只有在 Go compiler 經過讀取文字解析語法取得語法樹型別以及其他檢查現在這段程式碼才會在 Go compiler 內部用某種資料結構表示，而 Go compiler 可以相信這段程式碼是滿足 Go 規範的程式，這樣才是有語意的語言。這個觀點一開始對你來說可能蠻怪異的，但我們可以仔細來看這樣定義的好處有些語言如 Fennel https://fennel-lang.org/ 刻意把自己變成另一個語言 Lua 的另類文法，在語言表示層面要求共用一樣的語意。Fennel 還支援了 macro 系統語法可以作為片段，嵌入到任何位置，只不過後續的檢查階段可能拒絕嵌入後產生的語法，因為這樣產生的程式依然可能是語法或是語意不正確的，比如使用 C 語言的 prepr
2025/2/6 00:00https://dannypsnl.me/cs-0004
什麼是 subroutine？
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 就被發明了：找個 regi
2025/1/28 00:00https://dannypsnl.me/cs-0006
作業系統的行程排程
在一些非常簡單的作業系統實現裡面，會乾脆讓 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 用光之後（或是它的指令執行完畢）就可以被切斷。
2025/1/28 00:00https://dannypsnl.me/cs-0007
Transformation induced dual basis
Manifolds and Differential Geometry Let e1,e2,…,en∈Ve_1, e_2, \dots, e_n \in Ve1 ,e2 ,…,en ∈V be a basis of vector space VVV, and let e1,…,en∈V∗e^1, \dots, e^n \in V^*e1,…,en∈V∗ be a basis of dual space V∗V^*V∗. Now if eˉi=C ikek\bar{e}_i = C^k_{\ \ i} e_keˉi =C ik ek is another basis of VVV, then there is an induced basis eˉi=(C−1) kiek\bar{e}^i = (C^{-1})^i_{\ \ k} e^keˉi=(C−1) ki ek for dual space V∗V^*V∗. Proof [local-0] By Kronecker-delta 1=δ ii1 = \delta^i_{\ i}1=δ ii 1=δ ii=eˉieˉi=C ike
2024/12/31 00:00https://dannypsnl.me/math-000D
用 effect handler 實作 parser combinator
這些程式碼都是使用 OCaml 實現，並使用了 algeff 與 asai 程式庫解析器需要完成的任務就是根據規則把一系列 tokens 變成文法樹，並且回報為何解析失敗，一般大學作業等級的編譯器都會讓學生直接使用解析器生成器，如 menhir 這種工具。然而實際上開發真實語言的解析器時，往往會遇到需要錯誤恢復並繼續解析，最後再回報多個錯誤的要求，這時候生成器往往給出很差的結果，甚至乾脆就是做不到的。然而，手工編寫的解析器通常可維護性相當差劣。一種折衷的方案是所謂的解析器組合子，我過去也曾經介紹過如何利用組合子抽象掉重複的解析規則。但這種方案有個問題，就是回溯必須手動使用 try 組合子來在失敗時恢復狀態，但實務上這創造了相當難以理解的各種 try 安插，當我意識到這是因為 API 需要是兩階段的問題時，我就發現其實 effect handler 正是解決這個問題的好方法。我本來是直接使用 Effect.Deep 的，但後來發現這種情境直接用 algeff 就足夠了，因此改採這個方案。實際程式碼如下 module Tokens = struct type t = Lexer.to
2024/9/23 00:00https://dannypsnl.me/VSMS
Elaboration zoo 中的合一演算法與隱式參數
程式語言為了讓使用者省略不必要的輸入，必須為使用者推導內容，這種需求催生了合一這種類型的演算法。比如很多程式語言允許泛型，比如下面的 OCaml 程式碼 let id (x : 'a) : 'a = x Elaboration zoo 這個教學專案，它的程式碼要解決的，是一類更複雜的程式語言，叫做 dependent type 的系統中的合一問題，這類系統最重要的特性，就是類型也只是一種值，值也因此可以出現在類型中，但這就比較不是本篇的重點，有興趣的讀者可以閱讀 The Little Typer 來入門。在解釋完它的合一之後，我會介紹它隱式參數的解決方案 Algorithm 合一演算法的過程 [tt-0007] 假設有程式碼 let id {A : U} (x : A) : A := x let id2 {B : U} (x : B) : B := id _ x 這裡 id _ x 中的底線表示「省略的引數」，被稱為 hole，我們並沒有明確的給它任何值，比如 B。在展開這個 hole 時，我們用 meta variable ?0 替換它。但 meta variable 必須考慮 co
2024/9/22 00:00https://dannypsnl.me/tt-0006
使用 TLA+ 的第一步
由於很多 TLA+ 入門教學似乎都沒有談到實務上要從哪裡開始使用 TLA+，所以這裡我想介紹實際上要怎麼做。一個 TLA+ 的檔案以 .tla 為副檔名，其中由 --- MODULE name --- 開頭，由 === 結尾，例如 ---- MODULE plustwo ---- ===== 在其中可以引用模組，寫成 EXTENDS xxx, yyy, ... ---- MODULE plustwo ---- EXTENDS Integers ===== 使用 PlusCal 語言 [tla-0001]2024-08-27 比起直接寫出 Spec 等不變式，先寫 PlusCal language (https://lamport.azurewebsites.net/tla/tutorial/intro.html) 的程式再使用用它生成的 Spec 不變量會更簡單也更實用。因為 TLA+ 會嘗試生成所有可能的狀態，有可能出現所謂的 unbound model (https://learntla.com/topics/unbound-models.html)，就結果而言對它進行檢查永遠不會
2024/8/27 00:00https://dannypsnl.me/tla-0000
racket 中的有界續延如何實作 effect system 的功能？
racket 中的有界續延如何實作 effect system 的功能？2024-08-27Lîm Tsú-thuàn討論如何用 racket 中的 continuation 實作 effect system 的概念一個 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 sy
2024/8/27 00:00https://dannypsnl.me/cs-000G
The concept of webmention
Each web page should provide the following content (use my site dannypsnl.me as example) in sender view [webmention-0001]2024-07-30 According to webmention spec, if someone tries to notify my site that there is a link mentions my post, she has to do the following: curl -I https://dannypsnl.me/xxx to get my webmention endpoint in the head post the data, where is the link refers to my post POST /webmention-endpoint HTTP/1.1
2024/7/30 00:00https://dannypsnl.me/webmention-0000
無外部空間下如何考慮幾何空間的測量？
metric 就是在測量長度。不過在歐式空間裡面討論嵌入其中的曲面時，曲面有外部空間切向量，也就是歐式空間的向量可以使用。如果曲面沒有外空間，就需要自己做一個出來，這就引出了 Riemann metric 的想法：對可微分流形 MMM 的每一點 ppp 考慮抽象的切空間 TpMT_pMTp M（不考慮 TpMT_pMTp M 到底是什麼），重點是隨點附上內積函數 g:TpM×TpM→Rg : T_pM \times T_pM \to Rg:Tp M×Tp M→R，因為是模仿內積所以有 bilinearity, positive-definiteness, symmetry 等性質現在考慮曲線 y:[0,1]→My : [0, 1] \to My:[0,1]→M，在每一點度量 TpMT_pMTp M 向量並積分（加起來）即是曲線長度。又隨著區間 t:[0,1]t : [0, 1]t:[0,1] 改變，會有對應變化的 ppp 點，因此模仿並定義 length(y)=∫01g(dydt,dydt)dt\text{length}(y) = \int_0^1 \sqrt{g(\frac{dy}
2024/7/1 00:00https://dannypsnl.me/math-0001
為什麼需要 domain theory？遞迴的數學表示
一般的 OCaml 函數可以寫成 let f x y z = ... 一個直覺的想法是：每個型別都解釋成一個可數集合，該型別的 term 解釋成這個集合的元素。但有些函數會用到自己本身，例如整數階乘函數 let rec fac n = if n = 0 then 1 else n * fac(n-1) 它的值是什麼呢？答案是 μ(x:int→int).λ(n:int).{1(n=0)n×x(n−1)(n≠0)\mu (x : int \to int). \lambda (n : int). \begin{aligned} \begin{cases} 1 &\quad &(n = 0) \\ n \times x(n-1) &\quad &(n \ne 0) \end{cases} \end{aligned}μ(x:int→int).λ(n:int).{1n×x(n−1) (n=0)(n=0) μ\muμ 中的 xxx 就是 fac 自己，把原始 OCaml 程式中的 fac 換成 xxx 即可。問題是集合論沒有辦法充分解釋這個運算，具體來說，集合解釋不滿足 PCF 的 Adeq
2023/12/9 00:00https://dannypsnl.me/math-28UX
Soundness and completeness
Classical logic's soundness says, if ⊢clα\vdash_{cl} \alpha⊢cl α, then α\alphaα is classically valid. Classical logic's completeness says, if α\alphaα is classically valid, then ⊢clα\vdash_{cl} \alpha⊢cl α. 可以看到，要用 soundness 與 completeness 時，是在關心特定屬性 p，我們說一個系統 sound 就是在問「系統能導出的結果是否滿足 p」；我們說一個系統 complete 則是在問「滿足 p 的結果是否皆能從系統導出」。
2023/11/27 00:00https://dannypsnl.me/math-0000
A space is Hausdorff iff its diagonal map is closed
The proposition says a space is Hausdorff if and only if its diagonal map Δ:X→X×X\Delta : X \to X \times XΔ:X→X×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 Δ={(x,x)∣x∈X} \Delta = \{ (x, x) \mid x \in X \} Δ={(x,x)∣x∈X} Not hard to see below argument also applies to all finite XXX-product spaces. Proof [local-0] (Hausdorff => diagonal map is closed) Hausdorff means every t
2023/11/23 00:00https://dannypsnl.me/math-000B
understanding <math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math>F-algebra
To understand FFF-algebra, we will need some observations, the first one is we can summarize an algebra with a signature. For example, monoid has a signature: {1:1→m⋅:m×m→m\begin{cases} 1 : 1 \to m \\ \cdot : m \times m \to m \end{cases}{1:1→m⋅:m×m→m or we can say ring is: {0:1→m1:1→m+:m×m→m×:m×m→m−:m→m\begin{cases} 0 : 1 \to m \\ 1 : 1 \to m \\ + : m \times m \to m \\ \times : m \times m \to m \\ - : m \to m \end{cases}⎩⎨⎧ 0:1→m1:1→m+:m×m→m×:m×m→m−:m→m The next observation is we can consider
2023/10/24 00:00https://dannypsnl.me/math-000E
Lawvere's fixed point theorem 的陳述與應用
這篇文章試著介紹 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→ϕBAA \xrightarrow{\phi} B^AAϕ BA 是 point-surjective，則所有 B→fBB \xrightarrow{f} BBf B 都存在不動點 1→sB1 \xrightarrow{s} B1s B（滿足 f∘s=sf \circ s = sf∘s=s）。 Proof [local-0] 首先畫出交換圖其中 δ\deltaδ 的定義是 c↦⟨c,c⟩c \mapsto \langle c, c \ranglec↦⟨c,c⟩，所以對 1→pA1 \xrightarrow{p} A1p A 來說 δ∘p=⟨p,p⟩\delta \circ p = \langle p, p \rangl
2023/10/11 00:00https://dannypsnl.me/math-0005

本頁 50 篇

從有限元素中隨機取未使用的元素
元素集合可以轉換為正整數集合，因此問題可以寫成：給定範圍 [0,N)[0, N)[0,N)，已使用之數字集合為 UUU，最簡單的演算法就是排除 UUU [0,N)∖U[0, N) \setminus U[0,N)∖U 從中隨機取一個元素問題 [local-0] 然而排除已使用元素是固定成本，在已使用元素會變多的情況下更是越來越大的成本。隨機抽一個，再查看有沒有撞上已經使用的位置反而更有效。但這樣做的界線到底在哪裡？幾何分布 [local-1] 對於空間大小 NNN 與已使用的 UUU，隨機抽一個位址命中未使用元素的機率是 p=N−∣U∣Np = \frac{N - |U|}{N}p=NN−∣U∣ 假設每次抽樣互相獨立，那「抽到第 kkk 次才第一次成功」服從幾何分布 (1−p)k−1p(1-p)^{k-1} p(1−p)k−1p 連續 kkk 次都失敗（選到已使用的位置）的機率是 (1−p)k(1 - p)^k(1−p)k，期望次數是 1/p=NN−∣U∣1/p = \frac{N}{N - |U|}1/p=N−∣U∣N 所以我們可以看到 ∣U∣|U|∣U∣ 只佔 NNN 一小
2026/9/1 00:00https://dannypsnl.me/tr-D6VS
部落格作為一個fediverse帳號
延續部落格問題挑戰的規劃，我研究了怎麼讓blog作為fediverse帳號存在。我希望部落格文章會得到一個fediverse post，有人在fediverse上跟post互動時，可以在部落格本體看到變化。這樣就等於借用了fediverse作為留言系統這個專案公開端點是 https://fedi.dannypsnl.me，借用大量的Cloudflare（CF）功能與Fedify完成： D1：跟隨者、貼文、互動 KV：Fedify的快取 Queue：投遞跟收信 R2：貼文附圖的儲存 ActivityPub需要什麼？ [local-0] 一個fediverse帳號是一個HTTP服務，要能回答這幾件事： /@blog：actor，帳號本身 /@blog/inbox：別人寄東西來的地方 /@blog/outbox、followers、following：這個帳號的公開集合 /.well-known/webfinger：把 @[email protected] 這個名字換成上面那個actor的網址這些都能用Fedify處理，因為要簽HTTP Signatures，這塊很麻煩所以要盡
2026/8/30 00:00https://dannypsnl.me/8664
部落格問題挑戰
看ltlnx的部落格時看到這個挑戰，剛好也想寫點什麼所以就來寫吧！你當初為什麼開始寫部落格？你使用什麼平台來管理你的部落格？為什麼選擇它？你之前有在其他平台上寫過部落格文章嗎？你如何撰寫文章？例如，使用本地編輯工具，還是在部落格的後台／控制面板中編寫？你什麼時候最有寫作靈感？你會在寫完後立即發布，還是會先存成草稿醞釀一下？你部落格上最喜歡的文章是哪一篇？你對部落格有什麼未來計畫嗎？例如重新設計、搬到另一個平台，或是加入新功能？你當初為什麼開始寫部落格？ [local-0] 當初只是想紀錄一些學習上的問題，因為那時候看到「學東西最好的方式就是教別人」，所以就順便把筆記變成部落格你使用什麼平台來管理你的部落格？為什麼選擇它？ [local-1] 我用自己開發的靜態網站產生器tr-notes，工具的網站 https://tr-notes.srht.site/ tr-notes的起源是我使用forester的時候一直遇到breaking changes，但大抵上來說我覺得這種軟體很好用（可以讀 https://www.forester-notes.org/QHXS/inde
2026/8/18 00:00https://dannypsnl.me/MNIW
To CPS or not to CPS：編譯理論之爭
在什麼是CPS？我們討論過CPS是怎樣的程式風格，以及編譯器可以怎麼利用這種風格。但我們該不該使用CPS呢？這曾經引發一系列的爭論編譯理論之爭 [local-0] 1978 RABBIT: A Compiler for SCHEME，據說這是最早採用CPS的編譯器 1992 Compiling with Continuations，Appel整理並提供了完整的ML CPS風格編譯器 1993 The essence of compiling with continuations，形式化並辨識出ANF，認為direct style (ANF) 在local control flow上提供了更簡單的工作方式 1997 A reflection on call-by-value，這篇正式的討論了direct style在什麼時候可以替代CPS編譯器 2007 Compiling with continuations, continued，Kennedy認為CPS在functional language上有勝過ANF或是monadic IR的地方，主要爭點就是inline會導致ANF需要re
2026/7/29 00:00https://dannypsnl.me/ASEH
色彩繽紛的範疇論
我在這裡想要用範疇論（category theory，又稱抽象廢話）展示跟大家印象中不一樣的數學，有興趣深入學習的讀者可以在最後找到進一步的學習資源。範疇論是從代數拓樸、代數幾何等領域的發展中自然出現的概念，主要的用途是用來高效地描述物之間的關係、用一種抽象的視角觀察整體性質。下面舉一些例子幫助你大致理解一下範疇論在數學領域的定位，看不懂或是想跳過都沒差，並不影響後續閱讀 Example 數學中的Categories與Functors [local-0] 我們有所有集合與函數的範疇 Sets\text{Sets}Sets、所有群與群態射的範疇 Groups\text{Groups}Groups Monoid MMM 的Actions可以改寫成functor Mop→SetsM^{op} \to \text{Sets}Mop→Sets（事實上這類functor有個特殊名稱，叫做presheaf）拓樸空間 XXX 的所有開集之間的包含關係構成一個category Open(X)\text{Open}(X)Open(X) 遺忘functor，比如 Groups→Sets\text{Grou
2026/7/15 00:00https://dannypsnl.me/Z00L
J-sheaf 的直覺
JJJ-sheaf 的概念有點難解，這個定義是在模擬從小的opens（局部）往大的opens（整體）前進的時候，每個在整體上的定義都可以分成局部的定義，而局部的定義黏起來會得到整體的定義這樣的匹配性，而且局部之間的交疊必須匹配。對於具體的sheaf，可以參考這裡從topological space的opens構成的locale抽象化到category之後，我們就從opens變成操作objects；coverings變成sieves；在open XXX 上定義的某類函數抽象化成presheaf，因為我們想讓框架適用於所有類型的函數，而且我們發現函數並不是必要的條件，我們只需要這些東西在某個意義上表現的像函數，因此presheaf僅僅是說，對於object XXX 會有一個對應的集合，並且在morphism上我們contravariant（以符合幾何的直覺）。JJJ-sheaf也因此等於在問，對於這樣抽象的 topology 與「函數」，什麽算是在交集處互相同意對方的值？ category中沒有交集的概念，sieve的composition closure確保了如果 f∈Sf \in S
2026/7/10 00:00https://dannypsnl.me/LPLF
Brid.gy cross-post 的使用方法
Brid.gy cross-post 的使用方法2026-06-23Lîm Tsú-thuànbridgy cross-post 的使用方法因為我無法記住兩年前怎麼設定的 brid.gy，所以再次調查怎麼做然後寫下來。brid.gy 的首頁長這樣，像我是需要貼到 mastodon 所以就按 mastodon 按鈕接著會出現兩個選項我們這種用法要選的是 Cross-post to a Mastodon account @[email protected] 輸入你的 mastodon instance，取得授權之後，你的文章裡面只要有 microformat 應該就能用用來發佈了
2026/6/23 00:00https://dannypsnl.me/CIEP
Soufflé 入門
Soufflé是高效能的Typed Datalog引擎，能把宣告式規則編譯成C++，或用直譯器模式執行 fact 與 rule [local-0] fact（已知的事實）與 rule（能從事實推導新事實的規則）。先宣告一個輸入關係，代表「模組a直接相依於模組b」 // 代表 a 直接 import b .decl depends(a: symbol, b: symbol) .input depends .decl 宣告關係的名字與各欄位型別（symbol 是字串，另一個常用型別是 number）。.input 表示資料從外部讀入：預設是從同名的 depends.facts 檔案，每行一筆、以 Tab 分隔。接著我們定義第一條規則：模組若被任何人相依，就是「被使用的」 .decl used(m: symbol) used(m) :- depends(_, m). 讀法是「對任意 m，若存在 depends(_, m)，則 used(m) 成立」。:- 右邊是body（前提），左邊是head（結論），_ 是 wildcard，表示「有就好、是誰都可以」。開發者不用管理控制流程：規則評估結果
2026/6/21 00:00https://dannypsnl.me/programming-0TXN
日本北陸之旅 2025/10 能登
因為《放學後失眠的你》裡面的夜景（真脇遺跡）太漂亮了，所以我一直想要去能登一次想不到再來發生了能登半島地震，直到這次旅程，能登半島沿途大部分的道路都還在整修中，有臨時紅綠燈跟工程人員管制（單側輪流通行），隨處可見大災難的痕跡第一日（飛機/住宿） [hokuriku-day1] 在桃園機場隨意吃過午餐，坐上 12:10 起飛、往日本海岸線去的班機在降落小松之前在日本海上轉向，往陸地飛去，經過軍機場之後 16:05 降落在小松機場。小松並不大，主要都在等過海關，下了樓之後因為接駁車等待人數不少，擔心可能要再等一班，於是坐計程車去小松車站，買了類似台灣區間車的車票做到金澤站這台火車的座椅很有趣，有一個機械結構，乘客可以把座椅調整成對向四人座，或是兩人座。飯店 checkin 完畢再去找晚餐，這時候市場已經快關了，而且很多店大排長龍，就隨便找一間吃第二日（能登第一日） [hokuriku-day2] 這天的目標是先去 ORIX 取車，然後開去千里濱凪沙道路，取車前還有一點時間，先跑去看鼓門這一整日都陰雨綿綿，在取車之後在市區開了大概一個多小時之後來到千里濱，才發現因為海嘯的緣故，下
2026/6/19 00:00https://dannypsnl.me/VW5V
善與善的對抗
討厭推薦演算法、討厭廣告、討厭 AI、討厭生活壓力、討厭別人、討厭自己但行好事，莫問前程願自己不要原地踏步。但善與善的對抗之中，什麼是好事？
2026/6/15 00:00https://dannypsnl.me/BF9W
violet literate programming 支援
之前其實就有弄過一次但效果很不好，現在 LSP server 已經建立，基於 interaction 抽象層讀取資料產出 html 效果就好上很多 Example 初步實驗的效果 [violet-0000]2026-06-13 目前是用 violet weave 從一個 .vt.scrbl 編譯。程式碼區塊由 violet 前處理：@vt|{…}| 的內容會被抽出、型別檢查，轉成帶標記的 HTML。其餘內容原樣交給 tr-notes 把游標移到 identifiers 上時可以看到型別；調用部分連結到它的定義；?here 這樣的 goal 會顯示 context 與 target \universe US U \let id(A : universe U) -> (_ : A) -> A (Auniverse U : Uuniverse S U) : Auniverse U -> Auniverse U \where xA \let ex(A : universe U) -> (_ : A) -> A (Auniverse U : Uuni
2026/6/14 00:00https://dannypsnl.me/D1AX
轉移控制權作為 effect：coroutine 與排程器
這是 effect 系列的第三篇，這篇要解釋怎麼用 effect 攔截 coroutines 的 yield 並重新排程。所謂的 coroutines，就是一些互相約定好會主動讓出執行權利，互相「協作」的函數。是 continuation 極其常見的使用案例，首先我們先設定 abort 部分： (define sched-tag (make-continuation-prompt-tag 'sched)) (define (yield) (call/cc (lambda (k) (abort/cc sched-tag k)))) 可以看到 yield 就是預設外部會有一個 prompt (effect handler) 等著自己，於是它就把自己的 continuation 捕獲起來丟出去給 handler 我們需要一個地方存放還沒有做完的任務，所以定義了一個 queue tasks spawn 單純就是把任務推入 queue 中排隊 continue 的目的是提供 handler 等待 thunk 的 yield 再次把執行權釋出 (define tasks (make-queue)
2026/5/20 00:00https://dannypsnl.me/Y7OR
violet 的一點新進展
申請了 domain https://violet-lang.org/ 給 violet 使用。比較大的變化是 Inductive types 可以生成相應的 eliminator 的類型與計算重新設計了 constructors 的 namespace，@ice1000 說的是對的，constructors 被放到 namespace 之下其實影響不大，要用時再打開，或是設計表面語法就可以了提供 \operator 讓開發者自己定義需要的運算式語法，比如 \operator "\x + \y" => add x y \associativity: \left 模組現在預設是 private，並新增 \export 關鍵字建立了 project 概念，現在可以用 info.vt 管理專案依賴，進一步可以參考 https://github.com/violet-prover/std kernel 加入內建的 record 下一步？ [local-0] 現在的 <= \elim 並不處理有任何帶有非純變數參數的 elimination target，因為這會導致 eliminator
2026/5/17 00:00https://dannypsnl.me/ILIG
用 effect system 實現直釋器
這是 effect 系列的第二篇，這篇要展示的是用 effect 攔截對 environment 的查詢。所以第一步我們要定義一個攔截 effect (define lookup-tag (make-continuation-prompt-tag 'lookup)) (define (lookup x) (call/cc (lambda (k) (abort/cc lookup-tag k x)))) 第二步我們建立執行函數 EVAL，但我們建立一個 go 輔助函數，讓最上層負責攔截找不到 variables 時的查找，並提供沒有該 variable 的錯誤訊息。這裏跟一般直譯器實現的主要差異就是我們不需要傳 env 這樣的變數，這通常是某個 environment 實現（比如 hashmap 或是一些值構成的 list，由 de Bruijn indicies 參照）的實例 (define (go tm) (match tm [(? symbol? tm) (lookup tm)] [(? number? tm) tm] [`(+ ,@a) (apply + (map go a))]
2026/5/10 00:00https://dannypsnl.me/SW6P
正確處理單位的算術系統
在做物理或工程上的算術時，我們常常會在單位上出錯：把公尺加到秒上、把公斤乘進長度卻沒有標記，或是次方算錯，最後得到一個「數字看起來合理」但單位錯亂的結果。這些錯誤在紙筆運算時不容易被察覺，發現的時候往往已經是好幾步之後，回頭檢查非常的麻煩能不能讓工具替我們把關呢？如果單位本身就是型別的一部分，編譯器就能在我們把不相容的東西硬湊在一起時直接拒絕。我們可以用 Agda 來規範出這樣的一個系統用 Agda 實現單位正確的算術 [ag-OW40] {-# OPTIONS --safe --without-K #-} module ag-OW40 where open import MLTT.Spartan hiding (_+_) open import MLTT.Negation open import MLTT.List open import MGS.MLTT using (has-decidable-equality) open import Integers.Type open import Integers.Addition open import Integers.Multi
2026/5/7 00:00https://dannypsnl.me/S20M
以 effect 為合約：用 effect system 解耦遍歷演算法與存取點
我以前寫過一篇文章介紹 effect system，看過之後的回饋基本上有兩種哇靠這也太抽象了，到底在說什麼那 effect system 到底對我們日常的程式開發有什麼用？所以我打算利用零碎的時間寫寫各種應用範例，而這篇就是關於如何用 effect system 將遍歷演算法與 visit 處理分離。我想不重複 racket 中的有界續延如何實作 effect system 的功能？已經介紹過的各個 racket API，所以直接用程式案例說明。比如今天我們想要走訪 binary tree，以 inorder 走訪可以寫成 (define (dfs t) (match t [(list v L R) (dfs L) (visit v) (dfs R)] [v (visit v)])) 我們單純認定 (list root-value L-tree R-tree) 這樣的格式是 binary tree，這很可能不是最好的寫法，不過以這裡要講的概念來說，重點在 visit 是什麼，所以我們先看一下實現要記得用 (require racket/control) 引入 racket/c
2026/4/10 00:00https://dannypsnl.me/4Z05
RSS in emacs：elfeed
I've been trying some Emacs packages, including elfeed and meow, but the latter is not the topic of this post. I will briefly introduce elfeed package. I use straight.el to install packages: (use-package elfeed :custom (elfeed-feeds '("https://dannypsnl.srht.site/rss.xml"))) elfeed-feeds is where you configure the feeds. Here I use my personal site as an example. Use M-x elfeed to open a buffer of elfeed. In this buffer, pressing G will fetch and refresh the feeds. Once articles are listed, pres
2026/2/14 00:00https://dannypsnl.me/EHWW
Pattern Unification演算法理論部分
在這篇文章裡面我想要探討 Elaboration Zoo 裡面的 pattern unification 演算法怎麼算出來的，以及在什麼時候成立。主要是了解我們怎麼導出等式： ?α=?rhs′[spm−1] ?\alpha \overset{?}{=} \text{rhs}'[sp_m^{-1}] ?α=?rhs′[spm−1 ] 超越 Elaboration zoo 中的合一演算法與隱式參數僅是直覺的推理。在 Display map category 我們已經了解到，contexts 跟 substitutions 構成了一個範疇，而我們想要知道的是 epimorphism 的定義，所以 Kovacs 的第一步是把 epimorphism 定義改寫成更適合這個案例的定義 Definition Epimorphism [local-0] 我們說 Sub Γ ΔSub\ \Gamma\ \DeltaSub Γ Δ 是 epimorphism iff δ∘σ=δ′∘σ⇒δ=δ′A[σ]=A′[σ]⇒A=A′\begin{aligned} \delta \circ \sigma = \de
2026/2/13 00:00https://dannypsnl.me/F6C1
安裝 Guix
下載之後按照系統安裝文件描述的方式把 iso 燒錄到 USB or DVD，插入電腦開始安裝。基本上現在的引導介面已經跟 ubuntu 之類的老牌 distribution 相當了，只要按照螢幕上說的逐步回答就能設定完成。它的 root 跟一般帳號是明確分開的，密碼也不同，在設定完 root 密碼之後會要求建立至少一個一般帳號。partition 分成兩種，按照需求選擇就好。最後選介面時有很多選擇，Gnome、KDE、Sway 都有，這個也是習慣用什麼就選什麼就行了。這之後就會開始安裝，跑完之後重開機（boot 管理要記得切換到安裝好的系統才不會又跑進 installer）。到這裡就可以看 https://guix.gnu.org/manual/1.5.0/en/html_node/Getting-Started-with-the-System.html 文件開始編輯 /etc/config.scm 了。
2026/2/5 00:00https://dannypsnl.me/B4OI
2026 - Week 5
Racket 中的 concurrent programming [local-0] 想到就測試 rakka 跟 Racket coroutine thread 結果 native 還比較快XD，所以我就把 genserver 做成 Racket thread 封裝了 https://repo.dannypsnl.me/dannypsnl/erl。至於為什麼 coroutine thread 這麼快，我猜可能 CS 之後有很大改善，我之前沒有注意到這點 JIT [local-1] 延續上個禮拜的工作，用手搓的 JIT 實現 brainfuck 編譯器 brainfuck JIT Racket language server [local-2] racket-langserver 這個 PR 的目的是改善目前一團糟的測試體驗。現在的方式是啟動 subprocess 然後跟它的 stdio 互動，一來這意味著大量的系統資源需求，二來耦合這麼重就很難設計可以遠端連線的 server。所以第一步需要清理現在的設計，引入間接層讓測試只需要跟這個抽象部分互動就好 racket-llvm [loca
2026/1/28 00:00https://dannypsnl.me/2026-W5
2026 - Week 4
試著寫了 JIT 框架，研究了 JIT: Write XOR Execute policy 怎麼實現。目前放在 https://repo.dannypsnl.me/dannypsnl/still-compiling/src/branch/main/dynasm 中，目前還遠遠不成熟，可能做幾個 example 之後才會考慮釋出
2026/1/26 00:00https://dannypsnl.me/2026-W4
Rakka 使用初體驗
最近發現 racket 生態系裡面出現一個 Rakka 程式庫，它似乎把 Erlang 大部分一階抽象都做出來了，這是我個人想像很久的寫法，所以我當然很有興趣去嘗試。我的第一個實驗是針對的 sauron 內部程式庫 collector 進行重構。collector 原本就是模仿 Erlang 的訊息傳遞方式來抽象，使用 rakka 之後，我直接把這些抽象邏輯寫成 GenServer 的形式。結果發現效果非常不錯程式碼數量減少：collector 的程式碼量變成原來的大約三分之二。維護性提升：整體結構變得更好維護。所以之後遇到類似的需求，我就會考慮使用 rakka 處理，我就不用再寫處理訊息傳遞風格的樣板式重複程式碼了。而且它還實現了 EPMD protocol，可以跟其他 node 互動。
2026/1/9 00:00https://dannypsnl.me/GMYW
Display map category 捕捉了類型論的什麼面向？
要理解 Display map category 的定義（參考 Categorical Logic and Type Theory, Definition 10.4.1），我們需要理解它的動機跟捕捉問題的方式，因此我們要觀察一個個相繼式（我假設讀者已經熟練相繼式定義的類型論），並用範疇論（category theory）的語言重述。在用相繼式描述類型論時，公式 Γ⊢A type\Gamma \vdash A \text{ type}Γ⊢A type 表示 Γ\GammaΓ 可派生出類型 AAA。對於所有 Γ\GammaΓ 可派生的類型，我們用 Ty(Γ)Ty(\Gamma)Ty(Γ) 表示，所以我們也會用 A∈Ty(Γ)A \in Ty(\Gamma)A∈Ty(Γ) 來表示上面的相繼式。Display map category 捕捉的第一件事就是 contexts 構成一個 category，我們用 C\mathcal{C}C 記號表示這個範疇，並且我們要求 C\mathcal{C}C 有 terminal object ⋄\diamond⋄，用來表示空的 context。 cont
2026/1/6 00:00https://dannypsnl.me/tt-BBGG
現代 - 商業、科技與政治交織的空間
讓我們先從 LLM 開始談起，我認為 Context Widows 的觀點很適合開始理解問題在哪裡。問題不在 LLM 或是廣泛的 AI 領域有用或是沒用，正如 Context Widows 一文自己所說跟我從其他地方看到的，正面的產出確實存在，像是蛋白質折疊材料科學用壓縮映射模擬星系演變而可質疑的問題也一直存在：幻覺、缺乏理解。更不用說直接的負面影響氣候佔用能源（包含在天災時電網供電給計算中心而不是醫院）剽竊創意 Context Widows 真正要談的是，比起問 LLM 有沒有用，更恰當的問題是：LLM 能否有效地融入科學知識的創造、驗證和傳播過程中？ LLM 能否有效地融入科學知識的創造、驗證和傳播過程中？ [local-0] 由於一項技術的潛在用途並非其實際用途，而實際用途又取決於採用該技術的機構、機構試圖解決的問題以及機構用作衡量成功的既有指標。所以 Context Widows 認為探討 LLM 與科學的關係，等若詢問 LLM 出現之前，科學界已經運作著怎樣的體系？我們知道當代科學界的主導是引用體系，隨著時間發展，引用體系已經改變它本要量測的對象；科學家會調整
2025/12/30 00:00https://dannypsnl.me/U5YI
2025 年
今年開源的一點貢獻自己弄了個網站生成工具 tr 弄懂怎麼生成 induction principle 參與了一點 Yoxem 的 SICP 台語翻譯計畫 agda-mode-vscode 提示 unicode 符號輸入方式讓 magic-racket 可以開啟 macro 展開過程的互動 GUI 用來除錯 racket-langserver 的維護，今年底突然獲得管理權限xd 然後我下定決心研究了 epub 檔案格式，讓我更清楚可以對這些書籍檔案做什麼xd。因為年初我自己立的目標是看懂 mirror symmetry，數學我今年大致上學了 mirror symmetry 的表示論前提 k\mathbb{k}k-linear category cochain complex: 一系列 vector spaces CiC^iCi（或是 graded vector spaces）加上一個 degree 1 的 linear map ddd cohomology: ddd 按組成取 Ker dIm d\frac{\text{Ker}\ d}{\text{Im}\ d}Im dKer d
2025/12/28 00:00https://dannypsnl.me/2025
Rhombus 用標記運算自動排序資料
最近在研究 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]，因為這個標記會自動進行排序運算！
2025/12/15 00:00https://dannypsnl.me/programming-0005
具體的 simplicial set: Torus
simplex 要怎麼跟幾何扯上關係？這是因為 up to homotopy，我們可以把幾何形狀變形成用一群三角形（確切的來說是一些 simplex）表示的形狀。這裡要講的案例 Torus 是一個二維度的幾何曲面，一般定義成 S1×S1S^1 \times S^1S1×S1 並畫成要怎麼三角化呢？通常會簡化成這怎麼變成幾何形狀的？注意到標為同一個名稱的那些線，那表示那其實是同一條線。這需要定義一個 simplicial set S\mathcal{S}S（Hint: 根據定義是個 contravariant functor），其資訊如下： S[0]= {p}S[1]= {l0,l1,l2}S[2]= {a,b}Sδi(lj)= pSδi(a)= liSδi(b)= l2−i\begin{aligned} \mathcal{S}[0] =\ &\{ p \} \\ \mathcal{S}[1] =\ &\{ l0, l1, l2 \} \\ \mathcal{S}[2] =\ &\{ a, b \} \\ \mathcal{S}\delta_i(l_j) =\ &p \\ \math
2025/12/13 00:00https://dannypsnl.me/math-001J
Integrating Mathlive into editor.js and Thoughts on Note-Taking Systems
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: x^2 + y^2 = 1 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: He
2025/11/23 00:00https://dannypsnl.me/programming-0004
Impredicative
參考 https://github.com/AndrasKovacs/elaboration-zoo/tree/master/06-first-class-poly In type theory [local-0] A universe is impredicative if function types whose codomains are in the universe are always in the universe, regardless of their domain types. foo:(a:Uk)→…\text{foo} : (a : U_k) \to \ldotsfoo:(a:Uk )→… 如果 foo:Uk\text{foo} : U_kfoo:Uk 可以通過檢查，這個 Universe UkU_kUk 就是 impredicative 的，有 impredicative universe 存在的類型理論就叫做有 impredicativity。像 Rocq 或是 Lean 都有特殊的 Prop universe 有這樣的特性。 In Elaboratio
2025/10/12 00:00https://dannypsnl.me/tt-000V
sauron supports find references in project
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 Everyti
2025/9/11 00:00https://dannypsnl.me/programming-0003
TeXmacs
最近因為朋友提及，所以真正嘗試了 TeXmacs https://www.texmacs.org/ 這個軟體，感受到什麼是所見即所得應有的樣貌，於是想寫下一點介紹。由於 TeXmacs 做的特別好的是數學公式編輯，所以我們集中在這件事上。在 TeXmacs 中輸入 $ 就會立即創造一個 math 區塊，用 Ctrl + $ 則會創造置中的 math 區塊（$ 係指 Shift + 4，本文的快捷鍵皆為 MacOS 上的情況，在其他系統需注意差異）。 cursor 的所在區塊會被淺藍色框標記，範例如下被選擇的區塊，會用紅色標記。用鍵盤或是滑鼠都可以選取在 math 區塊中輸入分數時，鍵入 \frac 然後按下 Space，就會出現上下兩個區塊其中紫色的是 cursor，可以用上下鍵切換要在哪個區塊繼續輸入次方也是同理對於等號，也有特殊的操作可以使用，比如選擇等號後按下 Ctrl + A，就會在正上方出現輸入區塊最後，還有一些數學常見的段落，都已經寫成樣板可以直接插入：插入結果
2025/7/24 00:00https://dannypsnl.me/software-0008
My exploring Borsuk-Ulam Theorem
My exploration (around April, 2025) of Borsuk-Ulam theorem began with trying to prove the Lyusternik-Shnirel'man closed theorem for S1S^1S1 and S2S^2S2. 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:Sn→Rnf : S^n \to \mathbb{R}^nf:Sn→Rn, there exists a point x∈Snx \in S^nx∈Sn such that f(x)=f(−x)f(x) = f(-x)f(x)=f(−x). The Failed Stereographic Approach [local-0] My initial idea w
2025/7/1 00:00https://dannypsnl.me/math-000U
Determinant 的意義
從矩陣非常難看出 determinant 的意義，但它其實具備幾何的意涵：對 nnn 個向量張出的高維平行體的體積影響。矩陣 AAA 可以視為張量 V⊗V∗V \otimes V^*V⊗V∗，向量張出的高維平行體可以表示為 exterior product v1∧⋯∧vnv_1 \wedge \dots \wedge v_nv1 ∧⋯∧vn 。因此定義 det A\det AdetA 如下： det A(v1∧⋯∧vn)=Av1∧⋯∧Avn\det A (v_1 \wedge \dots \wedge v_n) = A v_1 \wedge \dots \wedge A v_ndetA(v1 ∧⋯∧vn )=Av1 ∧⋯∧Avn 這表示 AAA 把 viv_ivi 映射到 AviA v_iAvi 所得的新高維平行體的體積相對於先前的高維平行體的比例（可能會正負轉換）。補充：當 dim V=N\dim V = NdimV=N 時。NNN 階 skew-symmetric tensor 的空間 ΛNV\Lambda^N VΛNV 很明顯只有一個維度，這個空間在 Lectures
2025/6/17 00:00https://dannypsnl.me/math-000Q
部落格遷移
最近終於自己寫了個 site generator tr，這套機制確實是解決我很多問題，所以就開始遷移舊的部落格了。原則上大部分文章或是筆記都不會跟過來，因為這也是趁機丟掉一些已經過時/太簡單的筆記的機會，tr 讓我可以直接嵌入 wiki/nLab 來取代解釋基礎的定義。
2025/6/6 00:00https://dannypsnl.me/blog-0000
NixOS 需要定期清除 generations
這是今天遇到的問題，更新系統時它提示 /boot/ 的空間不足以安裝 efi 檔案了，直接砍 /boot/EFI/nixos/ 裡面的檔案是沒有用的，因為 NixOS 的 generations 會重新生成這些資料。所以正確的作法是先執行下面的指令 cd /nix/var/nix/profiles 裡面會有很多像是 system-數字-link 這樣的 soft links，每一個對應一個 NixOS 的 generation。把太古老的 generations 刪掉，執行 nix store gc 這會跑一段時間（如果你跟我一樣太久沒有清理就需要很久），結束之後再次更新系統就可以了。
2025/5/17 00:00https://dannypsnl.me/software-0000
何謂 elaboration？
elaboration 指的是轉換沒有語意的表面語法（surface syntax 或是說 source code）到有語意的語言表示（language representation）的過程，這樣講可能有點抽象，所以需要一些例子。試問 foo(a, b) 這段 Go source code 有語意嗎？事實上是沒有，因為只有在 Go compiler 經過讀取文字解析語法取得語法樹型別以及其他檢查現在這段程式碼才會在 Go compiler 內部用某種資料結構表示，而 Go compiler 可以相信這段程式碼是滿足 Go 規範的程式，這樣才是有語意的語言。這個觀點一開始對你來說可能蠻怪異的，但我們可以仔細來看這樣定義的好處有些語言如 Fennel https://fennel-lang.org/ 刻意把自己變成另一個語言 Lua 的另類文法，在語言表示層面要求共用一樣的語意。Fennel 還支援了 macro 系統語法可以作為片段，嵌入到任何位置，只不過後續的檢查階段可能拒絕嵌入後產生的語法，因為這樣產生的程式依然可能是語法或是語意不正確的，比如使用 C 語言的 prepr
2025/2/6 00:00https://dannypsnl.me/cs-0004
什麼是 subroutine？
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 就被發明了：找個 regi
2025/1/28 00:00https://dannypsnl.me/cs-0006
作業系統的行程排程
在一些非常簡單的作業系統實現裡面，會乾脆讓 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 用光之後（或是它的指令執行完畢）就可以被切斷。
2025/1/28 00:00https://dannypsnl.me/cs-0007
Transformation induced dual basis
Manifolds and Differential Geometry Let e1,e2,…,en∈Ve_1, e_2, \dots, e_n \in Ve1 ,e2 ,…,en ∈V be a basis of vector space VVV, and let e1,…,en∈V∗e^1, \dots, e^n \in V^*e1,…,en∈V∗ be a basis of dual space V∗V^*V∗. Now if eˉi=C ikek\bar{e}_i = C^k_{\ \ i} e_keˉi =C ik ek is another basis of VVV, then there is an induced basis eˉi=(C−1) kiek\bar{e}^i = (C^{-1})^i_{\ \ k} e^keˉi=(C−1) ki ek for dual space V∗V^*V∗. Proof [local-0] By Kronecker-delta 1=δ ii1 = \delta^i_{\ i}1=δ ii 1=δ ii=eˉieˉi=C ike
2024/12/31 00:00https://dannypsnl.me/math-000D
用 effect handler 實作 parser combinator
這些程式碼都是使用 OCaml 實現，並使用了 algeff 與 asai 程式庫解析器需要完成的任務就是根據規則把一系列 tokens 變成文法樹，並且回報為何解析失敗，一般大學作業等級的編譯器都會讓學生直接使用解析器生成器，如 menhir 這種工具。然而實際上開發真實語言的解析器時，往往會遇到需要錯誤恢復並繼續解析，最後再回報多個錯誤的要求，這時候生成器往往給出很差的結果，甚至乾脆就是做不到的。然而，手工編寫的解析器通常可維護性相當差劣。一種折衷的方案是所謂的解析器組合子，我過去也曾經介紹過如何利用組合子抽象掉重複的解析規則。但這種方案有個問題，就是回溯必須手動使用 try 組合子來在失敗時恢復狀態，但實務上這創造了相當難以理解的各種 try 安插，當我意識到這是因為 API 需要是兩階段的問題時，我就發現其實 effect handler 正是解決這個問題的好方法。我本來是直接使用 Effect.Deep 的，但後來發現這種情境直接用 algeff 就足夠了，因此改採這個方案。實際程式碼如下 module Tokens = struct type t = Lexer.to
2024/9/23 00:00https://dannypsnl.me/VSMS
Elaboration zoo 中的合一演算法與隱式參數
程式語言為了讓使用者省略不必要的輸入，必須為使用者推導內容，這種需求催生了合一這種類型的演算法。比如很多程式語言允許泛型，比如下面的 OCaml 程式碼 let id (x : 'a) : 'a = x Elaboration zoo 這個教學專案，它的程式碼要解決的，是一類更複雜的程式語言，叫做 dependent type 的系統中的合一問題，這類系統最重要的特性，就是類型也只是一種值，值也因此可以出現在類型中，但這就比較不是本篇的重點，有興趣的讀者可以閱讀 The Little Typer 來入門。在解釋完它的合一之後，我會介紹它隱式參數的解決方案 Algorithm 合一演算法的過程 [tt-0007] 假設有程式碼 let id {A : U} (x : A) : A := x let id2 {B : U} (x : B) : B := id _ x 這裡 id _ x 中的底線表示「省略的引數」，被稱為 hole，我們並沒有明確的給它任何值，比如 B。在展開這個 hole 時，我們用 meta variable ?0 替換它。但 meta variable 必須考慮 co
2024/9/22 00:00https://dannypsnl.me/tt-0006
使用 TLA+ 的第一步
由於很多 TLA+ 入門教學似乎都沒有談到實務上要從哪裡開始使用 TLA+，所以這裡我想介紹實際上要怎麼做。一個 TLA+ 的檔案以 .tla 為副檔名，其中由 --- MODULE name --- 開頭，由 === 結尾，例如 ---- MODULE plustwo ---- ===== 在其中可以引用模組，寫成 EXTENDS xxx, yyy, ... ---- MODULE plustwo ---- EXTENDS Integers ===== 使用 PlusCal 語言 [tla-0001]2024-08-27 比起直接寫出 Spec 等不變式，先寫 PlusCal language (https://lamport.azurewebsites.net/tla/tutorial/intro.html) 的程式再使用用它生成的 Spec 不變量會更簡單也更實用。因為 TLA+ 會嘗試生成所有可能的狀態，有可能出現所謂的 unbound model (https://learntla.com/topics/unbound-models.html)，就結果而言對它進行檢查永遠不會
2024/8/27 00:00https://dannypsnl.me/tla-0000
racket 中的有界續延如何實作 effect system 的功能？
racket 中的有界續延如何實作 effect system 的功能？2024-08-27Lîm Tsú-thuàn討論如何用 racket 中的 continuation 實作 effect system 的概念一個 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 sy
2024/8/27 00:00https://dannypsnl.me/cs-000G
The concept of webmention
Each web page should provide the following content (use my site dannypsnl.me as example) in sender view [webmention-0001]2024-07-30 According to webmention spec, if someone tries to notify my site that there is a link mentions my post, she has to do the following: curl -I https://dannypsnl.me/xxx to get my webmention endpoint in the head post the data, where is the link refers to my post POST /webmention-endpoint HTTP/1.1
2024/7/30 00:00https://dannypsnl.me/webmention-0000
無外部空間下如何考慮幾何空間的測量？
metric 就是在測量長度。不過在歐式空間裡面討論嵌入其中的曲面時，曲面有外部空間切向量，也就是歐式空間的向量可以使用。如果曲面沒有外空間，就需要自己做一個出來，這就引出了 Riemann metric 的想法：對可微分流形 MMM 的每一點 ppp 考慮抽象的切空間 TpMT_pMTp M（不考慮 TpMT_pMTp M 到底是什麼），重點是隨點附上內積函數 g:TpM×TpM→Rg : T_pM \times T_pM \to Rg:Tp M×Tp M→R，因為是模仿內積所以有 bilinearity, positive-definiteness, symmetry 等性質現在考慮曲線 y:[0,1]→My : [0, 1] \to My:[0,1]→M，在每一點度量 TpMT_pMTp M 向量並積分（加起來）即是曲線長度。又隨著區間 t:[0,1]t : [0, 1]t:[0,1] 改變，會有對應變化的 ppp 點，因此模仿並定義 length(y)=∫01g(dydt,dydt)dt\text{length}(y) = \int_0^1 \sqrt{g(\frac{dy}
2024/7/1 00:00https://dannypsnl.me/math-0001
為什麼需要 domain theory？遞迴的數學表示
一般的 OCaml 函數可以寫成 let f x y z = ... 一個直覺的想法是：每個型別都解釋成一個可數集合，該型別的 term 解釋成這個集合的元素。但有些函數會用到自己本身，例如整數階乘函數 let rec fac n = if n = 0 then 1 else n * fac(n-1) 它的值是什麼呢？答案是 μ(x:int→int).λ(n:int).{1(n=0)n×x(n−1)(n≠0)\mu (x : int \to int). \lambda (n : int). \begin{aligned} \begin{cases} 1 &\quad &(n = 0) \\ n \times x(n-1) &\quad &(n \ne 0) \end{cases} \end{aligned}μ(x:int→int).λ(n:int).{1n×x(n−1) (n=0)(n=0) μ\muμ 中的 xxx 就是 fac 自己，把原始 OCaml 程式中的 fac 換成 xxx 即可。問題是集合論沒有辦法充分解釋這個運算，具體來說，集合解釋不滿足 PCF 的 Adeq
2023/12/9 00:00https://dannypsnl.me/math-28UX
Soundness and completeness
Classical logic's soundness says, if ⊢clα\vdash_{cl} \alpha⊢cl α, then α\alphaα is classically valid. Classical logic's completeness says, if α\alphaα is classically valid, then ⊢clα\vdash_{cl} \alpha⊢cl α. 可以看到，要用 soundness 與 completeness 時，是在關心特定屬性 p，我們說一個系統 sound 就是在問「系統能導出的結果是否滿足 p」；我們說一個系統 complete 則是在問「滿足 p 的結果是否皆能從系統導出」。
2023/11/27 00:00https://dannypsnl.me/math-0000
A space is Hausdorff iff its diagonal map is closed
The proposition says a space is Hausdorff if and only if its diagonal map Δ:X→X×X\Delta : X \to X \times XΔ:X→X×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 Δ={(x,x)∣x∈X} \Delta = \{ (x, x) \mid x \in X \} Δ={(x,x)∣x∈X} Not hard to see below argument also applies to all finite XXX-product spaces. Proof [local-0] (Hausdorff => diagonal map is closed) Hausdorff means every t
2023/11/23 00:00https://dannypsnl.me/math-000B
understanding <math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math>F-algebra
To understand FFF-algebra, we will need some observations, the first one is we can summarize an algebra with a signature. For example, monoid has a signature: {1:1→m⋅:m×m→m\begin{cases} 1 : 1 \to m \\ \cdot : m \times m \to m \end{cases}{1:1→m⋅:m×m→m or we can say ring is: {0:1→m1:1→m+:m×m→m×:m×m→m−:m→m\begin{cases} 0 : 1 \to m \\ 1 : 1 \to m \\ + : m \times m \to m \\ \times : m \times m \to m \\ - : m \to m \end{cases}⎩⎨⎧ 0:1→m1:1→m+:m×m→m×:m×m→m−:m→m The next observation is we can consider
2023/10/24 00:00https://dannypsnl.me/math-000E
Lawvere's fixed point theorem 的陳述與應用
這篇文章試著介紹 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→ϕBAA \xrightarrow{\phi} B^AAϕ BA 是 point-surjective，則所有 B→fBB \xrightarrow{f} BBf B 都存在不動點 1→sB1 \xrightarrow{s} B1s B（滿足 f∘s=sf \circ s = sf∘s=s）。 Proof [local-0] 首先畫出交換圖其中 δ\deltaδ 的定義是 c↦⟨c,c⟩c \mapsto \langle c, c \ranglec↦⟨c,c⟩，所以對 1→pA1 \xrightarrow{p} A1p A 來說 δ∘p=⟨p,p⟩\delta \circ p = \langle p, p \rangl
2023/10/11 00:00https://dannypsnl.me/math-0005

最近被這些部落格提到

Hi 我劉昕〈超級多的「有趣的小知識或冷門概念」：BlogBlog 同樂會主持人回顧文〉2026/8/3 00:00
Lîm Tsú-thuàn 的「色彩繽紛的範疇論」向我們介紹了…… 範疇論，非常數學的數學，我先自首我跟不上裡面的內容。…

用 RSS 訂閱誰提到這個部落格

引用與交流近 90 天

全站關係圖 →

正文直接引用

被誰提到

Hi 我劉昕1 篇引用占比 1.5%最近 2026/8/3

核對正文連結（列出 1 筆連結）

Hi 我劉昕提到本站：超級多的「有趣的小知識或冷門概念」：BlogBlog 同樂會主持人回顧文→色彩繽紛的範疇論
「Lîm Tsú-thuàn 的「色彩繽紛的範疇論」向我們介紹了…… 範疇論，非常數學的數學，我先自首我跟不上裡面的內容。但範疇論似乎是以拓撲學為基礎而被提出，我就在場邊給大家暖暖場吧。你知道嗎？在拓撲學中，吸管、甜甜圈、馬克杯是同胚的（含有一個貫穿的洞），而如果不要太在意細節的話，其實所有後口動物——包含所有脊索動物、棘皮動物——也跟吸管、甜甜圈、馬克杯是同胚的。但如果在意一下細節的話，其實人有七或八個洞就是了。」
文章 #2546 · 發表 2026/8/3 · 位置正文 · 摘要取自正文 · 比對版本 semantic-links-v3 · 觀測 2026/10/16

近 90 天話題

近 90 天話題

最新收錄

最近被這些部落格提到

引用與交流近 90 天

正文直接引用

被誰提到

最近常寫的話題

使用的技術

主機與 CDN（低信心）

近 90 天話題