Remove ads
Idris是一個通用的依賴類型純函數式程式語言，其類型系統與Agda以及Epigram相似。
Idris語言具備堪與Coq媲美的交互式定理證明能力，自帶tactics，而其設計目標側重於通用系統編程更甚於輔助證明。Idris的其他設計目標還包括「可觀的」代碼性能，對副作用的控制，以及對於實現嵌入式領域特定語言（Embedded Domain Specific Language，EDSL）的支持。
Idris通過一個依賴類型的核心語言TT生成C語言的中間代碼並編譯到本地機器碼，並利用了一個基於Cheney算法的垃圾收集器實現。Idris亦擁有 JavaScript、Java和LLVM的編譯器後端。[4]
Idris 支持對依賴類型（）的定義。如下定義了，即元素類型 的 -元組類型：
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)
Remove ads
Idris 對嵌入式領域特定語言的支持主要包括以下方面[6]：
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 Num。注意在這裏，該函數被認為是完整的（total），儘管並未定義一個參數是 Nil 而另一個參數非 Nil 的模式。原因在於兩個作為參數的 vector 只能具備相同的長度，這一點通過依賴類型系統得到了保證，因此在編譯時兩者長度不同的情形絕無可能發生。這使得該函數定義仍然是完整的。
Remove ads
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;
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
Remove ads