Zero Calorie Drink Shop

笔记 10 异常和 continuations

用马桶吃饭的已经吃完饭回家了，饭盒原教旨主义团队还在加班洗碗，还拉着食品安全团队陪他们。

HTTP 1.1 200 OK
Date: Sat, 23 Aug 2025 21:30:37 GMT
Content-type: application/json; charset=utf-8
Content-length: 39


{"status":403,"message":"权限不足"}

在社区中你可能听到一种说法：在 unsafe 块里你可以像 C¹ 语言那样写。然而事实并不是这样，C 语言的约束太差，事实上给了程序员太多“宽松”的东西。而在 Rust 里，unsafe 真的很 unsafe —— 当你要接管编译器为你做的安全保证，危险就暗藏在其中。

协程（Coroutine）是一种计算机控制流结构，它允许代码块在执行过程中显式地暂停并恢复，同时保留其执行状态（包括调用栈、变量、上下文等），从而实现协同式多任务处理。

曾经一直没有太搞懂协程这个概念是什么。于是写下这样的一篇文章，尝试对自己解释协程是什么

注册表打开：HKEY_LOCAL_MACHINE\SOFTWARE\Microsoft\Windows\Dwm 新增一个 OverlayTestMode 的 DWORD 项，值为 5 重启即可

Point-free style can (clearly) lead to Obfuscation when used unwisely. As higher-order functions are chained together, it can become harder to mentally infer the types of expressions. The mental cues to an expression’s type (explicit function arguments, and the number of arguments) go missing.

https://wiki.haskell.org/Pointfree

Standard ML（SML），是一个函数式、指令式、模块化的通用的编程语言，具有编译时间类型检查和类型推论。它流行于编译器作者和编程语言研究者和自动定理证明研究者之中。

虽然这玩意是 1983 年的老登了，但是还能看到许多比较现代的东西——不得不感叹 PL 与工程语言的割裂。1972 年 C 语言被发明，1973 年 ML 被发明，一边是 void* 满天飞的弱类型语言，一边已经是用了 Hindley-Milner 类型推论的 sound 的语言了。

总而言之读了一下 Programing in Standard ML (又是你啊， Robert Harper) ，写写对 Standard ML 的主观感受

笔记 8 子类型

TL;DR：简而言之，代数效应是一种机制，允许在不破坏函数式编程纯度的前提下，更加结构化和组合化地处理副作用。

习题来自 https://bartoszmilewski.com/2014/11/24/types-and-functions/

唉早知道就不折腾这种全世界都找不出一万个人在用的东西了.txt

前言： unplugin-vue-router 是 unplugin 的一款插件，旨在在 src/pages 等目录下使用文件驱动的 routing 来避免手写 vue-router 配置带来的麻烦与潜在的失误，是约定优于配置的一个展现。

vite-plugin-vue-layouts 是与 unplugin-vue-router 非常般配的一款插件，旨在为 views 指定共享的 layout，在复杂前端工程上或许非常有用。

二者是 vuetify 前端框架推荐使用的插件。

然后就被它的【刻意的设计】坑了一把

笔记 7

此时对于我那幽默的《编译原理》课程还在用 C 语言写编译器的不满达到了顶峰。

你说得对，但是《编译原理》是由 Alfred V. Aho, Monica S. Lam, Ravi Sethi 和 Jeffrey D. Ullman 等人自主研发的一款全旧计算机世界编程游戏。游戏发生在一个被称作「C—」的简化语言，在这里，选择这门课的人将被迫享受「GCC 7.5.0」，没有一点 5202 年该有的体验。玩家将扮演一位名为「C 程序员」的神秘角色，在自由的编码中邂逅各种各样、时机诡异的 Segment Fault 们，和他们一起泄露内存，感受 C 语言的恶心之处——同时，逐步发掘「都 5202 年了这帮人还在拿 39 年前的书教文法分析」的真相。

但跑远了。总而言之这里介绍一种叫 parser combinator —— 解析器组合子的函数式手段，为您带来哪怕是手写递归下降也很舒适的体验（并非）

在之前的文章中我尝试了一下 Lean4 定理证明器——然后我是在并非干这个方向的所以后面就抛在脑后了

后面因为学习函数式语言于是又捡起了 Lean4 函数式编程，然后……好吧我真的不得不说真香啊

所以不要再说强类型了啊！！

链表可以当成双端队列来使用——至少在渐进时空复杂度上，它们是相同的。

但在现代化的 CPU 的支持下，std::vector 由于内存的连贯性，在小规模数据下甚至可以做到比 std::deque 更好的性能，更别提在随机访问上 std::vector 有巨大优势了。

简单的说单子(Monad)就是自函子范畴上的一个幺半群 👀 你说这个谁懂啊

笔记 6 最详细的一集，因为我要讲解这部分（摊手 但是读得很开心！这章真是让我受益匪浅啊！

笔记 5

