IDRIS：一种用于类型驱动开发的语言

在类型驱动开发中，类型是构造程序的工具。我们将类型作为程序的计划，并使用编译器和类型检查器作为我们的助手，引导我们找到满足该类型的完整程序。越有表现力的类型是我们放弃前面，我们就越有信心，结果程序将是正确的。

在Idris中，类型是语言中的一级构造。这意味着类型可以作为参数传递给函数，并且可以像任何其他值一样从函数返回，例如数字、字符串或列表。这是一个小而有力的想法，使：

要由编译器明确和检查的假设。例如，如果你假设一个列表是非空的，那么Idris可以确保在程序运行之前这个假设总是成立的。

在freenode上还有一个IRC频道#idris，将您的IRC客户端指向chat.freenode.net，然后/join#idris.或者，还有一个Web界面。

Idris源代码可以从我们的存储库中获得，更广泛的Idris社区的工具和代码可以在GitHub组织中获得。

圣安德鲁斯大学计算机科学学院的埃德温·布雷迪领导了Idris的开发。

我们也感谢SICSA(苏格兰信息学和计算机科学联盟)的持续支持