據Idris開發團隊披露，基于依賴類型的Idris語言即將完成0.99版本，該版本可被看成是1.0版的Alpha版本。Idris 1.0版有望于2017年2月左右發布。

\\

Idris是一種純函數式編程語言，目標在于注重語言通用性及滿足系統編程所需效率的同時，讓更多的編程人員使用基于類型的程序驗證技術。

\\

Idris的主要理念是依賴類型。正如函數表述了值之間依賴性，依賴類型旨在表示類型與值之間的依賴性。舉個例子，我們可以定義一類返回值為一個列表的函數，要求列表中的元素值依次遞減，只有滿足了該屬性，才會去編譯該函數所采用的任何具體實現。對于可被Idris所表示的軟件屬性，其它的例子還包括數組范圍驗證以及分布式或并發系統中的協議正確性，譬如確保所有程序遵循特定的協議訪問文件句柄。下面所示的代碼段使用Idris定義了Vect向量的依賴類型，并向vapp函數中添加了兩個向量：

\\\infixr 5 ::;\data Vect : Set -\u0026gt; Nat -\u0026gt; Set where\ VNil : Vect a O\ | (::) : a -\u0026gt; Vect a k -\u0026gt; Vect a (S k);\vapp : (Vect A n) -\u0026gt; (Vect A m) -\u0026gt; (Vect A (plus n m));\vapp VNil ys = ys;\vapp (x :: xs) ys = x :: vapp xs ys;\\\

編譯器可以檢測到上面代碼段中所涉及類型的誤用。例如，下面的vapp的實現就破壞了依賴性：

\\\vapp : Vect a n -\u0026gt; Vect a m -\u0026gt; Vect a (plus n m);\vapp VNil ys = ys;\vapp (x :: xs) ys = x :: vapp xs xs; -- BROKEN\\\

據Idris核心開發人員介紹，決定發布1.0版的主要原因是該語言正步入穩定。這并不意味著Idris已“可用于生產環境”，因為開發團隊還不可能做到提供長期支持或是保證實現的質量。即使如此，作為一種探究如何使用依賴類型編程的研究工具而言，Idris還是頗具價值的。

\\

與Coq類似，Idris也支持交互定理證明，其中包括了反向推理，但是在用于定理證明之前，Idris意在首先成為一種通用的編程語言。Idris程序將被編譯為C語言，其內存管理依賴于并使用了垃圾回收機制。

\\

查看英文原文： Idris Getting Close to Version 1.0

\\

---

感謝冬雨對本文的審校。

\

給InfoQ中文站投稿或者參與內容翻譯工作，請郵件至editors@cn.infoq.com。也歡迎大家通過新浪微博（@InfoQ，@丁曉昀），微信（微信號：InfoQChina）關注我們。

總結

以上是生活随笔為你收集整理的Idris趋近发布1.0版的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。