簡(jiǎn)介
- Emacs集成 Idris 開發(fā)環(huán)境
- Idris repl 使用說明
- Idris 代數(shù)類型定義
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*中加載當(dāng)前文件并啟用 type check 進(jìn)行檢查充石，出現(xiàn)的錯(cuò)誤會(huì)打印在*idris-notes* buffer中寡键。
注意
關(guān)于 IO 的調(diào)用問題，經(jīng)典 Hello World 程序：
module Main
main : IO ()
main = putStrLn "Hello World"
當(dāng)需要在repl中調(diào)用 main 方法時(shí)，需要通過:x main 執(zhí)行，才能看到執(zhí)行結(jié)果，Hello World 會(huì)顯示在*idris-process* buffer 中亭引。原因是 repl 會(huì)返回一個(gè) IO action，這個(gè) IO action 只會(huì)在 idris 之外 hook 的 terminal 中才會(huì)執(zhí)行皮获。https://github.com/idris-lang/Idris-dev/issues/3152
:x <expr> Execute IO actions resulting from an expression using the interpreter
2. 自定義數(shù)據(jù)類型
我們先定義一下自然數(shù)：自然數(shù)就是從0開始焙蚓，后面的數(shù)都比前一個(gè)自然數(shù)多1的數(shù)列。我們從小知道的自然數(shù)0, 1, 2,...,100,... 看上去只是一系列割裂開的一組符號(hào)洒宝，但是事實(shí)上购公，數(shù)列本身必然存在一些屬性，數(shù)與數(shù)之間必然存在規(guī)律雁歌。
基于前面提到的自然數(shù)的屬性宏浩，我們定義自然數(shù)如下
data Natural = Z | S Natural
讀作：自然數(shù)要么是Z（零），要么是自然數(shù)的后繼(S)
2.1 定義加法
接下來靠瞎，我們定義自然數(shù)的加法運(yùn)算
plus : Natural -> Natural -> Natural
plus Z m = m -- 模式1
plus (S n) m = S (plus n m) -- 模式2
首先定義出了 plus 函數(shù)的類型比庄，它是接收兩個(gè)自然數(shù)，然后返回一個(gè)自然數(shù)的函數(shù)乏盐，這里使用了柯里化的表現(xiàn)方式佳窑。
plus Z m = m 表示任何自然數(shù)加上零，都得自然數(shù)本身丑勤；
plus (S n) m = S (plus n m) 表示任何兩個(gè)自然數(shù)相加华嘹，都等于其中一個(gè)自然數(shù)的前趨和另一個(gè)自然相加結(jié)果的后繼。這句話說起來比較繞法竞，但是只要展開之后就比較容易理解了。
考察1 + 1 = 2强挫，可以表達(dá)如下：
(S Z) # 1 是 0 的后繼
plus (S Z) (S Z) -- 1 + 1
S (plus Z (S Z)) -- 根據(jù)模式2展開上面的式子
(S (S Z)) -- 根據(jù)模式1展開上面的式子
(S (S Z)) 就是自然數(shù)2
2.2 定義乘法
mult : Natural -> Natural -> Natural
mult Z m = Z
mult (S n) m = plus m (mult n m)
mult Z m = Z表示任何自然數(shù)乘以零岔霸，都得零；
mult (S n) m = plus m (mult n m)表示任何兩個(gè)自然數(shù)相乘俯渤，都等于其中一個(gè)自然數(shù)和另一個(gè)自然數(shù)的前趨相乘的結(jié)果呆细，加上它自身。
學(xué)習(xí)資料
[1] Idris mode
[2] Learn idris
[3] Idris docs
