代数定义- idris

发表于 更新于 分类于

关于环境和数据类型

简介

  1. Emacs集成 Idris 开发环境
  2. Idris repl 使用说明
  3. Idris 代数类型定义

1. Emacs 安装 idris-mode

1
2
3
4
5
6
7
(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 程序：

1
2
3
4
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

1
:x  <expr>  Execute IO actions resulting from an expression using the interpreter

2. 自定义数据类型

我们先定义一下自然数：自然数就是从0开始，后面的数都比前一个自然数多1的数列。我们从小知道的自然数0, 1, 2,…,100,… 看上去只是一系列割裂开的一组符号，但是事实上，数列本身必然存在一些属性，数与数之间必然存在规律。

基于前面提到的自然数的属性，我们定义自然数如下

1
data Natural = Z | S Natural

读作：自然数要么是Z（零），要么是自然数的后继(S)

2.1 定义加法

接下来，我们定义自然数的加法运算

1
2
3
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，可以表达如下：

1
2
3
4
(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 定义乘法

1
2
3
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