类型与函数¶
原语类型¶
Idris 定义了一些原语(Primitive)类型:Int
、Integer
和 Double
用于数值类型,
Char
和 String
用于文本操作,Ptr
则表示外部指针。库中还声明了一些数据类型,
包括 Bool
及其值 True
和 False
。我们可以用这些类型来声明常量。
将以下内容保存到文件 Prims.idr
中,在命令行中输入 idris Prims.idr
以将其加载到 Idris 的交互式环境中:
module Prims
x : Int
x = 42
foo : String
foo = "Sausage machine"
bar : Char
bar = 'Z'
quux : Bool
quux = False
提示
原语(Primitive)本意为不可分割的基本构件,原语类型即最基本的类型。
Idris 文件由一个可选的模块声明(此处为 module Prims
),一个可选的导入列表,
一组声明及其定义构成。在本例中并未指定导入。Idris 可由多个模块构成,
每个模块中的每个定义都有它自己的命名空间。这点会在 模块与命名空间
一节中进一步讨论。在编写 Idris 程序时,声明的顺序和缩进都很重要。
函数和数据类型必须先定义再使用,每个定义都必须有类型声明,例如之前列出的
x : Int
和 foo : String
。新声明的缩进级别必须与之前的声明相同。
此外,分号 ;
也可用于结束声明。
库模块 Prelude
会在每个 Idris 程序中自动导入,包括 IO 功能,算术运算,
数据结构以及多种通用函数。Prelude 中定义了一些算术和比较运算符,
我们可以在提示符中使用它们。在提示符中进行求值会给出一个答案及其类型。例如:
*prims> 6*6+6
42 : Integer
*prims> x == 6*6+6
True : Bool
Idris 为原语类型定义了所有的普通算术和比较运算。它们通过接口进行了重载,
并可被扩展以适用于用户定义的类型,这点我们会在 接口
一节中讨论。布尔表达式可通过 if...then...else
构造来测试,例如:
*prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
"The answer!" : String
数据类型¶
数据类型的声明方式和语法与 Haskell 非常相似。例如,自然数和列表的声明如下:
data Nat = Z | S Nat -- 自然数(零与后继)
data List a = Nil | (::) a (List a) -- 多态列表
以上声明来自于标准库。一进制自然数要么为零(Z
),
要么就是另一个自然数的后继(S k
);列表要么为空(Nil
),
要么就是一个值被添加在另一个列表之前(x :: xs
)。
在 List
的声明中,我们使用了中缀操作符 ::
。
像这样的新操作符可通过缀序声明(Fixity Declaration)来添加,如下所示:
infixr 10 ::
函数、数据构造器与类型构造器均可用名字作为中缀操作符。它们被括在括号中时,
也可作为前缀形式使用,例如 (::)
。中缀操作符可使用下面的任何符号:
:+-*\/=.?|&><!@$%^~#
有些以这些符号构成的操作符无法被用户定义。它们是
:
、=>
、->
、<-
、=
、?=
、|
、**
、
==>
、\
、%
、~
、?
以及 !
。
函数¶
函数通过模式匹配(Pattern Matching)实现,语法同样和 Haskell 类似。
其主要的不同在于 Idris 的所有函数都需要类型声明,声明中使用单冒号 :
(而非 Haskell 的双冒号 ::
)。自然数的某些运算函数定义如下,同样来自标准库:
-- 一进制加法
plus : Nat -> Nat -> Nat
plus Z y = y
plus (S k) y = S (plus k y)
-- 一进制乘法
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 提示符中测试这些函数:
Idris> plus (S (S Z)) (S (S Z))
4 : Nat
Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
12 : Nat
注解
在显示一个 Nat
元素,如 (S (S (S (S Z))))
时,Idris 会将其显示为
4
。 plus (S (S Z)) (S (S Z))
的结果实际上为 (S (S (S (S Z))))
,
即自然数 4
。这点可在 Idris 提示符中验证:
Idris> (S (S (S (S Z))))
4 : Nat
和算术运算符一样,整数字面也可通过接口重载,因此我们也能像下面这样测试函数:
Idris> plus 2 2
4 : Nat
Idris> mult 3 (plus 2 2)
12 : Nat
你可能会很好奇,既然计算机已经完美内建了整数运算,我们为何还需要一进制的自然数?
主要的原因在于一进制数的结构非常便于推理,而且易与其它数据结构建立联系,
我们之后就会看到。尽管如此,我们并不希望以牺牲效率为代价获得这种便捷。幸运的是,
Idris 知道 Nat
(以及类似的结构化类型)和数之间的联系,
这意味着 Idris 可以优化它们的表示以及像 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
被重新定义了)。若某个名字是某个类型的
形参(Parameter),那么仅当它在类型中出现时才会在 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
从句中定义的函数和其它顶层函数一样,都需要类型声明。
然而,函数 f
的类型声明可在以下情况中省略:
f
出现在顶层定义的右边f
的类型完全可以通过其首次应用来确定
因此,举例来说,以下定义是合法的:
even : Nat -> Bool
even Z = True
even (S k) = odd k where
odd Z = False
odd (S k) = even k
test : List Nat
test = [c (S 1), c Z, d (S Z)]
where c x = 42 + x
d y = c (y + 1 + z y)
where z w = y + w
坑¶
Idris 程序中可以挖 坑(Hole) 来表示未完成的部分。例如,我们可以在「Hello world」
程序中为问候语 greeting
挖一个坑:
main : IO ()
main = putStrLn ?greeting
语法 ?greeting
挖了个坑,它表示程序中尚未写完的部分。这是个有效的 Idris
程序,你可以检查 greeting
的类型:
*Hello> :t greeting
--------------------------------------
greeting : String
检查坑的类型也会显示作用域中所有变量的类型。例如,给定一个未完成的 even
定义:
even : Nat -> Bool
even Z = True
even (S k) = ?even_rhs
我们可以检查 even_rhs
的类型,查看期望的返回类型,以及变量 k
的类型:
*Even> :t even_rhs
k : Nat
--------------------------------------
even_rhs : Bool
坑非常有用,因为它能帮助我们 逐步地 编写函数。我们无需一次写完整个函数, 而是留下一些尚未编写的部分,让 Idris 告诉我们如何完成其定义。
提示
lhs(left hand side) 与 rhs(right hand side)分别表示等式中等号的左边和右边, 即左式和右式。
依赖类型¶
一等类型¶
在 Idris 中,类型是一等(First-Class)的,即它们可以像其它的语言构造那样被计算和操作 (以及传给函数)。例如,我们可以编写一个用来计算类型的函数:
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat
该函数可从一个 Bool
值计算出适当的类型,布尔值表示其类型是否为一个单例(Singleton)。
我们可以在任何能够使用类型的地方用该函数计算出一个类型。例如,它可用于计算返回类型:
mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []
它也可拥有不同的输入类型。以下函数能够计算 Nat
列表之和,或者返回给定的
Nat
,这取决于单例标记 single
是否为 True
:
sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum False (x :: xs) = x + sum False xs
向量¶
依赖类型的一个范例就是「带长度的列表」类型,在依赖类型的文献中,
它通常被称作向量(Vector)。向量作为 Idris 库的一部分,可通过导入 Data.Vect
来使用,当然我们也自己声明它:
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
注意我们使用了与 List
相同的构造器名。只要名字声明在不同的命名空间内
(在实践中,通常在不同的模块内),Idris 就能接受像这样的特设(ad-hoc)名重载。
有歧义的构造器名称通常可根据上下文来解决。
这里声明了一个类型族(Type Family),该声明的形式与之前的简单类型声明不太一样。
我们显式地描述了类型构造器 Vect
的类型,它接受一个 Nat
和一个类型作为参数,其中 Type
表示类型的类型。我们说 Vect
通过 Nat
来 索引,并被 Type
参数化 。
每个构造器会产生该类型家族的不同部分。 Nil
只能用于构造零长度的向量,
而 ::
用于构造非零长度的向量。在 ::
的类型中,我们显式地指定了一个类型为
a
的元素和一个类型为 Vect k a
的尾部(Tail)(即长度为 k
的向量),
二者构成了一个长度为 S k
的向量。
同 List
以及 Nat
这类简单类型一样,我们可以通过模式匹配以同样的方式为
Vect
这样的依赖类型定义函数。
作用于 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 -- 有误
在经由 Idris 类型检查器检查时,它会给出以下结果:
$ idris VBroken.idr --check
VBroken.idr:9:23-25:
When checking right hand side of Vect.++ with expected type
Vect (S k + m) a
When checking an application of constructor Vect.:::
Type mismatch between
Vect (k + k) a (Type of xs ++ xs)
and
Vect (plus k m) a (Expected type)
Specifically:
Type mismatch between
plus k k
and
plus k m
该错误信息指出两个向量的长度不匹配:我们需要一个长度为 k + m
的向量,
而你提供了一个长度为 k + k
的向量。
有限集¶
有限集,顾名思义,即元素有限的集合。它作为 Idris 库的一部分,可通过导入
Data.Fin
来使用,当然也可以像下面这样声明它:
data Fin : Nat -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
从它的签名中,我们可以看出该类型构造器接受一个 Nat
,然后产生一个 类型 。
因此,它不是一个「对象的容器」意义上的集合,而是个拥有无名元素的一般集合。举例来说,
就是「存在一个包含五个元素的集合」的那种集合。实际上,它是一个捕获了所有落入零至
(n - 1)
范围内的整数的类型,其中 n
是用于实例化 Fin
类型的参数。例如,
Fin 5
可被视作从 0 到 4 之间的整数的类型。
我们来仔细地观察一下它的构造器。
对于拥有 S k
个元素的有限集来说,FZ
是它的第零个元素,
FS n
则是它的第 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
元素有限集的元素,以及一个类型为 a
的 n
元素向量。不过这里还有两个名字:n
和 a
,它们未被显式地声明。index
包含了 隐式 参数。我们也可以将 index
的类型写作:
index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
隐式参数在类型声明的大括号 {}
中给定,它们并没有在应用 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
写不写它纯属偏好问题,不过有时它能让参数更加明确,有助于函数文档的记录。
此外, {}
在等号左边时可用作模式匹配,即 {var = pat}
获取一个隐式变量,
并试图对「pat」进行模式匹配。例如:
isEmpty : Vect n a -> Bool
isEmpty {n = Z} _ = True
isEmpty {n = S k} _ = False
「using
」记法¶
有时为隐式参数提供类型会十分有用,特别是存在依赖顺序,或隐式参数本身含有依赖的情况下。
例如,我们可能希望在以下定义中指明隐式参数的类型,它为向量定义了前提(它也在
Data.Vect
的 Elem
下定义):
data IsElem : a -> Vect n a -> Type where
Here : {x:a} -> {xs:Vect n a} -> IsElem x (x :: xs)
There : {x,y:a} -> {xs:Vect n a} -> IsElem x xs -> IsElem x (y :: xs)
IsElem x xs
的实例描述了 x
是 xs
中的一个元素。我们可以构造这样的谓词:
若所需的元素在向量的头部时为 Here
,在向量的尾部中时则为 There
。例如:
testVec : Vect 4 Int
testVec = 3 :: 4 :: 5 :: 6 :: Nil
inVect : IsElem 5 Main.testVec
inVect = There (There Here)
重要
隐式参数与作用域
在类型签名中,类型检查器会将所有以小写字母开头 并且 没有应用到别的东西上的变量
视作隐式变量。要让上面的代码示例能够编译,你需要为 testVec
提供一个限定名。
在前面的例子中,我们假设该代码处于 Main
模块内。
如果大量使用相同的隐式参数,就会导致定义难以阅读。为避免此问题,可使用 using
块来为任何在块中出现的隐式参数指定类型和顺序:
using (x:a, y:a, xs:Vect n a)
data IsElem : a -> Vect n a -> Type where
Here : IsElem x (x :: xs)
There : IsElem x xs -> IsElem x (y :: xs)
注:声明顺序与 mutual
互用块¶
通常,函数与数据类型必须在使用前定义,因为依赖类型允许函数作为类型的一部分出现,
而类型检查会依赖于特定的函数如何定义(尽管这只对全函数成立,见 完全性检查)。
然而,此限制可通过使用 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
块中,首先所有的类型声明会被添加,然后是函数体。
因此,没有一个函数类型可以依赖于块中任何函数的归约行为。
I/O¶
如果计算机程序不能通过某种方式与用户或系统进行交互,那么它基本上没什么用。在 Idris
这样纯粹(Pure)的语言中,表达式没有副作用(Side-Effect)。而 I/O
的难点在于它本质上是带有副作用的。因此在 Idris 中,这样的交互被封装在 IO
类型中:
data IO a -- IO 操作返回一个类型为 a 的值
我们先给出 IO
抽象的定义,它本质上描述了被执行的 I/O 操作是什么,
而非如何去执行它们。最终操作则由运行时系统在外部执行。我们已经见过一个带 IO
的程序了:
main : IO ()
main = putStrLn "Hello world"
putStrLn
的类型描述了它接受一个字符串,然后通过 I/O 活动返回一个单元类型
()
的元素。它还有一个变体 putStr
用来输出字符串但不换行。
putStrLn : String -> IO ()
putStr : String -> IO ()
我们可以从用户的输入中读取字符串:
getLine : IO String
Prelude 中定义了很多 I/O 操作,例如为了读写文件,需要包含:
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
执行 IO a
类型的 I/O 操作 iovalue
,然后将类型为
a
的结果送入变量 x
中。在这种情况下,getLine
会返回一个
IO String
,因此 name
的类型为 String
。缩进十分重要:
do 语句块中的每个语句都必须从同一列开始。pure
操作允许我们将值直接注入到
IO 操作中:
pure : a -> IO a
后面我们会看到,do
-记法比这里的展示更加通用,并且可以被重载。
惰性¶
通常,函数的参数会在函数被调用前求值(也就是说,Idris 采用了 及早(Eager) 求值策略)。然而,这并不总是最佳的方式。考虑以下函数:
ifThenElse : Bool -> a -> a -> a
ifThenElse True t e = t
ifThenElse False t e = e
该函数会使用参数 t
或 e
二者之一,而非二者都用(我们之后会看到其实它被用于实现
if...then...else
构造)。我们更希望 只有 用到的参数才被求值。为此,
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
余数据类型¶
我们可以通过余数据类型,将递归参数标记为潜在无穷来定义无穷数据结构。对于一个余数据类型
T
,其每个构造器中类型为 T
的参数都会被转换成类型为 Inf T
的参数。
这会让每个 T
类型的参数惰性化,使得类型为 T
的无穷数据结构得以构建。
余数据类型的一个例子为 Stream
,其定义如下:
codata Stream : Type -> Type where
(::) : (e : a) -> Stream a -> Stream a
它会被编译器翻译成下面这样:
data Stream : Type -> Type where
(::) : (e : a) -> Inf (Stream a) -> Stream a
以下是如何用余数据类型 Stream
来构建无穷数据结构的例子。
在这里我们创建了一个 1 的无穷流:
ones : Stream Nat
ones = 1 :: ones
要重点注意:余数据类型不允许创建互用的无穷递归数据结构。 例如,以下代码会创建一个无穷循环并导致栈溢出:
mutual
codata Blue a = B a (Red a)
codata Red a = R a (Blue a)
mutual
blue : Blue Nat
blue = B 1 red
red : Red Nat
red = R 1 blue
mutual
findB : (a -> Bool) -> Blue a -> a
findB f (B x r) = if f x then x else findR f r
findR : (a -> Bool) -> Red a -> a
findR f (R x b) = if f x then x else findB f b
main : IO ()
main = do printLn $ findB (== 1) blue
为了修复它,我们必须为构造器参数的类型显式地加上 Inf
声明,因为余数据类型
不会将它添加到和正在定义的构造器类型 不同 的构造器参数上。例如,以下程序输出「1」。
mutual
data Blue : Type -> Type where
B : a -> Inf (Red a) -> Blue a
data Red : Type -> Type where
R : a -> Inf (Blue a) -> Red a
mutual
blue : Blue Nat
blue = B 1 red
red : Red Nat
red = R 1 blue
mutual
findB : (a -> Bool) -> Blue a -> a
findB f (B x r) = if f x then x else findR f r
findR : (a -> Bool) -> Red a -> a
findR f (R x b) = if f x then x else findB f b
main : IO ()
main = do printLn $ findB (== 1) blue
提示
「归纳数据类型」和「余归纳数据类型」
余数据类型(Codata Type)的全称为余归纳数据类型(Coinductive Data Type), 归纳数据类型和余归纳数据类型是对偶的关系。从语义上看, Inductive Type 描述了如何从更小的 term 构造出更大的 term;而 Coinductive Type 则描述了如何从更大的 term 分解成更小的 term。 二者即为塔斯基不动点定理中的最大不动点(对应余归纳)和最小不动点(对应归纳)。 参考自 Belleve 的回答。
常用数据类型¶
Idris 包含了很多常用的数据类型和库函数(见发行版中的 libs/
目录及
文档 )。本节描述了其中的一部分。
作为 Prelude.idr
的一部分,下面描述的函数都会被每个 Idris 程序自动导入,
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
注意它们的构造器名称是相同的:只要构造器名称在不同的命名空间中声明,
它们就可以被重载(其实一般的名字都可以),并且通常会根据其类型来确定。
作为一种语法糖,任何带有 Nil
和 ::
构造其名的类型都可被写成列表的形式。
例如:
[]
表示Nil
[1,2,3]
表示1 :: 2 :: 3 :: Nil
库中还定义了一些用于操作这些类型的函数。 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
例如,给定以下整数向量,以及一个将整数乘以 2 的函数:
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/prelude/Prelude/List.idr
libs/base/Data/List.idr
libs/base/Data/Vect.idr
libs/base/Data/VectType.idr
其中包括过滤、追加、反转等函数。
题外话:匿名函数与操作符段¶
上面的表达式其实还有更加利落的写法。其中一种就是使用匿名函数(Anonymous Function):
*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
。
提示
匿名函数在函数式编程中又称为 λ-表达式(Lambda Expression)。
Maybe¶
Maybe
描述了可选值,表示给定类型的值是否存在:
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
。
元组¶
值可以通过以下内建的数据类型构成序对(Pair):
data Pair a b = MkPair a b
序对的语法糖可以写成 (a, b)
,根据上下文,其意思为 Pair a b
或 MkPair a b
。元组(Tuple)可包含任意个数的值,它通过嵌套的序对来表示:
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
同样,它也有语法糖。(a : A ** P)
表示由 A 和 P 构成的序对的类型,其中名字
a
可出现在 P
中。( a ** 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
递归调用的结果来提取结果的长度和向量。
为此,我们使用 with
记法,它允许我们对中间值进行模式匹配:
filter p (x :: xs) with (filter p xs)
| ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
我们之后会看到 with
的更多详情。
依赖序对有时被称作「Sigma 类型」。
记录¶
记录(Record) 数据类型将多个值(记录的 字段(Field))收集在一起。 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> firstName fred
"Fred" : String
*Record> age fred
30 : Int
*Record> :t firstName
firstName : Person -> String
我们也可以用字段名来更新一个记录(确切来说,会产生一个更新了给定字段的记录的副本):
*Record> record { firstName = "Jim" } fred
MkPerson "Jim" "Joe" "Bloggs" 30 : Person
*Record> record { firstName = "Jim", age $= (+ 1) } fred
MkPerson "Jim" "Joe" "Bloggs" 31 : Person
语法 record { field = val, ... }
会生成一个更新了记录中给定字段的函数。=
为字段赋予新值,而 $=
通过应用一个函数来更新其值。
每个记录在它自己的命名空间中定义,这意味着字段名可在多个记录中重用。
记录以及记录中的字段可拥有依赖类型。更新允许更改字段的类型,前提是结果是良类型的。
record Class where
constructor ClassInfo
students : Vect n Person
className : String
将 students
的字段更新为不同长度的向量是安全的,因为它不会影响该记录的类型:
addStudent : Person -> Class -> Class
addStudent p c = record { 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 = record { students $= (p ::) } c
嵌套记录的更新¶
Idris 也提供了便于访问和更新嵌套记录的语法。例如,若一个字段可以通过表达式
c (b (a x))
访问,那么它就可通过以下语法更新:
record { a->b->c = val } x
这会返回一个新的记录,通过路径 a->b->c
访问的字段会被设置为 val
。
该语法是一等的,即 record { a->b->c = val }
本身拥有一个函数类型。
与此对应,你也可以使用以下语法访问该字段:
record { a->b->c } x
$=
记法对嵌套记录的更新亦有效。
依赖记录¶
记录也可依赖于值。记录拥有 形参,它无法像其它字段那样更新。 形参作为结果类型的参数出现,写在记录类型名之后。例如,一个序对类型可定义如下:
record Prod a b where
constructor Times
fst : a
snd : b
使用前面的 class
记录,班级的大小可用 Vect
及通过 size
参数化该记录的大小来限制其类型。例如:
record SizedClass (size : Nat) where
constructor SizedClassInfo
students : Vect size Person
className : String
注意 它无法再使用之前的 addStudent
函数了,因为这会改变班级的大小。
现在用于添加学生的函数必须在类型中指定班级的大小加一。由于其大小用自然数指定,
新的值可使用 S
构造器递增:
addStudent : Person -> SizedClass n -> SizedClass (S n)
addStudent p c = SizedClassInfo (p :: students c) (className c)
更多表达式¶
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"
列表推导¶
Idris 提供了 推导 记法作为构建列表的简便写法。一般形式为:
[ expression | qualifiers ]
它会根据逗号分隔的限定式 qualifiers
给定的条件,通过求值表达式 expression
产生的值来生成列表。例如,我们可以按如下方式构建构建勾股三角的列表:
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
,b
之差为增量,构建从 a
到 c
的数列。
它可作用于 Nat
、Int
以及 Integer
,它们使用了 Prelude 中的 enumFromTo
与 enumFromThenTo
函数。
case
表达式¶
另一种检查 简单 类型的中间值的方法是使用 case
表达式。例如,
以下函数在给定的字符处将字符串分为两部分:
splitAt : Char -> String -> (String, String)
splitAt c x = case break (== c) x of
(x, y) => (x, strTail y)
break
是个库函数,它从给定的函数返回 true 的位置将字符串分为一个字符串的序对。
我们接着解构它返回的序对,并移除第二个字符串的第一个字符。
一个 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
限制: case
构造用于对中间表达式进行简单的分析,以此避免编写辅助函数,
它也在内部用于实现 let
和 λ-绑定的模式匹配。它 仅 在以下情况中可用:
- 每个分支 匹配 一个相同类型的值,并 返回 一个相同类型的值。
- 结果的类型是「已知」的,即表达式的类型无需对该
case
表达式进行类型检查就能确定。
完全性¶
Idris 区分 完全(全,Total) 函数与 部分(偏,Partial) 函数。 全函数满足以下情况之一:
- 对于所有可能的输入都会终止,或
- 产生一个非空的,有限的,可能为无限结果的前缀
若一个函数是完全的,我们可以认为其类型精确描述了该函数会做什么。例如,
若我们有一个返回类型为 String
的函数,根据它是否完全,我们能知道的东西会有所不同:
- 若它是全函数,就会在有限的时间内返回一个类型为
String
的值; - 若它是偏函数,那么只要它不崩溃或进入无限循环,就会返回一个
String
。
Idris 对此作了区分,因此它知道在进行类型检查(正如我们在 一等类型 一节所见)的时候,哪些函数可以安全地求值。毕竟,若它在类型检查时试图对一个不终止的函数求值, 那么类型检查将无法终止!因此,在类型检查时只有全函数才会被求值。偏函数仍然可在类型中使用, 但它们不会被进一步求值。