Practical Foundations for Programming Languages 是 Robert Harper 的一本书，而这是我写的笔记 4

Practical Foundations for Programming Languages 是 Robert Harper 的一本书，而这是我写的笔记 3

陪伴我 4 年的及腰长发其实都到臀部了今日卒，谨以此发文对其表达深切的悼念（）

久闻 Zig 语言大名，作为一众底层语言的有力竞争者，Zig 被常常认为是 better C。Zig 自己也说，“Zig 与 C 竞争，而不是依赖于它”。前天用 Zig 写了一个简单的命令行跨平台贪吃蛇游戏，也算是体验了一下 Zig 的有趣功能。

Practical Foundations for Programming Languages 是 Robert Harper 的一本书，而这是我写的笔记 2

A blogging guide, built for minimalists who aren’t quite as nerdy.

Practical Foundations for Programming Languages 是 Robert Harper 的一本书，而这是我写的笔记

Gleam is a friendly language for building type-safe systems that scale! —— https://gleam.run/

虽然我倒不觉得纯函数式语言能有多 friendly……

写这个解析器主要是为了看自己的 C++ 水平，毕竟 JSON 是一个同时能做到语法简单的同时考验人的编码水平的 data structure，其次是为了好玩。 好玩吗？好玩。

This blog was written entirely because of the item Familiarize yourself with alternatives to overloading on universal references in Effcetive Morden C++. We start with a practical problem trying to emulate std::optional in C++14, because optional monads are a good paradigm for expressing values ​​that may be null, rather than assuming everything is maybe null which can easily break through the type system. 写下这篇文章完全是因为看到了 Effcetive Morden C++ 中的熟悉通用引用重载的替代方法。我们从一个现实的问题开始，即在 C++14 尝试模拟 std::optional，因为 optional 是表达可能为空的值的时候一个很好的范式，而不是假定一切都可能为 null 并轻易击穿类型系统。

Impressions of the programming languages I have come across

谁喜欢 Python 啊，反正我不喜欢。

Extreme 难度的 Slice 过关了，终于可以自称类型体操入门了（喜）

This blog post was inspired by my classmate who encountered pip’s dependencies hell when configuring machine learning python code. Yeah, for my academics-immersed amateur of industy, environment configuration and package managers are very unfamiliar things. It’s not strange to crash into hell.

Sometimes it’s simply impossible to find a combination of package versions that do not conflict. Welcome to dependency hell.

一时兴起想写一个随机句子生成器。正巧在学上下文无关语言 (Context-Free Language, CFL)，意识到句子的结构很大程度上是一个上下文无关语法。查阅 X-bar 理论得到也确实类似如此。

同时正好在学 Rust，所以试了一下拿 Rust 编写这个生成器，并编译到 WebAssembly (WASM)。效果很成功！

花了几个小时写下了 So Simple.

这是一个致力于“尽可能少写 CSS”的主题。实际上也确实，整个主题几乎全部是裸的 HTML。排列从上到下，没有什么值得插入的元素，就像在读报纸一样。

这个主题是返璞归真的一次尝试。希望它能让我满意。

一篇简短的笔记，为 Misskey 开启 Meilisearch 后，重新索引过去的帖子。

我是去年的 11 月知道的 Firefish。它是我当时找到的最美丽的联邦宇宙软件，相比于死板的 Mastodon，过于倾向于日语又太娱乐的 Misskey，它同时兼具美观大方与功能丰富。管理员可以自由配置最大帖子长度，Nodejs 的后端也让它比 Ruby on Rails 编写的 Mastodon 对性能要求更低。我欣然安装上了它，并把它作为自己的主要联邦宇宙软件。

可惜，当时我还不知道它的状态已经岌岌可危。就在当时，原有的主要贡献者大多已经离开，panos 和 namekuji 离开了这摊烂摊子开启了新项目 Catodon。数个月后，Firefish 的 maintainer Kainoa 就直接撒手不管，在没有事先告知的情况下将 maintainer 更改给 naskya。naskya 非常负责且具有热爱，在伊的代理下 Firefish 回光返照了一段时间 —— 我也是那个时候尝试了为 Firefish 进行贡献。

可惜 maintainer 的名头为伊带来了巨大的压力与恶心的网络骚扰者。 naskya 的身体和精神状态都无法负担这样的项目，不到一年之后，Firefish 再次被抛弃。这次，大约再也没人能救 Firefish 了。

我在 2018 年建立这个博客以后，就一直没有换过其它博客平台。试过 Wordpress，也试过 Writefreely，总还是没有 Hexo 之类的静态站点生成器来得又快又好。当然现在似乎更流行别的结构了，Hugo，vuepress，毕竟 Hexo 已经是个有十来岁的老家伙了。在前端，十年足以发生翻天覆地的变化，而 Hexo 已经被远远的甩在后头。

