Functional

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 的主观感受

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

此时对于我那幽默的《编译原理》课程还在用 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 函数式编程，然后……好吧我真的不得不说真香啊

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

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

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

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

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