来自瑞典Linköping University的Filip Strömbäck老师来我们组访问，进行的一个名为Bootstrapping a Programming Language from Nothing的Seminar。本文的内容为基于此材料的个人理解。

经过前两周的奋战，我们终于摆脱了手写二进制、手动数字节的地狱。使用上次开发的工具我们已经可以像编写汇编代码一样比较舒适地开发了（尽管我们还要操心一下ELF文件头的填写和机器码的翻译，不过和之前相比已经好很多了）。下一步我们可以选择做一个真的汇编器，不过这同样困难且枯燥，而且对我们的开发体验提升不大。我是说，如果我们能现在就实现一个语义更高级的语言，我们为什么还需要汇编呢？不过，这真的能做到吗？

来自瑞典Linköping University的Filip Strömbäck老师来我们组访问，进行的一个名为Bootstrapping a Programming Language from Nothing的Seminar。本文的内容为基于此材料的个人理解。

在上一篇中我们手撸了一个十六进制编码器，可以支持解析文本文件，自动小端序输出，支持写注释。现在，至少我们不用一个个数的敲机器码了。

接下来要解决的是另一个反人类的事情：手动链接。在写上次的程序时，我们需要把每个跳转指令的目标地址一个个的掰手指数出来，这很麻烦。更麻烦的是，当你想修改程序导致字节数变化之后，这些地址都会变，完了要重新数重新填。于是，这次我们来解决这个问题，摆脱手动链接。

来自瑞典Linköping University的Filip Strömbäck老师来我们组访问，进行的一个名为Bootstrapping a Programming Language from Nothing的Seminar。本文的内容为基于此材料的个人理解。

设想你在一个无人岛上求生，身边只有一个x86电脑，上面除了Linux操作系统、文本编辑器之外什么都没有，作为没有好用的编程语言就会似的PL nerd，是时候捏着鼻子写机器码了……那我们开始吧！

你怎么知道我去ICFP2025了？

起因

半年前uu鼓励我把我阶段性的成果（真的有吗？）发表一下，也获得一些反馈，候选TyDe，ICFP和SPLASH的SRC。最后是参加ICFP了的SRC，我还从来没有参加过类似的活动，更是无法想象我还能因此去ICFP的，我印象里ICFP是只有中了牛逼论文才能去的牛逼会议。不过意外的是（？）我的SRC paper被accepted了，这意味着我真可以去ICFP了！其实至此我已经很知足了，但是uu说：你给我拿个奖回来，你不想我还想呢！

博客复活是怎么一回事呢？其实就是我看这个站有很多不喜欢的黑历史，所以一并清理掉了！

几百年前就想入门OCaml了，但是一直咕咕，现在终于下定决心学习一下。

前段时间入了个树莓派zero 2w玩玩，因为性能比较捉急，所以没有装桌面环境。

最近被问到了关于ADT的事情呢，于是想写一篇速通关于ADT、递归类型是怎么回事. 它面向了解过如何使用ADT，不过对ADT和递归类型的背后理论感兴趣的人，其他的部分我会尽可能self-contained.

本文是POPL2022同名文章的中文翻译，無断転載禁止。

关于match types的Scala文档：https://docs.scala-lang.org/scala3/reference/new-types/match-types.html

Type-level programming在FP越来越流行，但type-level programming和subtyping的组合还没有充分的探索。这篇文章中的match types等价于类型层面的pattern matching，在基于system F$_{<:}$的一个演算上形式化了match type这个feature，证明了它的soundness。在Scala3的reference compiler上实现了match types的系统。

本文为Type Theory and Formal Proof : An Introduction 的笔记，纯个人向（

之前我们遇到了以下的依赖关系：

• 依赖于项的项：$\lambda_\to$.
• 依赖于项的项$+$依赖于类型的项：$\lambda2$.
• 依赖于项的项$+$依赖于类型的类型：$\lambda\underline{\omega}$.

显然有一个扩展缺失了：

• 依赖于项的项$+$依赖于项的类型：$\lambda{\rm P}$.