Idris语言站在了Haskell这个巨人之上，继承了Haskell的诸多优点，同时添加了一些新的特性。Idris 1的编译器使用Haskell语言编写，Idris 2对Idris 1进行了重写，引入了新的类型系统，基于QTT类型进行了优化。
这篇文章将介绍Idris 2的核心特性，主要跟通用编程相关的一些特性，包括纯函数式编程、依赖类型、交互式开发等，对后面的学习做个铺垫。
纯函数式编程
函数式编程是一种编程范式，强调使用纯函数，而不是改变状态的命令式编程。
传统的命令式编程，程序的执行就是一条条语句的执行，每条语句都可能会改变程序的状态，从而达到最终的结果状态，整个程序的执行过程就是一个状态机。
而在函数式编程中函数是第一等公民，函数可以作为参数传递，也可以作为返回值。程序可看作是函数的组合，执行过程就是这些函数的求值过程。如果使用无副作用的纯函数，避免使用命令式编程中的状态变量，这样就可以确保程序的可预测性和可维护性。
很多函数式编程语言，比如Elisp、Scheme等，都副作用留下了口子，如lisp系语言普遍都有setq函数来修改变量的值:
(setq x 10)
这的确给某些操作提供了方便，但也破坏了纯函数的一些性质，比如引用透明性。
引用透明性是指，对于一个纯函数而言，对于同样的输入会得到同样的输出。这样就可以使用输出来替换输入，而不会改变函数的行为。编译器可以利用这个性质，来优化程序的执行效率，如fibonacci函数。
fib n = fib (n – 1) + fib (n – 2)
在计算过程中，如果按照普通的递归方式计算，那么会重复计算很多子问题，导致效率低下。当我们得知了fib是个纯函数，我们就可以将fib n的值缓存下来，下次遇到fib x时，先查缓存，如果缓存中没有，再计算并缓存。这是应用代码能做的优化，同理，编译器也可以做类似的优化，如：公共子表达式消除（CSE）、记忆化（Memoization）等。
副作用
如果没有副作用，程序怎么跟真实的世界交互？读写文件、终端输入输出、网络通信等，通通都有副作用；如果没有副作用，我们的程序就是实验室里的花瓶，一点用处也没有。但引入副作用，又会使得函数不纯，在Haskell、Idris里是怎么解决这个矛盾的呢？
Haskell、Idris引入了IO类型，它*描述*一系列的IO操作序列。返回IO类型的函数，依然还是纯函数，因为它只描述了函数的行为，求值之后就会得到这一系列的操作，具体的执行交给语言的运行时。如，IO String表示一个IO操作序列，实际执行后会返回一个字符串。通过将求值（evaluation）和执行（execution）分开，保证函数的纯化。
针对上面的描述，举个简单的例子，帮助理解其区别。伪代码如下：
刷牙: IO ()
刷牙 = do
挤牙膏
上刷刷
下刷刷
左刷刷
右刷刷
漱口
之所以刷牙是个纯函数，是因为我们求值之后都能得到相同的操作序列，而不会改变程序的状态，这只是一个描述和计划，我们没有实际刷牙。而执行过程才是真正的按照这个过程刷牙，会改变程序的状态，我们的牙齿刷完了，变白了，漱口水少了。。。。
依赖类型
依赖类型是一类依赖于值的类型系统，其返回值类型可依据参数值动态变化。如：Vect Nat String，该列表类型把列表长度编码到类型里，这样Vect 2 String跟Vect 3 String就不是同一个类型了。
这是类型系统的强弱排名，可看出依赖类型处于最顶端，属于最强的一阶。
【弱】───────────────────────────────────────────────────────────────────────▶【强】
无类型 STLC System F Fω GADT 细化类型 完整依赖类型(CoC)
│ │ │ │ │ │ │
Python C/Go Rust/Java Haskell GADT LiquidHaskell Lean4/Idris2
JS
类型系统越强，表达能力越强，这样就可以更方便地描述程序的行为，让类型检查器帮我们静态检查程序的行为是否符合类型，从而避免运行时错误。我们考虑两个列表合并的例子，假设这两个列表里的元素类型是整型，我们第一版先用无类型的Scheme实现：
(define (vector-append-rec v1 v2)
(list->vector
(append (vector->list v1)
(vector->list v2))))
;; 测试
(vector-append-rec #(1 2) #("a" "b")) ; #(1 2 "a" "b")
因为Scheme是无类型的语言，所以对于我们的假设无能为力，无法在编译时检查类型，最终还是能编译通过。
我们再考虑C++，C++类型要比Scheme强，我们同样实现两个整型vector的合并函数append，代码为：
std::vector<int> append(std::vector<int> a, std::vector<int> b) {
a.insert(a.end(), b.begin(), b.end());
return a;
}
;; 测试
append({1, 2}, {"a", "b"}); // 编译报错
这一版编译报错，因为vector已经把元素类型的信息编码到了类型里，函数类型的参数为vector<int>，而传入的是vector<string>，类型不一致导致编译失败。
最后用支持依赖类型的Idris实现，进一步将列表的长度编码到类型里，代码为：
append :: Vect m a -> Vect n a -> Vect (m + n) a
append a b = …
因为实现比较复杂，这里就不展开了。需要关注的是，通过依赖类型描述了append函数需要满足的性质，即合并两个列表后，返回的列表长度是两个参数长度的和。如果函数实现过程中，返回的类型不满足这个性质，就会导致编译失败。随着类型系统的增强，可以在类型层面表达更多的函数性质，从而将错误拦截在编译阶段。
依赖类型给程序带来了更多的类型检查能力，帮助我们发现程序中的错误，避免运行时错误。
类型驱动开发
有了依赖类型，我们就能更精确地描述程序的行为，比如，上面提到的append函数，使得类型驱动开发成为可能。
类型驱动开发，是一种开发风格：用类型表达程序意图，先写下函数类型，留白函数定义，然后再逐步使用上下文信息填充函数定义，涉及到的函数类型可能需要多次精化（refine）。Idris推崇这种风格的开发方式，提供了很多语言和工具上的支持。
Hole（类型洞）
Hole是类型驱动开发的核心机制。在编写函数时，可以用?name作为占位符，表示"这里我还不知道怎么写，但我知道它应该是什么类型"。编译器会告诉我们这个hole的上下文——包括当前作用域中的变量及其类型，以及hole的目标类型。这就像一个交互式对话：你先告诉编译器你想要什么类型，编译器反过来告诉你当前有哪些"材料"可用。
append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = ?body
当我们查看body的类型时，会返回：
Main> :t body
0 m : Nat
0 a : Type
0 n : Nat
ys : Vect m a
xs : Vect n a
——————————
body : Vect (plus n m) a
横线上方是当前可用的变量及其类型（上下文），下方是需要填充的目标类型。有了这些信息，开发者就可以根据上下文逐步构造出正确的实现。
交互式编辑命令
Idris的REPL（交互式解释器）提供了一系列交互式命令，让类型驱动开发如虎添翼, 例如：
- :t :type – 查看表达式的类型。
- :cs :casesplit – 对某个变量进行模式匹配，自动生成所有情况的分支。
- :ps :proofsearch – 让编译器自动尝试搜索满足当前hole类型的表达式。
- :ml :makemalemma – 当一个hole的类型过于复杂时，可以将它提取为一个辅助引理（lemma），单独证明。
- :ac :addclause – 添加一个子句到当前hole的证明中。
- …
直接用上面的命令，稍微有点麻烦。一些编辑器通过插件（如Vim、Emacs的idris-mode）提供了更友好的交互，我们能用快捷键、鼠标等操作来完成类型驱动开发。