实际上，我对 Hexo 多少有一点恋旧情绪，毕竟它是我第一次尝试自建博客，也是我第一次尝试 Contribute 到开源项目。截至我写的时候，这个博客使用的主题 Anatolo 还是我 Star 数最高的个人项目。

但 Hexo 的确是老了。正如我的朋友所说，Hexo 的表演该落幕了，让它退场吧。 Hexo 大多数主题都是用的是裸的 <script> 标签引入前端库，少有主题加入代码压缩，几乎没有主题使用过 typescript。 文档也疏于维护， hexo-utils 更是代码奇奇怪怪 。

但我还是不忍心彻底放弃 Hexo。因此，我花了一个晚上的时间，对我博客的 Client 进行了重写。同时也是为了探索，像 Hexo 这样的老东西还可不可能与现代化的前端技术相集成。

说真的，Hexo 这么烂下去我真要换 Hugo 了——为什么它甚至不支持给 hljs 添加语言插件？

好吧，这篇博客讲述如何让你的 Hexo 博客支持高亮 Lean，并且是后端渲染。

Lean 4 是一个功能强大的交互式定理证明器和编程语言，结合了逻辑推理与编程，主要用于形式化验证、数学证明以及高可靠性软件开发。Lean 4 提供了一个灵活的类型系统和高性能的编译器，使其在理论研究和实际应用中都有出色表现。 —— GPT 说的。

F*ck 我为什么要去看这种东西啊（悲） —— 我说的

之前对于 Vue 的响应式封装（这里主要思考的是 computed），主要是用用，其实是懒得思考背后的原理的。毕竟原理其实可以用一句话说明：计算属性对别的属性产生有向的依赖关系，这个依赖关系构成一个有向无环图（DAG），图上的某个节点更新后重新计算其所有后置节点即可。

但是仔细想来，内部其实有一些时间复杂度的问题。显然，我们不能暴力调用回调函数（会卡出指数级时间复杂度 $O(2^n)$ 下面会详细解释）。同时朴素的做法很难解决这样的问题：

const a = ref([]);
const b = computed(() => a.join(","));
for (let i = 1; i <= n; i++) {
  a.value = a.value.concat([i]);
}

注意到对于一个网页而言，我们实际上期望 b 能在整个宏任务跑完以后才更新。所以实际上a.value 的 setter 触发的更新必须要进行推迟。

这篇文章讲讲我怎么在思考这些的过程中试着复刻一个 vue 的计算属性 computed 的

Latex 符号大全

前几天在思考，Python 和 JS 都拥抱了类型检查（类型注释），但是 Ruby 却只能用 Sorbet 这样的影响性能的类型检查器（Ruby 没有官方的类型检查工具，引入静态类型检查的 gem 反而降低了性能），在搜索中找到了 Crystal 这门语言。

https://crystal-lang.org/

看描述我就惊艳到了：作为一个静态语言，Crystal 居然长得这么像 Ruby，于是本着不妨玩玩的想法，我进行了 Crystal 的初试。

# A very basic HTTP server
require "http/server"

server = HTTP::Server.new do |context|
  context.response.content_type = "text/plain"
  context.response.print "Hello world, got #{context.request.path}!"
end

address = server.bind_tcp(8080)
puts "Listening on http://#{address}"

# This call blocks until the process is terminated
server.listen

简而言之，我写了一个可以查看Misskey/Firefish/Sharkey/…等Misskey系软件导出帖子存档的工具！

网址： https://lhcfl.github.io/misskey-archive-viewer-web

源代码： https://github.com/Lhcfl/misskey-archive-viewer

2023年10月18日， X (Twitter) 发布了一则公告，宣布他们在进行一项“测试”：在新西兰和菲律宾注册的新用户必须支付 $1 的年费才能在 X (twitter) 上和人互动。并且“在此测试中，现有用户不受影响”。
这促使我写下这篇文章：早该跑路了！如果之前的 Twitter 还努力营造一种“为了所有人”的印象，重视用户的黏性，Elon Musk的肆意妄为无疑是宣告 Twitter 终究是一个由公司掌握的营利性平台，而任何这样的大型中心化平台都不可避免的被少数人控制。国内平台尤甚，The big brother可以随意获取你的隐私，审查你的言论 (censorship)，无需理由就能禁言、封禁你的账户，随意关闭任何回答的评论区。你真的愿意让你使用社交平台的权利被拿捏在它们手中吗？

Mastodon 非营利组织的首席执行官兼 Mastodon 软件的首席开发者 Eugen Rochko（在联邦宇宙上被称为 Gargron）最近的举动让一些人担心 Mastodon（该软件项目和该非盈利组织）对 Fediverse 的其余部分造成的巨大影响。是的。我们的确应该担心。

$e^{i\pi} = -1$

这里将会显示一句话

联想电脑 wifi 无法使用，有时只需输入一条命令即可

sudo modprobe -r ideapad_laptop

Vim 的学习笔记