引言¶
在传统编程语言中，类型 与 值 之间有明确的区分。例如在 Haskell 中, 下面这些类型分别表示整数、字符、字符列表 以及任意值的列表：
Int,Char,[Char],[a]
与此对应，下面这些值分别为上述类型的成员：
42,’a’,"Hello world!",[2,3,4,5,6]
然而，在带有 依赖类型（Dependent Type） 的语言中，它们的区别并不明显。
依赖类型允许类型「依赖」于值，换句话说，类型是 一等（First-Class） 的语言构造，
即它可以像值一样进行操作。标准范例就是带长度的列表类型 [1] Vect n a，
其中 a 为元素的类型，而 n 为该列表的长度且可以任意长。
当类型包含了描述其性质的值（如列表的长度）时，它就能描述函数自身的性质了。
比如连接两个列表的操作，它拥有性质：结果列表的长度为两个输入列表的长度之和。
因此我们可以为 app 函数赋予如下类型，它用于连接向量（Vector）：
app : Vect n a -> Vect m a -> Vect (n + m) a
本教程介绍了 Idris，一个通用的依赖类型函数式编程语言。Idris
项目旨在为可验证的通用编程打造一个依赖类型的语言。
为此，Idris 被设计成了编译型语言，目的在于生成高效的可执行代码。
它还拥有轻量的外部函数接口，可与外部 C 库轻松交互。
目标受众¶
本教程面向已经熟悉函数式语言（如 Haskell 或 OCaml ）的读者，旨在简要地介绍该语言。 尽管大多数概念都会有简单的解释，读者仍须熟悉 Haskell 的语法。 我们亦假设读者有兴趣使用依赖类型来编写和验证系统软件。
对 Idris 更加深入的介绍，见 Edwin Brady 所著的《 Idris 类型驱动开发 》， 其进度要慢得多，涵盖了交互式程序开发以及更多的例子。本书可从 Manning 获取。