介绍
在传统的编程语言中，类型 和 值 之间有明显的区别。例如，在 Haskell ，以下是类型，分别代表整数、字符、字符列表和任意值的列表：
Int,Char,[Char],[a]
相应地，以下值是这些类型的成员的示例：
42,’a’,"Hello world!",[2,3,4,5,6]
然而，在具有*依值类型*的语言中，它们的区别不太明显。依值类型允许类型“依赖”值——换句话说，类型是*一等*语言结构，可以像任何其他值一样被操作。标准示例是给定长度的列表类型 [1]， Vect n a ，其中 a 是元素类型， n 是列表的长度，且可以任意长。
当类型可以包含值，并且这些值描述属性时，例如一个列表的长度，函数的类型就可以开始描述它自己的属性。以两个列表的连接为例。这个操作的属性是：结果列表的长度是两个输入列表的长度之和。因此，我们可以给 app 函数提供以下类型，它用于连接向量：
app : Vect n a -> Vect m a -> Vect (n + m) a
本教程介绍了Idris，一种具有依值类型的通用函数式编程语言。Idris 项目的目标是建立一个适用于可验证的通用编程的依值类型语言。为此，Idris 被设计为一种编译语言，旨在生成高效的可执行代码。同时它还有一个轻量级的外部函数接口，允许与外部库轻松互动。
目标受众
本教程旨在作为该语言的简要介绍，并针对已经熟悉函数式语言的读者，如 Haskell 或 OCaml 。特别是假设对 Haskell 语法有一定程度的熟悉，尽管大多数概念至少会被简单地解释。同时还假设读者对使用依值类型来编写和验证软件有一定的兴趣。
关于Idris的更深入的介绍，它以更慢的速度进行，涵盖了交互式程序开发，也有更多的示例，见 Type-Driven Development with Idris ，作者 Edwin Brady ，本书可从 Manning 获取。
示例代码
本教程包括一些示例代码，这些代码已经针对Idris 2进行了测试。这些文件与Idris 2发行版一起提供，所以你可以很容易地使用它们。它们可以在 samples 目录下找到。然而，强烈建议你自己输入它们，而不是简单地加载然后阅读。
脚注