简介
- Emacs集成 Idris 开发环境
- Idris repl 使用说明
- Idris 代数类型定义
1. Emacs 安装 idris-mode
(use-package idris-mode
:mode (("\\.idr$" . idris-mode)
("\\.lidr$" . idris-mode))
:ensure t
:defer t)
(provide 'init-idris)
emacs 打开任何以*.idr和*.lidr作为后缀的文件，都可以启用idris-mode.
另外，使用C-c C-l可以在*idris-repl*中加载当前文件并启用 type check 进行检查，出现的错误会打印在*idris-notes* buffer中。
注意
关于 IO 的调用问题，经典 Hello World 程序：
module Main
main : IO ()
main = putStrLn "Hello World"
当需要在repl中调用 main 方法时，需要通过:x main 执行，才能看到执行结果，Hello World 会显示在*idris-process* buffer 中。原因是 repl 会返回一个 IO action，这个 IO action 只会在 idris 之外 hook 的 terminal 中才会执行。https://github.com/idris-lang/Idris-dev/issues/3152
:x <expr> Execute IO actions resulting from an expression using the interpreter
2. 自定义数据类型
我们先定义一下自然数：自然数就是从0开始，后面的数都比前一个自然数多1的数列。我们从小知道的自然数0, 1, 2,...,100,... 看上去只是一系列割裂开的一组符号，但是事实上，数列本身必然存在一些属性，数与数之间必然存在规律。
基于前面提到的自然数的属性，我们定义自然数如下
data Natural = Z | S Natural
读作：自然数要么是Z（零），要么是自然数的后继(S)
2.1 定义加法
接下来，我们定义自然数的加法运算
plus : Natural -> Natural -> Natural
plus Z m = m -- 模式1
plus (S n) m = S (plus n m) -- 模式2
首先定义出了 plus 函数的类型，它是接收两个自然数，然后返回一个自然数的函数，这里使用了柯里化的表现方式。
plus Z m = m 表示任何自然数加上零，都得自然数本身；
plus (S n) m = S (plus n m) 表示任何两个自然数相加，都等于其中一个自然数的前趋和另一个自然相加结果的后继。这句话说起来比较绕，但是只要展开之后就比较容易理解了。
考察1 + 1 = 2，可以表达如下：
(S Z) # 1 是 0 的后继
plus (S Z) (S Z) -- 1 + 1
S (plus Z (S Z)) -- 根据模式2展开上面的式子
(S (S Z)) -- 根据模式1展开上面的式子
(S (S Z)) 就是自然数2
2.2 定义乘法
mult : Natural -> Natural -> Natural
mult Z m = Z
mult (S n) m = plus m (mult n m)
mult Z m = Z表示任何自然数乘以零，都得零；
mult (S n) m = plus m (mult n m)表示任何两个自然数相乘，都等于其中一个自然数和另一个自然数的前趋相乘的结果，加上它自身。
学习资料
[1] Idris mode
[2] Learn idris
[3] Idris docs
