Idris
Idris
關於 Idris練習

想學習並精通 Idris 嗎？

加入 Exercism 的 Idris 學習軌道，即可獲得 58 個練習 並享有程式碼自動分析 以及 個人導師引導， 全部100% 免費。

加入 Idris 學習軌道 探索練習

關於 Idris

module EvenOdd

data Even : Nat -> Type where
  EZ : Even Z
  ES : Even n -> Even (S (S n))

ee : Even n -> Even m -> Even (n + m)
ee EZ m     = m
ee (ES n) m = ES (ee n m)

在 Exercism 上，Idris 共有58 個程式設計練習。 從 All Your Base 到 考拉茲猜想。

透過 Exercism 上有趣又有成就感的程式設計練習，測試你對各種概念的理解，讓你的程式設計能力更上一層樓。

All Your Base

All Your Base

將以某個進位的一串數字所表示的數，轉換成任意其他進位。

祕密握手

祕密握手

給定一個十進位數字，將它轉換成祕密握手對應的事件序列。

考拉茲猜想

考拉茲猜想

利用考拉茲猜想，計算抵達 1 所需的步數。

查看 Exercism 上所有 Idris 練習

Idris 的核心功能

Idris

依值型別

安全第一！在編譯期就為程式的正確性提供強而有力的保證。

純函式

靈感來自 lambda 演算，作用域與迴圈都是透過定義和呼叫函式來表達。

型別類別

將型別分類成類別，就能提供型別安全的多載。

多執行緒

資料不可變，讓並行更安全、也更容易推理。

輕巧

Idris 只提供少量的通用功能。

創新

Idris 是一個積極開發中的研究測試平台

以 Idris 的方式獲得引導

每種語言都有自己做事的方式。Idris 也不例外。我們的導師會幫助你學會像 Idris 開發者那樣思考，以及如何寫出 道地的 Idris 程式碼。解完一個練習後，把它提交給我們的 志工團隊，他們會給你提示、想法和回饋，告訴你 怎麼寫得更像你在 Idris 中平常會看到的樣子。他們也會幫助你發現那些 你不知道自己不知道的事。

進一步了解引導

由社群提供的 Idris 練習

Exercism 上的 Idris 學習軌道有 58 個練習，幫助你寫出更好的程式碼。

查看所有 Idris 練習
Idris

開始使用 Idris 學習軌道

最棒的是，它對所有人 100% 免費。

加入 Idris 學習軌道