类型和函数
原语类型
Idris 定义了几个原语类型。 Int , Integer 和 Double 用于数字操作， Char 和 String 用于文本操作，以及 Ptr 表示外来指针。库中还声明了几种数据类型，包括 Bool ，其值为 True 和 False 。我们可以用这些类型声明一 些常量。在文件 Prims.idr 中输入以下内容，并通过输入 idris2 Prims.idr 将其加载到 Idris 交互环境中：
module Prims
x : Int
x = 94
foo : String
foo = "Sausage machine"
bar : Char
bar = 'Z'
quux : Bool
quux = False
一个 Idris 文件由一个可选的模块声明（这里是 module Prims ）组成，后面是可选的导入列表和声明与定义的集合。在这个例子中没有指定导入。然而 Idris 程序可以由几个模块组成，每个模块的定义都有自己的命名空间。这将在 模块和命名空间 部分进一步讨论。当编写 Idris 程序时，定义的顺序和缩进都很重要。函数和数据类型必须在使用前定义，顺便说一下，每个定义都必须有一个类型声明，例如上面列表中的 x : Int , foo : String ,。新的声明必须从与前一个声明相同的缩进层次开始。或者用分号 ; 来终止声明。
库模块 prelude 会被每个 Idris 程序自动导入，包括 IO 、算术、数据结构和各种常用函数的设施。preclude 模块定义了几个算术和比较运算符，我们可以在提示符下使用。在提示符下对事物进行求值会得到一个答案，例如：
Prims> 13+9*9
94 : Integer
Prims> x == 9*9+13
True
所有常见的算术和比较运算符都是被定义为原语类型的。它们通过接口被重载，我们将在 接口 一节中讨论，并且可以被扩展到用户定义的类型上工作。例如，布尔表达式可以用 if...then...else 构建来测试：
*prims> if x == 8 * 8 + 30 then "Yes!" else "No!"
"Yes!"
数据类型
数据类型的声明方式和语法与 Haskell 类似。例如，自然数和列表可以被声明如下：
data Nat = Z | S Nat -- Natural numbers
-- (zero and successor)
data List a = Nil | (::) a (List a) -- Polymorphic lists
数据类型名称不能以小写字母开头（我们将在后面看到为什么不可以！）。 上面的声明来自标准库。一进制自然数可以是零 (Z)，也可以是另一个自然数的后继者 (S k)。列表可以是空的 (Nil )，也可以是添加到另一个列表前面的值 (x :: xs )。在 List 的声明中，我们使用了一个 infix 运算符 :: 。像这样的新运算符可以使用缀序声明来添加，如下所示：
infixr 10 ::
函数、数据构造器和类型构造器都可以被赋予 infix 运算符作为名称。它们可以以前缀的形式使用，如果用括号括起来，例如： (::) 。中缀运算符可以使用任何符号：
:+-*\/=.?|&><!@$%^~#
一些由这些符号构建的运算符不能被用户定义。这些是
%, \, :, =, |, |||, <-, ->, =>, ?,
!, &, **, ..
函数
函数是通过模式匹配实现的，同样使用与 Haskell 类似的语法。主要的区别是 Idris 要求所有函数的类型声明使用单冒号 : (而不是Haskell的双冒号 :: ）。一些自然数算术函数可以定义如下，同样取自标准库：
-- Unary addition
plus : Nat -> Nat -> Nat
plus Z y = y
plus (S k) y = S (plus k y)
-- Unary multiplication
mult : Nat -> Nat -> Nat
mult Z y = Z
mult (S k) y = plus y (mult k y)
标准的算术运算符 + 和 * 也被重载，供 Nat 使用，并用上述函数实现。与 Haskell 不同，对函数名是否必须以大写字母开头没有任何限制。函数名 (上面的 plus 和 mult )、数据构造函数 ( Z, S, Nil 和 ::) 和类型构造函数 ( Nat 和 List) 都属于同一个命名空间。然而，根据惯例，数据类型和构造函数名称通常以大写字母开头。我们可以在 Idris 提示下测试这些函数：
Main> plus (S (S Z)) (S (S Z))
4
Main> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
12
和算术运算一样，整数字面量也是使用接口重载的，这意味着我们也可以按如下方式测试函数：
Idris> plus 2 2
4
Idris> mult 3 (plus 2 2)
12
顺便说一下，你可能会想知道，既然我们的计算机已经内置了完美的整数运算，为什么我们还有一进制自然数。原因主要是一进制自然数有一个非常方便的结构，容易推理，而且容易与其他数据结构联系起来，我们将在后面看到。尽管如此，我们并不希望这种方便是以牺牲效率为代价的。幸运的是， Idris 知道 Nat （和类似的结构化类型）和数字之间的关系。这意味着它可以优化表示，以及诸如 plus 和 mult 等函数。
where 从句
也可以使用 where 从句在 局部 定义函数。例如，为了定义一个反转列表的函数，我们可以使用一个辅助函数来累积新的反转后的列表，而这个函数不需要全局可见：
reverse : List a -> List a
reverse xs = revAcc [] xs where
revAcc : List a -> List a -> List a
revAcc acc [] = acc
revAcc acc (x :: xs) = revAcc (x :: acc) xs
缩进是很重要的 -- where 块中的函数必须比外部函数有更深的缩进层次。
备注
作用域
任何在外层作用域中可见的名字在 where 从句中也是可见的（除非它们被重新定义，例如这里的 xs ）。在类型声明中出现的名字也将在 where 从句的作用域内。
除了函数， where 块也可以包括局部数据类型声明，比如下面的 MyLT 在 foo 的定义之外不能访问：
foo : Int -> Int
foo x = case isLT of
Yes => x*2
No => x*4
where
data MyLT = Yes | No
isLT : MyLT
isLT = if x < 20 then Yes else No
在 where 从句中定义的函数需要一个类型声明，就像任何顶层函数一样。下面是另一个例子，说明这在实践中是如何工作的：
even : Nat -> Bool
even Z = True
even (S k) = odd k where
odd : Nat -> Bool
odd Z = False
odd (S k) = even k
test : List Nat
test = [c (S 1), c Z, d (S Z)]
where c : Nat -> Nat
c x = 42 + x
d : Nat -> Nat
d y = c (y + 1 + z y)
where z : Nat -> Nat
z w = y + w
完全性和覆盖性
默认情况下，Idris 的函数必须是 covering 。也就是说，必须有涵盖输入类型的所有可能值的模式。例如，下面的定义将给出一个错误：
fromMaybe : Maybe a -> a
fromMaybe (Just x) = x
这给出了一个错误，因为 fromMaybe Nothing 没有定义。Idris会输出报告：
frommaybe.idr:1:1--2:1:fromMaybe is not covering. Missing cases:
fromMaybe Nothing
你可以用 partial 注解来忽略这一警告。
partial fromMaybe : Maybe a -> a
fromMaybe (Just x) = x
然而，这并不可取，一般来说，你只应该在函数的初始开发过程中，或者在调试过程中这样做。 如果你试图在运行时对 fromMaybe Nothing 进行求值，你将得到一个运行时错误。
孔
Idris programs can contain holes which stand for incomplete parts of programs. For example, we could leave a hole for the greeting in our "Hello world" program:
main : IO ()
main = putStrLn ?greeting
语法 ?greeting 引入了一个孔，它代表程序中尚未编写的一部分。这是一个有效的I dris 程序，你可以检查 greeting 的类型：
Main> :t greeting
-------------------------------------
greeting : String
检查一个孔的类型也会显示作用域内任何变量的类型。例如，给定一个不完整的定义 even ：
even : Nat -> Bool
even Z = True
even (S k) = ?even_rhs
我们可以检查 even_rhs 的类型，看到预期的返回类型，以及变量 k 的类型：
Main> :t even_rhs
k : Nat
-------------------------------------
even_rhs : Bool
孔的用途在于可以帮助我们 渐进的 写函数。与其一次写完整个函数，我们可以留下一些部分不写，Idris 会告诉我们完还需要完成哪些内容。
依值类型
一等类型
在 Idris 中，类型是一类公民，意味着它们可以像其他语言结构一样被计算和操作（并传递给函数）。例如，我们可以写一个函数来计算一个类型：
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat
这个函数从一个 Bool 值计算出适当的类型，这个 Bool 值表示是否是一个单例。我们可以在任何可以使用类型的地方使用这个函数来计算一个类型。例如，它可以被用来计算一个返回类型：
mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []
或者它可以用在输入类型上。以下函数计算 Nat 列表的总和，或返回给定的 Nat ，具体取决于单例标志是否为真：
sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum False (x :: xs) = x + sum False xs
向量
依赖数据类型的一个标准例子是 "有长度的列表" 类型，在依值类型文献中习惯上称为向量。它们作为 Idris 库的一部分，可以通过 Data.Vect 导入，或者我们可以像这样声明它们：
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
注意，我们使用了与 List 相同的构造函数名称。Idris 接受这样的临时名称重载，只要这些名称是在不同的命名空间（在实践中，通常是在不同的模块中）声明的。有歧义的构造函数名称通常可以通过不同的上下文来解决。
这声明了一个类型族，因此声明的形式与上面的简单类型声明相当不同。我们明确说明类型构造函数 Vect 的类型 -- 它接受一个 Nat 和一个类型作为参数，其中 Type 代表类型的类型。我们说 Vect 是在 Nat 上建立 索引 的 ，并且通过 Type 参数化 。每个构造函数针对类型族的不同部分。 Nil 只能用来构造零长度的向量，而 :: 用来构造非零长度的向量。在 :: 的类型中，我们明确指出，一个类型为 a 的元素和一个类型为 Vect k a 的尾部（即一个长度为 k 的向量）组合成一个长度为 S k 的向量。
我们可以通过模式匹配的方式，在 Vect 这样的依值类型上定义函数，就像在上面 List 和 Nat 这样的简单类型上一样。 Vect 上的函数的类型将描述涉及到的向量的长度会发生什么。例如，下面定义的 ++ 用于链接两个 Vect ：
(++) : Vect n a -> Vect m a -> Vect (n + m) a
(++) Nil ys = ys
(++) (x :: xs) ys = x :: xs ++ ys
(++) 的类型指出，结果向量的长度将是输入长度的总和。如果我们把定义弄错了，使之不成立，Idris 将不接受这个定义。例如：
(++) : Vect n a -> Vect m a -> Vect (n + m) a
(++) Nil ys = ys
(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
当通过 Idris 类型检查器运行时，这将导致以下结果：
$ idris2 Vect.idr --check
1/1: Building Vect (Vect.idr)
Vect.idr:7:26--8:1:While processing right hand side of Main.++ at Vect.idr:7:1--8:1:
When unifying plus k k and plus k m
Mismatch between:
k
and
m
这个错误信息表明，两个向量之间存在长度不匹配 -- 我们需要一个长度为 k + m 的向量，但提供了一个长度为 k + k 的向量。
有限集
有限集，顾名思义，是具有有限数量元素的集合。它作为Idris库的一部分，可以通过 Data.Fin 导入，或者可以按以下方式声明：
data Fin : Nat -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
从签名中，我们可以看到这是一个类型构造函数，它接收一个 Nat ，并产生一个类型。所以，这不是一个表示对象的容器的集合，相反，它是未命名元素的典型集合，例如，"5个元素的集合"。实际上，它是一个捕捉零到 (n - 1) 范围内的整数的类型，其中 n 是用来实例化 Fin 类型的参数。例如， Fin 5 可以被认为是0到4之间的整数的类型。
让我们更详细地看看这些构造函数。
FZ 是具有 S k 个元素的有限集的第零个元素； FS n 是具有 S k 元素的有限集的第 n+1 个元素。 Fin 由 Nat 索引，它表示集合中元素的数量。因为我们不能构造一个空集的元素，因此也就无法构造出 Fin Z 。
如上所述， Fin 家族的一个有用的应用是表示有界自然数。由于第一个 n 自然数构成了一个由 n 个元素组成的有限集合，我们可以将 Fin n 作为大于或等于零且小于 n 的整数集合。
例如，下面这个函数通过给定一个有界的索引 Fin n 来查找 Vect 中的元素。在 prelude 中定义如下：
index : Fin n -> Vect n a -> a
index FZ (x :: xs) = x
index (FS k) (x :: xs) = index k xs
这个函数在一个向量的指定位置查找一个值。该位置以向量的长度为界(每种情况下都是 n)，所以不需要进行运行时的边界检查。类型检查器保证该位置不大于向量的长度，当然也不小于零。
还要注意，这里没有 Nil 的情况。这是因为这是不可能的。因为没有类型为 Fin Z 且位置是 Fin n 的元素，那么 n 不可能是 Z 。因此，试图在一个空向量中查找一个元素，会在编译时产生一个类型错误，因为它将迫使 n 成为 Z 。
隐式参数
让我们仔细看看 index 的类型。
index : Fin n -> Vect n a -> a
它需要两个参数，一个是 n 个元素的有限集，一个是 n 个元素的向量，类型是 a 。但是还有两个名字， n 和 a ，这两个名字没有被明确声明。 index 使用了 隐式 参数 。我们也可以把 index 的类型写成：
index : forall a, n . Fin n -> Vect n a -> a
隐式参数是用``forall``声明的，在 index 的应用中没有给出；它们的值可以从 Fin n 和 Vect n a 参数的类型中推测出来。在类型声明中作为参数或索引出现的任何以小写字母开头的名称，如果没有应用于任何参数， 总是 会自动被绑定为隐式参数；这就是为什么数据类型名称不能以小写字母开头。隐式参数仍然可以在应用程序中明确给出，例如，使用 {a=value} 和 {n=value} 。
index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
事实上，任何参数，不管是隐式还是显式，都可以被赋予一个名字。我们可以将 index 的类型声明为：
index : (i : Fin n) -> (xs : Vect n a) -> a
你是否要这样做是一个品味问题--有时它可以帮助记录一个函数，使参数的目的更加明确。
隐式参数的名字在函数的主体中是有作用域的，尽管它们在运行时不能使用。关于隐式参数还有很多要说的--我们将在 多重性 一节中讨论在运行时也可以使用的问题，以及其他事项
注：声明顺序和 mutual 块
一般来说，函数和数据类型必须在使用前定义，因为依值类型允许函数作为类型的一部分出现，而类型检查可以依赖于特定函数的定义方式（尽管这只适用于完全函数；见 完备性检查（Totality Checking））。然而，可以通过使用 mutual 块来放宽这个限制，它允许数据类型和函数同时被定义：
mutual
even : Nat -> Bool
even Z = True
even (S k) = odd k
odd : Nat -> Bool
odd Z = False
odd (S k) = even k
在 mutual 块中，首先添加所有的类型声明，然后是函数体。因此，任何一个函数类型都不会依赖于块中其它函数的递归行为。
前向声明可以让你对相互定义的概念的声明顺序有更精细的控制。如果你需要在相互定义的函数的类型中提到一个数据类型的构造函数，或者需要依靠相互定义的函数的行为来进行类型检查，这就很有用。
data V : Type
T : V -> Type
data V : Type where
N : V
Pi : (a : V) -> (b : T a -> V) -> V
T N = Nat
T (Pi a b) = (x : T a) -> T (b x)
data Even : Nat -> Type
data Odd : Nat -> Type
data Even : Nat -> Type where
ZIsEven : Even Z
SOddIsEven : Odd n -> Even (S k)
data Odd : Nat -> Type where
SEvenIsOdd : Even n -> Odd (S k)
even : Nat -> Bool
odd : Nat -> Bool
-- or just ``even, odd : Nat -> Bool``
even Z = True
even (S k) = odd k
odd Z = False
odd (S k) = even k
将签名声明放在前面可以建议 Idris 检 测他们相应的相互定义。
I/O
如果计算机程序不以某种方式与用户或系统互动，那么它们就没有什么用处。像 Idris 这样的纯语言 -- 即表达式没有副作用的语言 -- 的困难在于 I/O 本质上是有副作用的。因此， Idris 提供了一个参数化的类型 IO ， 描述 运行时系统在执行一个函数时将执行的交互作用：
data IO a -- description of an IO operation returning a value of type a
我们先给出 IO 的抽象化定义，但实际上它描述了要执行的 I/O 操作是什么，而不是如何执行它们。由此产生的操作是在外部由运行时系统执行的。我们已经看到了一个I/O程序：
main : IO ()
main = putStrLn "Hello world"
putStrLn 的类型表明它接收一个字符串，并返回一个产生单元类型 () 元素的 I/O 动作。它还有一个变体 putStr，用于输出不带换行符的字符串：
putStrLn : String -> IO ()
putStr : String -> IO ()
我们还可以从用户输入中读取字符串：
getLine : IO String
还有一些其他的 I/O 操作可用。例如，通过在你的程序中添加 import System.File ，你可以获得读写文件的函数，包括：
data File -- abstract
data Mode = Read | Write | ReadWrite
openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
closeFile : File -> IO ()
fGetLine : (h : File) -> IO (Either FileError String)
fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
fEOF : File -> IO Bool
请注意，其中几个会返回 Either ，因为它们可能会失败。
“ do ” 记法
I/O 程序通常需要对行动进行排序，将一个计算的输出输入到下一个计算的输入中。然而， IO 是一个抽象类型，所以我们不能直接访问一个计算的结果。相反，我们用 do 记法来排列操作：
greet : IO ()
greet = do putStr "What is your name? "
name <- getLine
putStrLn ("Hello " ++ name)
语法 x <- iovalue 执行I/O操作 iovalue ，类型为 IO a ，并将类型为 a 的结果放入变量 x 。在这种情况下， getLine 返回一个 IO String ，所以 name 具有类型 String 。缩进很重要 -- do 块中的每个语句必须在同一列开始。 pure 操作允许我们将一个值直接注入到一个 IO 操作中：
pure : a -> IO a
我们将在后面看到， do 符号比这里展示的更加通用，而且可以重载。
你可以尝试在 Idris 2 REPL 执行 greet ，运行命令 :exec greet ：
惰性
通常情况下，函数的参数在函数本身之前被求值（也就是说，Idris使用 及早 求值策略）。然而，这并不总是最好的方法。考虑一下下面的函数：
ifThenElse : Bool -> a -> a -> a
ifThenElse True t e = t
ifThenElse False t e = e
这个函数会使用 t 或 e 参数中的一个，而不是两个都用。我们希望 只有 被使用的参数被求值。为了实现这一点，Idris 提供了一个 Lazy 原语，它允许暂缓求值。它是一个原语，但在概念上我们可以把它看成是这样：
data Lazy : Type -> Type where
Delay : (val : a) -> Lazy a
Force : Lazy a -> a
一个 Lazy a 类型的值是不被求值的，直到它被 Force 强迫。Idris 类型检查器知道 Lazy 类型，并在必要时插入 Lazy a 和 a 之间的转换，反之亦然。因此，我们可以这样写 ifThenElse ，而不需要明确使用 Force 或 Delay ：
ifThenElse : Bool -> Lazy a -> Lazy a -> a
ifThenElse True t e = t
ifThenElse False t e = e
无限数据类型
我们可以通过余数据类型（codata），将递归参数标记为潜在无穷来定义无限的数据结构。余数据类型的一个例子是Stream，它的定义如下。
data Stream : Type -> Type where
(::) : (e : a) -> Inf (Stream a) -> Stream a
下面是一个例子，说明余数数据类型 Stream 可以用来形成一个无限的数据结构。在这种情况下，我们正在创建一个无限的 1 的流。
ones : Stream Nat
ones = 1 :: ones
有用的数据类型
Idris包括一些有用的数据类型和库函数（见发行版中的 libs/ 目录，以及`文档 <https://www.idris-lang.org/pages/documentation.html>`_ ）。本节描述了其中一些，以及如何导入它们。
List 和 Vect
我们已经看到过 List 和 Vect 数据类型：
data List a = Nil | (::) a (List a)
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
你可以通过 import Data.Vect 获得对 Vect 的访问。请注意，List 和 Vect 每个构造函数的名字都是一样的 -- 构造函数的名字（事实上，一般的名字）可以被重载，只要它们被声明在不同的命名空间（见章节 模块和命名空间 ），并且通常会根据它们的类型来解析。作为语法糖，任何被命名为 Nil 和 :: 的实现都可以写成列表形式。例如：
[]表示Nil[1,2,3]表示1 :: 2 :: 3 :: Nil
同样，任何名称为 Lin 和 :< 的实现都可以写成 snoc-list 形式：
[<]表示Lin[< 1, 2, 3]表示Lin :< 1 :< 2 :< 3。
prelude 包括一个预定义的 snoc-lists 的数据类型：
data SnocList a = Lin | (:<) (SnocList a) a
该库还定义了一些用于操作这些类型的函数。 map 对 List 和 Vect 都是重载的（我们将在后面的 接口 章节中讨论接口时看到更多精确的细节），并对列表或向量的每个元素应用一个函数。
map : (a -> b) -> List a -> List b
map f [] = []
map f (x :: xs) = f x :: map f xs
map : (a -> b) -> Vect n a -> Vect n b
map f [] = []
map f (x :: xs) = f x :: map f xs
例如，给定以下的整数向量，和一个将整数加倍的函数：
intVec : Vect 5 Int
intVec = [1, 2, 3, 4, 5]
double : Int -> Int
double x = x * 2
函数 map 可用于将向量中的每个元素翻倍：
*UsefulTypes> show (map double intVec)
"[2, 4, 6, 8, 10]" : String
关于 List 和 Vect 上的函数的更多细节，请查阅库文件：
libs/base/Data/List.idrlibs/base/Data/Vect.idr
函数包括过滤、追加、反转等。
题外话：匿名函数和操作符段
有更多的方法来写上述表达式。其中一种方法是使用匿名函数：
*UsefulTypes> show (map (\x => x * 2) intVec)
"[2, 4, 6, 8, 10]" : String
符号 \x => val 构建了一个匿名函数，它接受一个参数 x 并返回表达式 val 。匿名函数可以接受多个参数，用逗号分隔，例如： \x, y, z => val 。参数也可以被赋予明确的类型，例如： \x : Int => x * 2 ，并且可以模式匹配，例如： \(x, y) => x + y 。另外我们也可以使用一个操作符段：
*UsefulTypes> show (map (* 2) intVec)
"[2, 4, 6, 8, 10]" : String
(*2) 是一个将一个数字乘以2的函数的缩写。它可以被扩展为 \x => x * 2 。类似地， (2*) 将被扩展为 \x => 2 * x 。
Maybe
Maybe 被定义在 Prelude 中，描述了一个可选的值。要么有一个给定类型的值，要么没有：
data Maybe a = Just a | Nothing
Maybe 是给操作提供类型的一种方式，可能会失败。例如，在 List （而不是一个向量）中查找东西可能会导致越界错误：
list_lookup : Nat -> List a -> Maybe a
list_lookup _ Nil = Nothing
list_lookup Z (x :: xs) = Just x
list_lookup (S k) (x :: xs) = list_lookup k xs
maybe 函数用于处理 Maybe 类型的值，如果有值可以对该值应用一个函数，或者提供一个默认值后再应用函数：
maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
注意，前两个参数的类型被包裹在 Lazy 中。由于这两个参数中只有一个会被实际使用，我们把它们标记为 Lazy ，以防它们是复杂的表达式，计算后再丢弃它们会很浪费。
元组
值可以用以下内置数据类型配对：
data Pair a b = MkPair a b
作为语法糖，我们可以写 (a, b) ，根据上下文，这意味着 Pair a b 或 MkPair a b 。元组可以包含任意数量的值，以嵌套对的形式表示：
fred : (String, Int)
fred = ("Fred", 42)
jim : (String, Int, String)
jim = ("Jim", 25, "Cambridge")
*UsefulTypes> fst jim
"Jim" : String
*UsefulTypes> snd jim
(25, "Cambridge") : (Int, String)
*UsefulTypes> jim == ("Jim", (25, "Cambridge"))
True : Bool
依值对
依值对允许一个对中的第二个元素的类型取决于第一个元素的值：
data DPair : (a : Type) -> (p : a -> Type) -> Type where
MkDPair : {p : a -> Type} -> (x : a) -> p x -> DPair a p
同样，这也有语法上的糖。 (x : a ** p) 是一对 A 和 P 的类型，其中名称 x 可以出现在 p 里面。 ( x ** p ) 构建一个该类型的值。例如，我们可以将一个数字与一个特定长度的 Vect 配对：
vec : (n : Nat ** Vect n Int)
vec = (2 ** [3, 4])
如果你愿意，你可以用长的方式写出来；两者是等同的：
vec : DPair Nat (\n => Vect n Int)
vec = MkDPair 2 [3, 4]
类型检查器可以从向量的长度推断出第一个元素的值。我们可以写一个下划线``_``来代替我们期望类型检查器填写的值，所以上述定义也可以写成：
vec : (n : Nat ** Vect n Int)
vec = (_ ** [3, 4])
我们也可能倾向于省略这对元素中第一个元素的类型，因为它同样可以被推断出来：
vec : (n ** Vect n Int)
vec = (_ ** [3, 4])
依值对的一个用途是返回依值类型的值，其中的索引不一定事先知道。例如，如果我们根据一些谓词从 Vect 中过滤出元素，我们将不会事先知道所产生的向量的长度：
filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
如果 Vect 是空的，结果就是：
filter p Nil = (_ ** [])
在 :: 的情况下，我们需要检查对 filter 的递归调用的结果，从结果中提取长度和矢量。要做到这一点，我们使用 case 表达式，它允许对中间值进行模式匹配：
filter : (a -> Bool) -> Vect n a -> (n' ** Vect n' a)
filter p Nil = (_ ** [])
filter p (x :: xs)
= case filter p xs of
(_ ** xs') => if p x then (_ ** x :: xs')
else (_ ** xs')
依值对有时被称为 "Sigma 类型"。
记录
记录 是将几个值（记录的*字段* ）收集在一起的数据类型。Idris 提供了定义记录的语法，并自动生成字段访问和更新函数。与用于数据结构的语法不同，Idris 中的记录遵循一种与 Haskell 不同的语法。例如，我们可以在一个记录中表示一个人的名字和年龄：
record Person where
constructor MkPerson
firstName, middleName, lastName : String
age : Int
fred : Person
fred = MkPerson "Fred" "Joe" "Bloggs" 30
使用 constructor 关键字提供构造函数名称，然后给出*字段* ，这些字段在 where 关键字之后的缩进块中（这里是 firstName ， middleName ， lastName ，和 age ）。你可以在一行中声明多个字段，只要它们具有相同的类型。字段名可以用来访问字段的值：
*Record> fred.firstName
"Fred" : String
*Record> fred.age
30 : Int
*Record> :t (.firstName)
Main.Person.(.firstName) : Person -> String
我们可以使用前缀字段投影，就像在Haskell中一样：
*Record> firstName fred
"Fred" : String
*Record> age fred
30 : Int
*Record> :t firstName
firstName : Person -> String
可以使用pragma %prefix_record_projections off 在每条记录的定义中禁用前缀字段投影，这使得所有随后定义的记录只产生点状的投影。这个 pragma 在模块结束前或在最近一次出现 %prefix_record_projections on 之前都是有效的。
我们还可以使用字段名来更新一条记录（或者更准确地说，产生一个更新了给定字段的记录副本）：
*Record> { firstName := "Jim" } fred
MkPerson "Jim" "Joe" "Bloggs" 30 : Person
*Record> { firstName := "Jim", age $= (+ 1) } fred
MkPerson "Jim" "Joe" "Bloggs" 31 : Person
语法 { field := val, ... } 产生一个函数，更新记录中的给定字段。 := 给一个字段分配一个新的值， $= 应用一个函数来更新它的值。
每条记录都被定义在自己的命名空间中，这意味着字段名可以在多条记录中重复使用。
记录和记录中的字段可以有依值类型。允许更新改变一个字段的类型，只要其结果是良类型。
record Class where
constructor ClassInfo
students : Vect n Person
className : String
将 students 字段更新为不同长度的向量是安全的，因为它不会影响记录的类型：
addStudent : Person -> Class -> Class
addStudent p c = { students := p :: students c } c
*Record> addStudent fred (ClassInfo [] "CS")
ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
我们也可以用 $= 来更简洁地定义 addStudent ：
addStudent' : Person -> Class -> Class
addStudent' p c = { students $= (p ::) } c
嵌套记录投影
嵌套的记录字段可以使用点符号访问：
x.a.b.c
map (.a.b.c) xs
对于点符号，点后不能有空格，但是点前可以有空格。合成投影必须有括号，否则 map .a.b.c xs 将被理解为 map.a.b.c xs 。
嵌套的记录字段也可以用前缀符号访问：
(c . b . a) x
map (c . b . a) xs
周围有空格的点代表函数组合运算符。
嵌套记录更新
Idris 还提供了一个方便的语法来访问和更新嵌套记录。例如，如果一个字段可以用表达式 x.a.b.c 来访问，它可以用以下语法来更新：
{ a.b.c := val } x
这将返回一个新的记录，由路径 a.b.c 访问的字段被设置为 val 。语法也是一等的，即 { a.b.c := val } 本身有一个函数类型。
$= 符号对嵌套的记录更新也有效。
依值记录
记录也可以依赖于数值。记录有 参数 ，这些参数不能像其他字段一样被更新。参数作为结果类型的参数出现，并写在记录类型名称的后面。例如，一个对类型可以定义如下：
record Prod a b where
constructor Times
fst : a
snd : b
使用前面的 Class 记录，可以用 Vect 来限制类的大小，并通过对记录的大小进行参数化，将大小纳入类型。 例如：
record SizedClass (size : Nat) where
constructor SizedClassInfo
students : Vect size Person
className : String
在前面 addStudent 的情况下，我们仍然可以在 SizedClass 上添加一个学生，因为大小是隐含的，当添加一个学生的时候大小会被更新：
addStudent : Person -> SizedClass n -> SizedClass (S n)
addStudent p c = { students := p :: students c } c
事实上，我们刚才看到的依值对类型在实践中被定义为一条记录，其字段 fst 和 snd 允许从依值对中投影出数值：
record DPair a (p : a -> Type) where
constructor MkDPair
fst : a
snd : p fst
可以使用记录更新语法来更新依赖字段，前提是所有相关字段都要一次性更新。例如：
cons : t -> (x : Nat ** Vect x t) -> (x : Nat ** Vect x t)
cons val xs
= { fst := S (fst xs),
snd := (val :: snd xs) } xs
甚至可以更省事：
cons' : t -> (x : Nat ** Vect x t) -> (x : Nat ** Vect x t)
cons' val
= { fst $= S,
snd $= (val ::) }
更多表达式
let 绑定
计算出的中间值可以使用 let 来绑定到变量：
mirror : List a -> List a
mirror xs = let xs' = reverse xs in
xs ++ xs'
我们也可以在 let 绑定中进行模式匹配。例如，我们可以从记录中提取字段，如下所示，也可以通过在顶层进行模式匹配：
data Person = MkPerson String Int
showPerson : Person -> String
showPerson p = let MkPerson name age = p in
name ++ " is " ++ show age ++ " years old"
这些 let 绑定可以使用类型注解：
mirror : List a -> List a
mirror xs = let xs' : List a = reverse xs in
xs ++ xs'
由于 = 既可以表示类型相等（=== 或 ~=~）也可以表示定义，某些表达式可能会有歧义。这里是一个例子：
-- Diag : a -> Type
-- Diag v = let ty : Type = v = v in ty
-- ^
-- |
-- Doesnt compile! because ambiguous here
在这种情况下，我们也可以使用符号 := 来代替 =，除其他用途外，还可以避免与命题相等性相关的歧义：
Diag : a -> Type
Diag v = let ty : Type := v = v in ty
上面的代码可以读作 "ty 的类型是 Type 并且它的值是 v = v"。
局部定义也可以使用 let 引入。就像顶层定义和在 where 子句中定义的一样，你需要：
声明函数和它的类型
通过模式匹配来定义函数
foldMap : Monoid m => (a -> m) -> Vect n a -> m
foldMap f = let fo : m -> a -> m
fo ac el = ac <+> f el
in foldl fo neutral
符号 := 不能在局部函数定义中使用。这意味着它可以用来交错使用 let 绑定和局部定义，而不会引入歧义。
foldMap : Monoid m => (a -> m) -> Vect n a -> m
foldMap f = let fo : m -> a -> m
fo ac el = ac <+> f el
initial := neutral
-- ^ this indicates that `initial` is a separate binding,
-- not relevant to definition of `fo`
in foldl fo initial
列表推导式
Idris提 供了 推导式 符号，作为建立列表的方便速记法。其一般形式是：
[ expression | qualifiers ]
通过对 expression 进行求值，根据逗号分隔的 qualifiers 给出的条件生成一个符合条件的列表。例如，我们可以建立一个毕达哥拉斯三段论的列表，如下所示：
pythag : Int -> List (Int, Int, Int)
pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
x*x + y*y == z*z ]
[a..b] 符号是另一种速记方法，它在 a 和 b 之间建立一个数字列表。或者 [a,b..c] 在 a 和 c 之间建立一个数字列表，增量由 a 和 b 之间的差异指定。这适用于 Nat, Int 和 Integer 类型，是 prelude 中的 enumFromTo 和 enumFromThenTo 函数的语法糖。
case 表达式
另一种检查中间值的方法是使用 case 表达式。例如，下面的函数在一个给定的字符处将一个字符串分成两个：
splitAt : Char -> String -> (String, String)
splitAt c x = case break (== c) x of
(l, r) => (l, strTail r)
break 是一个库函数，它在给定函数返回真值的地方将一个字符串分解成一对子字符串。然后我们对它返回的一对子字符串进行解构，并删除第二个子字符串的第一个字符。
一个 case 表达式可以匹配多种情况，例如，检查一个中间值的类型 Maybe a 。回顾 list_lookup 函数，它在一个列表中查找一个索引，如果索引出界则返回 Nothing 。我们可以用它来写 lookup_default ，它查找一个索引，如果索引出界则返回一个默认值：
lookup_default : Nat -> List a -> a -> a
lookup_default i xs def = case list_lookup i xs of
Nothing => def
Just x => x
如果索引在范围内，我们得到该索引的值，否则我们得到一个默认值：
*UsefulTypes> lookup_default 2 [3,4,5,6] (-1)
5 : Integer
*UsefulTypes> lookup_default 4 [3,4,5,6] (-1)
-1 : Integer
完全性
Idris 区分了 完全 和 部分 函数。完全函数是一个这样的函数，它要么：
对所有可能的输入终止，或者
产生一个可能无限结果的非空有限前缀
如果一个函数是完全的，我们可以认为其类型是对该函数将做什么的精确描述。例如，如果我们有一个返回类型为 String 的函数，我们知道一些不同的东西，这取决于它是否是完全的：
如果是完全的，它将在有限时间内返回一个类型为
String的值：如果是部分的，那么只要不崩溃或进入无限循环，就会返回一个
String。
Idris 做了这个区分，所以它知道哪些函数在类型检查时是安全的（正如我们在 一等类型 中看到的）。毕竟，如果它试图在类型检查期间求值一个没有终止的函数，那么类型检查就不会终止！因此，在类型检查期间，只有完全函数会被求值。部分函数仍然可以在类型中使用，但不会被进一步求值。