编程语言怎么不算一种小众软件呢
以下介绍的编程语言学了几乎可以保证你找不到相关工作，所以学着玩就好了
Crystal
接下来要说的语言都非常硬核，先搞点简单的语言缓冲一下
Crystal 可以说是静态类型版本的 Ruby，继承了大量的 Ruby 语法同时搞了一套很好的类型批注，妈妈再也不用担心你的日志里满是 undefined method xxx for nil (NoMethodError) 了
Crystal 是具有以下目标的编程语言：
- 和 Ruby 相似（但不要求兼容）的语法
- 静态类型检查，但不要求处处指定变量或者方法的类型
- 可以 call C 代码
- 对编译时进行评估和生成代码，避免 boilerplate code.
- 编译成高效的原生代码
这玩意的类型批注和 TypeScript 非常像，比如你可以写 Int32 | String 这个类型，它在底层相当于是一个用类型当 Tag 的 sum type
当然现在 Crystal 还是一门非常初生（？）的语言，嗯就是语法描述也不全，生态少得可怜，连编辑器提示都没有，各种地方都透露着种种不成熟
Crystal 有自动类型推断的功能。也就是说，大部分情况下类型声明可以直接不写，比如这样。但这玩意确实是个静态、native 语言而且既然后端是 LLVM，性能完全可以比肩 C++ 和 Rust
def add(a, b)
a + b
end
puts add(1, 2) # 3
puts add("1", "2") # "12"
这段代码有些类似于 C++这样写
template<typename A, typename B>
auto add(const A& a, const B& b) {
return a + b;
}
我个人很喜欢 Ruby 和 Crystal 一脉相承的一个想法：程序员的幸福最大化。 Ruby 是这样的，程序员只要负责写的爽就行了，而 Ruby 要考虑的事情就多了
即使 C++有 auto （更多静态类型语言会要求你写冗长的泛型），我们为什么不能更进一步呢？传入两个参数，把它们加起来。电脑理所应当可以从参数类型推导结果类型。那我为什么还要写呢？你已经是个成熟的编程语言了，该学会揣摩我到底要写什么类型了。我很喜欢。
Ruby 和 Crystal 都是特别面向对象的语言。比绝大多数自称面向对象的语言还要面向对象。
举个例子，Ruby/Crystal 支持这样的写法
3.times do |i|
puts i
end
# 输出：
# 0
# 1
# 2
这是因为哪怕是数字 3 也被视为一个对象，是 Object 的子类，可以有自己的 methods。而且你不用担心 Int 被视为对象会有性能问题，当年已经是 2014 了，早就不像某 Java 一样 Integer 和 int 一样必须明确区分了，编译器足够聪明知道什么东西能直接塞进寄存器里
所以在 Crystal 内可以写出这样极其直观的代码
puts 3.seconds # 00:00:03
puts 3.minute # 00:03:00
puts 3.hours # 03:00:00
puts 3.years # Time::MonthSpan(@value=36)
这些也可以传入到 sleep 中作为参数。sleep 3.seconds 即为 sleep3 秒，所有人一眼就能看懂，再也不用担心什么 sleep 传入的int参数到底是毫秒还是秒的问题。
Koka 语言
热身结束来点硬核的
Welcome to Koka – a strongly typed functional-style language with effect types and handlers.
Koka 是一门 research 语言，关键字看上去比较的 kotlin（？），特色是 first class 级的支持 algebraic effect。
Algebraic effect 是什么呢，可以理解成异常 Pro Plus Ultra，提供一种理论和能力，为副作用提供类型标注
如果你有什么代码洁癖的话可能会意识到在代码里用异常是一个比较危险需要谨慎的事情，因为现在的所有工业语言，异常都是没有类型批注的，最多支持到异常规格比如说老版本C++的
void foo() throw Exception1, Exception2
但这玩意一旦遇到高阶函数比如著名的 map 和 filter 就挂了，因为要给函数产生的可能的异常进行类型批注是一个比较困难的事情
一些现代语言比如 原神 Rust，还有 Go 之类的直接抛弃了异常，选择用返回值来描述错误，这种方式其实挺好，但还是增加了不必要的复杂度，比如你写 Go 会看到一大堆
if err != nil {
return nil, err
}
解决方式（当然我很怀疑这个解决方式是不是太复杂了，PL就这样搞出来的东西感觉普通程序员根本没有足够的智力能用）的其中之一是代数效应，核心思想是：我们可以把副作用进行传递和组合 。
比如如下 Koka 代码：
// combine-effects: forall<a> () -> <pure,ndet> a
fun combine-effects()
val i = srandom-int() // non-deterministic
throw("oops") // exception raising
combine-effects() // and non-terminating
分配给 combine-effects 的效应是 ndet、div 和 exn。
algebraic effects 的做法是，我们把副作用抽象为 操作符（operations） 和 处理器（handlers） 两部分。以最经典的一种 effect 也就是异常为例：
effect raise
ctl raise( msg : string ) : a
这定义了一个 effect 类型 raise 和一个 (msg : string) -> raise a 类型的 operation raise。声明 effect 的签名后，我们已经可以使用这些 operations 了：
fun safe-divide( x : int, y : int ) : raise int
if y==0 then raise("div-by-zero") else x / y
其中我们看到 safe-divide 函数获得了 raise 效应（因为我们在函数体内使用了 raise 操作符）。这样的效应类型意味着我们只能在处理 raise 的上下文中 evaluate 这个函数（换句话说，它是 “动态绑定”的，或者我们 “具有 raise 能力”） 的上下文。
我们可以通过为 raise 给出具体定义来处理这种效果。例如，我们可能总是返回一个默认值：
fun raise-const() : int
with handler
ctl raise(msg) 42 // 哦，宇宙的终极答案是 42
8 + safe-divide(1,0)
// 返回 42 而不是 50
调用 raise-const() 的计算结果为 42，不是 50。当调用 raise 时（在 safe-divide 中），它将 yield 于其最内层的 handler，展开堆栈，然后才 evaluate 操作符的定义 – 这个例子中，只是从定义 handler 的点直接返回 42。现在我们可以看到为什么它被称为 ctl operator （控制操作符），因为 raise 改变了常规的线性控制流，并从原始调用点直接 yield 到其最内层的处理程序。还要注意 raise-const 现在又是一个 total function 了，handler 抵消了 raise 的效果。
然后 Koka 的糖很有意思，比如
Koka allows anonymous functions to follow the function call instead – this is also known as trailing lambdas
fun hello-ten()
var i := 0
while { i < 10 }
println("hello")
i := i + 1
比如这个 while，它看上去很像一个语法，但其实是个函数 desugared to while( fn(){ i < 10 }, fn(){ ... } )
这样，许多的 control flow 都其实是一些用来当 control flow 的语法糖而已，能很好的允许你自定义语法
Idris
大体上看, Idris 这个语言的设计, 基本上是 Haskell 的延续, 整体上语法和 Haskell 十分接近, Haskell 程序员用起来基本上只会更爽, 不太会有什么不适 (除了不是默认 Lazy 这一点需要适应之外).
所以简而言之, Idris 就是带 Dependent Type 的 Haskell, 外加各种语法上的改良, 解决了诸多由 Haskell 所遗留的问题, 是 Haskeller 心目中的理想语言.
Dependent Type 允许你还有类型安全的带长度的 List（Vect n）。解答了我多年的疑问（）我们为什么不能干脆把长度视为一个泛型丢进 vector 里呢？ Idris 说行，当然行：
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
Vect 这个类型有了一个 Nat n 做参数，Idris2 基于量化类型理论实现了一个神奇的事情，如果你不用这个 n，它就能安全的在编译期被擦除，如果你用到它，它就会被保留。这里的 Nat 是一个 inductive type 可能实现成：
data Nat = Z -- Zero
| S Nat -- Successor
一进制自然数有一个非常方便的结构，容易推理，而且容易与其他数据结构联系起来，比如上面的 Vect，可以很好的推理。尽管如此，我们当然并不希望这种方便是以牺牲效率为代价的。但是！Idris 它能知道 Nat（和类似的结构化类型）和数字之间的关系。这意味着它可以优化表示，以及诸如 plus 和 mult 等函数。
有了 Vect 你就能容易写出常数时间的 len 函数（相反，List 需要遍历获取长度）
还有 Linear Type 这个东西。
Idris 2 是基于 量化类型理论（QTT） ，这是由 Bob Atkey 和 Conor McBride 开发的核心语言。在实践中，Idris 2 中的每个变量都有一个 数量 与之相关。数量是的取值是下列其中之一：
- 0 ，表示变量在运行时被 擦除
- 1 ，表示变量在运行时 正好使用一次
- 不受限制 ，这与 Idris 1 的行为相同
在 Idris 2 中你可以原生的用一些 Linear Type 的东西。这玩意核心思想大概是在结构性规则上去掉了收缩规则和弱化规则（参照： https://zhuanlan.zhihu.com/p/630206189）意味着 Linear 的 Type 只能使用，且必须使用一次。这种形式在一些东西上比较方便，比如说某种 resource，像 Connection 之类的，打开-关闭 总是成对出现
RAII 当然可以保证一次释放，但是当一个东西的“生命周期”比较动态、甚至可能交叉的时候，常见的 RAII 模式就没那么好用了。
Lean 4
如果你你想入函数式语言的坑我会推荐你别上来就学 Haskell，而是用 Lean 4。因为作为 pure functional 语言，Lean 4有 for 和 let mut 这些东西（内部似乎是靠 rebind 和/或 state monad 做到的），可以循序渐进地学习函数式的思想，Haskell 为了展现函数式的优美经常滥用 pointfree style（我愿称为 pointless style）装逼很好用但是如果你没被它腌入味了，根本就看不懂写的什么东西，完全不适合初学
作为一个编程语言兼定理证明器，你可能会在 Lean 4 里面看到很多的数学符号这是正常的不用害怕因为你写代码不太用得到它们，何况你都来写 Lean 4 了不顺便学点数学说不过去吧
Lean 4 的 std 是安装好的，所有类型都可以直接跑去看 std 的源码，享受 clangd/rust analyzer 级别的顶级 lsp 体验
好了懒得写了就说这么多（）