Zero Calorie Drink Shop

A childless azukisan lady who is miserable at her own live.

That is me. Only a nihilistic phantom.

Feed Github

Standard ML 尝旧

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

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

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

Code Functional Programing Language

碎碎念

本来不想在博客写这些的，不过算了写写吧。

vite-plugin-vue-layouts 使用记

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

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

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

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

学习在 Lean4 中使用 Parser Combinator

此时对于我那幽默的《编译原理》课程还在用 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 —— 解析器组合子的函数式手段，为您带来哪怕是手写递归下降也很舒适的体验（并非）

Code Lean Functional

2/9/2025

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

更好的 C 语言：Zig 初体验

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

Zig Code Programing Language

用 C++ 写一个玩具 JSON 库

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

Code C++

DIY std::optional: Using Universal References in C++

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 并轻易击穿类型系统。

Note C++ Code 双语

Introduction to Pass Principles

Abstract: Passness is part of the terminology of transition. Passness is the degree of likelihood that a transgender person is socially identified as the gender they identify with, and is a core part of pass theory, which is crucial to the quality of life of transgender people. However, distinguishing passness is not an easy task, and existing theories cannot address this issue well. There are several reasons. First, most known descriptions of passness are non-theoretical and cannot be accurately described by mathematical language. Second, there is a lack of rigorous specifications as a reference to classify a test trans as pass. Third, passness is stateful, and stateful pass testing remains challenging due to the large input space. In this paper, we propose several new passness testing systems called CBA to address the above challenges related to passness testing.

Joke

Package Manager: The History

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.

Code

一晚上搓出的 So Simple 博客主题

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

Screenshot of example website of SoSimple theme

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

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

Hexo Blog Frontend

再见 Firefish (Firefish 迁移 Sharkey 指北)

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

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

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

Fediverse Misskey Code Backend

在 Hexo 老瓶装新酒

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

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

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

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

Hexo Code

使 Hexo 支持高亮 Lean

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

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

Lean Hexo Blog Code

Lean 初见笔记

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

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

Math Programing Language Lean Code Functional

试着复刻一个vue的计算属性

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

但是仔细想来，内部其实有一些时间复杂度的问题。显然，我们不能暴力调用回调函数（会卡出指数级时间复杂度 O(2n)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 的

Frontend Javascript Algorithm Code

静态版Ruby？Crystal语言试用

前几天在思考，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

Crystal Programing Language Code

从中心化平台跑路：迁移到联邦宇宙（Fediverse）

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

Decentralized Fediverse Community

Mastodon的单一文化问题

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

Decentralized Fediverse Mastodon Community

一言

这里将会显示一句话