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)

58 个编程练习，尽在 Exercism 的 Idris。 从 背包问题 到 匹配括号。

借助有趣又有收获的编程练习提升编程水平，在 Exercism 上检验你对概念的理解。

背包问题

背包问题

给定一个只能承载一定重量的背包，确定要往背包里放哪些物品，才能使它们的总价值最大。

倍数之和

倍数之和

给定一个数字，求出指定各数字的所有倍数之和，且这些倍数都小于该数字。

匹配括号

匹配括号

确保括号和大括号都能正确匹配。

查看 Exercism 上所有 Idris 练习

Idris 的主要功能

Idris

依赖类型

安全第一！在编译期对程序的正确性提供强有力的保证。

纯函数式

受 λ 演算启发，作用域和循环都靠定义和调用函数来表达。

类型类

把类型归类成类型类，就能实现类型安全的重载。

多线程

数据不可变，并发因此更安全，也更容易推理。

精简

Idris 只提供少量通用功能。

创新

Idris 是一个活跃开发中的研究试验平台

以 Idris 的方式接受指导

每种语言都有自己的做事方式，Idris 也不例外。我们的导师会帮助你学会像 Idris 开发者那样思考，并教你如何写出地道的 Idris 代码。解完一道练习后，把它提交给我们由志愿者组成的团队，他们会给你提示、想法和反馈，帮你写出更接近 Idris 中常见风格的代码，还会帮你发现那些你并不知道自己不知道的东西。

了解更多关于指导的内容

由社区贡献的 Idris 练习

Exercism 上的 Idris 轨道有 58 个练习，帮你写出更好的代码。

查看 Idris 的全部练习
Idris

开始学习 Idris 轨道

最棒的是，它对所有人 100% 免费。

加入 Idris 轨道