Idris

Idris

編程範型	函數式編程
設計者	Edwin Brady
面市時間	2007年，​17年前​（2007）[1]
當前版本	1.3.3（2020年5月23日）[2]
型態系統	靜態類型, 強類型, 依賴類型
操作系統	跨平台
許可證	BSD-3
文件擴展名	.idr, .lidr
網站	Idris
啟發語言
Agda, Coq, Epigram（英語：Epigram (programming language)）, Haskell, ML

Idris是一個通用的依賴類型純函數式編程語言，其類型系統與Agda以及Epigram（英語：Epigram (programming language)）相似。

Idris語言具備堪與Coq媲美的交互式定理證明能力，自帶tactics，而其設計目標側重於通用系統編程更甚於輔助證明。Idris的其他設計目標還包括「可觀的」代碼性能，對副作用的控制，以及對於實現嵌入式領域特定語言（Embedded Domain Specific Language，EDSL）的支持。

Idris通過一個依賴類型的核心語言TT生成C語言的中間代碼並編譯到本地機器碼，並利用了一個基於Cheney算法的垃圾收集器實現。Idris亦擁有 JavaScript、Java和LLVM的編譯器後端。^[4]

Idris的名字來自於20世紀70年代的英國兒童動畫片《火車頭艾弗（英語：Ivor_the_Engine#Idris_the_Dragon）》裡，一條會唱歌的龍。^[5]

Idris 支持對依賴類型（${\displaystyle \lambda \Pi }$）的定義。如下定義了${\displaystyle {\mbox{Vec}}(a,n)}$，即元素類型 ${\displaystyle a}$ 的 ${\displaystyle n}$-元組類型：

data Nat = O | S Nat
infixr 5 ::

data Vect : Type -> Nat -> Type where
    VNil : Vect a O
  | (::) : a -> Vect a k -> Vect a (S k)

Idris 對嵌入式領域特定語言的支持主要包括以下方面^[6]：

1. 編譯期間求值。
2. 可重載的語法。
3. 與C語言庫的接口，以及高效的代碼生成。

Idris 擁有與 F# 相似的類型提供器，它允許編譯器在編譯期間根據所執行代碼的需求而生成新的類型信息。這使得靜態類型系統更具可擴展性。^[7]

Idris 的語法與 Haskell 有許多相似之處。一個最簡單的 Hello World 程序如下：

module Main

main : IO ()
main = putStrLn "Hello, World!"

該程序與 Haskell 的等效寫法僅有兩點不同：類型簽名使用單個冒號「:」而不是雙冒號「::」；開頭的模塊聲明中不必使用 where 從句。

Idris 亦支持 where 從句、let 表達式、with 規則、簡單的 case 表達式和模式匹配等。

一個在 Idris 中使用依賴類型的示例：

total
append : Vect n a -> Vect m a -> Vect (n + m) a
append Nil       ys = ys
append (x :: xs) ys = x :: append xs ys

該函數將一個包含 m 個類型 a 的元素的 vector 連接到一個包含 n 個類型 a 的元素的 vector 之後。由於輸入 vector 的確切類型依賴於它的值，故在編譯（類型檢查）時即可保證輸出的 vector 必將包含 (n + m) 個類型 a 的元素。

關鍵字「total」將會執行函數的完整性（totality）檢查。若函數定義未涵蓋所有可能的情形（partial function），則檢查器會報錯。

另一個使用依賴類型的示例：

total
pairAdd : Num a => Vect n a -> Vect n a -> Vect n a
pairAdd Nil       Nil       = Nil
pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys

Num a 標誌着類型 a 屬於 Type class（英語：Type class） Num。注意在這裡，該函數被認為是完整的（total），儘管並未定義一個參數是 Nil 而另一個參數非 Nil 的模式。原因在於兩個作為參數的 vector 只能具備相同的長度，這一點通過依賴類型系統得到了保證，因此在編譯時兩者長度不同的情形絕無可能發生。這使得該函數定義仍然是完整的。

Idris 默認採取及早求值（Eager evaluation），而非 Haskell 的惰性求值（Lazy evaluation）方式。Idris 支持使用 Lazy 關鍵字顯式地指定惰性求值：

data Lazy : Type -> Type where
  Delay : (val : a) -> Lazy a

Force : Lazy a -> a

boolCase : Bool -> Lazy a -> Lazy a -> a;
boolCase True t e = t;
boolCase False t e = e;

• The Idris homepage（頁面存檔備份，存於網際網路檔案館）, including documentation, frequently asked questions and examples
• Idris at the Hackage repository（頁面存檔備份，存於網際網路檔案館）
• Idris Tutorial