Standard ML（SML），是一个函数式、指令式、模块化的通用的编程语言，具有编译时间类型检查和类型推论。它流行于编译器作者和编程语言研究者和自动定理证明研究者之中。
虽然这玩意是 1983 年的老登了，但是还能看到许多比较现代的东西——不得不感叹 PL 与工程语言的割裂。1972 年 C 语言被发明，1973 年 ML 被发明，一边是 void* 满天飞的弱类型语言，一边已经是用了 Hindley-Milner 类型推论的 sound 的语言了。
总而言之读了一下 Programing in Standard ML (又是你啊， Robert Harper) ，写写对 Standard ML 的主观感受
TL;DR：简而言之，代数效应是一种机制，允许在不破坏函数式编程纯度的前提下，更加结构化和组合化地处理副作用。
唉早知道就不折腾这种全世界都找不出一万个人在用的东西了.txt
简单的说单子(Monad)就是自函子范畴上的一个幺半群 👀 你说这个谁懂啊
Gleam is a friendly language for building type-safe systems that scale! —— https://gleam.run/
虽然我倒不觉得纯函数式语言能有多 friendly……
Lean 4 是一个功能强大的交互式定理证明器和编程语言，结合了逻辑推理与编程，主要用于形式化验证、数学证明以及高可靠性软件开发。Lean 4 提供了一个灵活的类型系统和高性能的编译器，使其在理论研究和实际应用中都有出色表现。 —— GPT 说的。
F*ck 我为什么要去看这种东西啊（悲） —— 我说的
前几天在思考，Python 和 JS 都拥抱了类型检查（类型注释），但是 Ruby 却只能用 Sorbet 这样的影响性能的类型检查器（Ruby 没有官方的类型检查工具，引入静态类型检查的 gem 反而降低了性能），在搜索中找到了 Crystal 这门语言。
看描述我就惊艳到了：作为一个静态语言，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