用户定义的数据类型 User defined data types - part 1

本讲义的难度等级

这份讲义包括简单、中等、困难和高级的材料。如果有些材料感觉很难，那可能是因为它很难，而不是你的错。这意味着如果你想在这个模块中取得高分，你必须努力学习，所有模块都是如此。

本讲义的视频讲座

在本讲义的适当位置还链接了以下视频，以方便大家观看。

1. Introduction, the booleans revisited, isomorphisms, Weekdays and the new Maybe type constructor (35 min)
2. Type retracts (13 min)
3. Either and And and pairs (9 min)
4. Lists revisited (9 min)
5. Binary trees (12 min)
6. Directions, addresses and paths in binary trees (15 min)
7. Traversals in binary trees (10 min)
8. Inverting traversals (18 min)

Total 2hrs.

实验一下这里包含的 Haskell 代码 Experimenting with the Haskell code included here

你应该对这些笔记中的 Haskell 代码进行实验，以达到充分理解。这意味着要运行代码并在其中加入一些东西，例如练习和谜题的解决方案，或者你自己的聪明想法。

这些讲义是 markdown 格式，包括 Haskell 代码。为了从 markdown 代码中得到 Haskell 代码，我们可以使用资源目录中的 mdtohs.hs 程序，在 Unix/Linux 终端中，如下所示。

$ cat Data1.md | runhaskell ./mdtohs.hs > Data1.hs

这意味着 "将文件 Data1.md 的内容复制到 Haskell 程序 mdtohs.hs 的标准输入中，并将该程序的输出存储在文件 Data1.hs 中"。这可以等效地写成

$ runhaskell ./mdtohs.hs < Data1.md > Data1.hs

这将删除所有的 markdown 代码，只保留 Haskell 代码，这样我们就可以用它来工作。

我们已经为你运行了这个，文件 Data1.hs 在这个 GitLab 仓库中可用。你可以自己拷贝这个文件，以避免我们更新时发生冲突。

这些讲义中的 Haskell 导入 Haskell imports in these lecture notes

任何需要的库导入都应该在文件的顶部提到。我们需要以下东西来生成用于测试的随机输入：

module Data1 where

import System.Random

类型同义词 Type synonyms

A video discussing the next few sections is available on Canvas.

有时，主要是为了清晰起见，我们可能希望给一个现有的类型起一个新的名字。例如，Haskell 的前奏将字符串定义为一个字符的列表：

type String = [Char]

由于 String 只是一个类型的同义词，所以诸如列表连接和反向

(++) :: [a] -> [a] -> [a]
reverse :: [a] -> [a]

可以自由地应用于字符串：

> "abc" ++ reverse "def"
"abcfed"

类型同义词也可以有参数，例如，在

type Lst a = [a]

用户定义的数据类型 User defined data types

The booleans revisited

布尔在 Haskell 中的定义如下，在前奏中：

data Bool = False | True

这就定义了一个新的类型，叫做 Bool，有两个元素（或者说constructors），叫做 False 和 True。

   False :: Bool
   True  :: Bool

一个数据类型上的函数可以通过在其构造函数上进行模式匹配来方便地定义。例如，在前奏中，联合运算

(&&) :: Bool -> Bool -> Bool

的定义如下：

False && _ = False
True  && x = x

Haskell 中模式匹配语义的一个略微微妙的方面是：

1. 不同的模式匹配条款按照从上到下的顺序被尝试，并且
2. 函数的输入参数只被评估到检查它们是否与当前模式匹配所需的程度。

这种语义的后果是，上述连词的定义实现了短路评估：如果第一个参数是 False，那么函数甚至不评估第二个参数就返回 False。

与此相反，请考虑以下连词的替代定义：

conj :: Bool -> Bool -> Bool
conj False False = False
conj False True  = False
conj True  False = False
conj True  True  = True

这个版本没有实现短路评估：无论第一个参数的值是多少，第二个参数都会被评估。 我们可以通过在 GHC 解释器中运行以下实验来观察这两个版本的 conjunction 之间的区别。

> False && undefined
False
> False `conj` undefined
*** Exception: Prelude.undefined
#CallStack (from HasCallStack):
  error, called at libraries/base/GHC/Err.hs:79:14 in base:GHC.Err
  undefined, called at <interactive>:28:11 in interactive:Ghci5

类型同构 Type isomorphisms

让我们介绍另一个数据类型 BW，定义为

data BW = Black | White

通过类型转换函数，该类型与 Bool 类型是同构的。

bw2bool :: BW -> Bool
bw2bool Black = False
bw2bool White = True

bool2bw :: Bool -> BW
bool2bw False = Black
bool2bw True  = White

这对函数 (bw2bool,bool2bw) 是一个同构，意味着它们是相互逆向的，在这个意义上，它们是

   bw2bool(bool2bw b) = b

for all b :: Bool, and

   bool2bw(bw2bool c) = c

for all c :: BW.

类型同构不应该与类型同义词相混淆。例如，如果我们试图直接使用一个 BW 类型的值，而预期是 Bool 类型的值，我们会得到一个类型错误。

> let test = Black && True

<interactive>:39:1: error:
    • Couldn't match expected type 'Bool' with actual type 'BW'
    • In the first argument of '(&&)', namely 'Black'
      In the expression: Black && True
      In an equation for 'it': it = Black && True

另一方面，如果我们使用显式强制器 bw2bool 和 bool2bw 来包装这些值，那么一切都会被检查：

> let test = bool2bw (bw2bool Black && True)

当然，Black 和 White 的名字是任意的，在 BW 和 Bool 之间还有一个同构，即用 True 替换 Black，用 False替换 White。

bw2bool' :: BW -> Bool
bw2bool' Black = True
bw2bool' White = False

bool2bw' :: Bool -> BW
bool2bw' False = White
bool2bw' True  = Black

当然，Bool 和 BW 这两种类型都是与 Bool 类型同构的（同样以两种不同方式）。

data Bit = Zero | One

的二进制数字。其中一个同构关系如下：

bit2Bool :: Bit  -> Bool
bool2Bit :: Bool -> Bit

bit2Bool Zero  = False
bit2Bool One   = True

bool2Bit False = Zero
bool2Bit True  = One

另一个是以下：

bit2Bool' :: Bit  -> Bool
bool2Bit' :: Bool -> Bit

bit2Bool' Zero  = True
bit2Bool' One   = False

bool2Bit' False = One
bool2Bit' True  = Zero

Note: The syntax rules of Haskell require that both type names (here Bool, BW, Bit) and constructor names (here False, True, Black, White, Zero, One) should start with a capital letter.

Weekdays

数据类型的另一个例子是

data WeekDay = Mon | Tue | Wed | Thu | Fri | Sat | Sun

我们可以要求 Haskell 免费为我们做一些工作（也有其他方法可以用我们自己的汗水来做，使用类型类实例，我们将在后面讨论）：

data WeekDay = Mon | Tue | Wed | Thu | Fri | Sat | Sun
               deriving (Show, Read, Eq, Ord, Enum)

这将自动把 WeekDay 类型添加到具有这五个名字的类型类中，这些类型类给出的功能是

   show :: WeekDay -> String
   read :: String -> WeekDay
   (==) :: WeekDay -> WeekDay -> Bool
   (<), (>), (<=), (>=) :: WeekDay -> WeekDay -> Bool
   succ, pred :: WeekDay -> WeekDay

在我们采用的教科书中查找这个。注意 show 是 Java 的 toString 的对应物，而 read 做的是相反的事情。一些例子是：

> show Tue
"Tue"
> read "Tue" :: WeekDay  -- (the type annotation tells Haskell to try to parse the string as a WeekDay)
Tue
> read "Dog" :: WeekDay
*** Exception: Prelude.read: no parse
> Mon == Tue
False
> Mon < Tue
True
> succ Mon
Tue
> pred Tue
Mon
> [Mon .. Fri]
[Mon,Tue,Wed,Thu,Fri]

Monday doesn't have a predecessor, and Sunday doesn't have a successor:

> pred Mon
*** Exception: pred{WeekDay}: tried to take `pred' of first tag in enumeration
CallStack (from HasCallStack):
  error, called at data.hs:20:47 in main:Main
> succ Sun
*** Exception: succ{WeekDay}: tried to take `succ' of last tag in enumeration
CallStack (from HasCallStack):
  error, called at data.hs:20:47 in main:Main

请注意，在工作日的类型中，名称的选择是任意的。An equally good, isomorphic definition is

data WeekDay' = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday

一些重要的类型构造函数 Some important type constructors

The Maybe type constructor

有时，一个函数可能无法给出一个结果，在这种情况下，我们希望它能明确地说，它不能。为此，我们使用前奏中的 Maybe 类型：

data Maybe a = Nothing | Just a

这里 a 是一个类型参数，我们对 Nothing 和 Just 有如下类型。

   Nothing :: Maybe a
   Just    :: a -> Maybe a

这意味着构造函数 Just 是一个函数。它转换一个 a 类型的元素为一个 Maybe a 类型的元素。所以这个函数 Just 是一个所谓的 type coercion，也被称为 type cast。

For example:

   Just 17 :: Maybe Integer

总之，Maybe a 类型的唯一可能元素是 Nothing 和 Just x，其中 x 具有 a 类型。

在 Java 中，Maybe 类型的构造函数被称为 Optional。

Example: integer computations that may give errors 可能出现错误的整数计算

在下面的除法定义中，如果分母是 0，那么除法是不可能的，所以结果是 Nothing。如果是可能的，我们就简单地进行除法，我们用类型转换函数 Just 将得到的 Int 转换为 Maybe Int，然后得到函数 dive 的结果：

dive :: Int -> Int -> Maybe Int
x `dive` y = if y == 0 then Nothing else Just (x `div` y)

For example, we get

>10 `dive` 2
Just 5
> 10 `dive` 0
Nothing

But now suppose you want to do 3 + (10 `dive` 0). You would expect Nothing but instead this expression doesn't even type check:

> 3 + (10 `dive` 0)

<interactive>:11:1: error:
    • No instance for (Num (Maybe Int)) arising from a use of '+'
    • In the expression: 3 + (5 `dive` 0)
      In an equation for 'it': it = 3 + (5 `dive` 0)

What this is saying is that (10 `div` 0) is expected to be an Int, because + expects an Int as its right argument, but it isn't. That's because it is a Maybe Int. So we need a version of addition that can cope with errors as its possible inputs:

adde :: Maybe Int -> Maybe Int -> Maybe Int
adde Nothing  Nothing  = Nothing
adde Nothing  (Just y) = Nothing
adde (Just x) Nothing  = Nothing
adde (Just x) (Just y) = Just (x + y)

Now to fix 3 + (5 `dive` 0) we replace + by adde, but also we need to convert the number 3 to the type Maybe Int with the type coercion or type cast Just.

> Just 3 `adde` (10 `dive` 2)
Just 8
> Just 3 `adde` (10 `dive` 0)
Nothing

A more concise definition of adde:

adde' :: Maybe Int -> Maybe Int -> Maybe Int
adde' (Just x) (Just y) = Just (x+y)
adde' _       _         = Nothing

这样做是因为 Haskell 程序的执行从上到下尝试模式，而最后一个模式会抓住所有剩余的可能性。

使用 cases 的定义也是可能的：

adde'' :: Maybe Int -> Maybe Int -> Maybe Int
adde'' xm ym = case xm of
                Nothing -> Nothing
                Just x  -> case ym of
                            Nothing -> Nothing
                            Just y  -> Just (x+y)

稍后我们将看到，有一种更简洁的方法可以使用monads来做这种定义。但现在我们将坚持使用模式匹配和案例。

Example: find the first position an element occurs in a list 找到一个元素在列表中出现的第一个位置

因为如果该元素没有出现在列表中，第一个位置是未定义的，在这种情况下，我们回答 Nothing：

firstPosition :: Eq a => a -> [a] -> Maybe Integer
firstPosition x []     = Nothing
firstPosition x (y:ys)
           | x == y    = Just 0
           | otherwise = case firstPosition x ys of
                           Nothing -> Nothing
                           Just n  -> Just(n+1)

For example:

> firstPosition 'a' ['a'..'z']
Just 0
> firstPosition 'b' ['a'..'z']
Just 1
> firstPosition 'z' ['a'..'z']
Just 25
> firstPosition '!' ['a'..'z']
Nothing

which we summarize as

    firstPosition 'a' ['a'..'z'] = Just 0
    firstPosition 'b' ['a'..'z'] = Just 1
    firstPosition 'z' ['a'..'z'] = Just 25
    firstPosition '!' ['a'..'z'] = Nothing

你需要用书来了解什么是 case，以及它一般是如何工作的，但在这个例子中应该是很清楚的。你还需要用书来了解使用 | 来表示方程的 _ 防护的条件定义。

我们将经常使用 Maybe 类型的构造函数，因为有很多情况下，一些输入是无效的 _。

Task. Define a function allPositions :: Eq a => a -> [a] -> [Int] that finds all positions in which an element element occurs in a list. For example, we should have allPositions 17 [13,17,17,666] = [1,2] and allPositions 17 [1,2,3] = [].

Type retracts

A video discussing this section is available.

以你目前的水平，这一部分可能相当难。把它看作是一个挑战。如果你迷路了，可以在初读时跳过它，进入下一节，以后再回来看。这很重要，因为它涉及到数据编码，这是计算机科学的一个重要方面，甚至是关键方面。我们在这里说的是 Haskell，但实际上它适用于任何编程语言。

我们已经看到了类型同构的例子。例如，Bool 类型与黑白颜色的 BW 类型是同构的，也与二进制数字 Zero 和 One 的 Bit 类型同构。

更一般地说，类型 a 和 b 的同构是一对函数

f :: a -> b
g :: b -> a

such that

• f (g y) = y for all y :: b, and
• g (f x) = x for all x :: a.

我们总结这两个等式时说，这两个函数是互逆的。这意味着我们可以在 a 类型的元素和 b 类型的元素之间来回转换，就像我们把 False 转换为 Zero，把 True 转换为 One 那样。你可以把 f 和 g 看作是重命名函数：函数 f = bit2Bool 把一个位重命名为一个布尔值，函数 g = bool2Bit 把一个布尔值重命名为一个位。

在实践中，这意味着我们是使用元素为 True 和 False 的 Bool 类型，还是使用元素为 Zero 和 One 的 Bit 类型，这并不重要。事实上，计算机的工作是通过用二进制数字对布尔的这种识别来进行的。

类型之间还有一种关系，在实践中也很有用：一个类型 b 可以 "住" 在另一个类型 a 里面，也就是在a里有一个 "副本"。一个简单的例子是，Bool 类型在 Int 类型中拥有一个副本。

bool2Int :: Bool -> Int
bool2Int False = 0
bool2Int True  = 1

我们不仅在 Int 里面有一个 Bool 的副本，而且我们还可以回去，这样我们就可以从 0 和 1 得到 False 和 True。

int2Bool :: Int -> Bool
int2Bool n | n == 0    = False
           | otherwise = True

然而，注意到不仅是 1 被转换回 True，而且除了 0 以外的所有东西都被转换为 True。

我们有

   int2Bool (bool2Int y) = y

for every y :: Bool, but we don't have bool2Int (int2Bool x) = x for all x :: Int, as this fails for e.g. x = 17 because bool2Int (int2Bool 17) is 1 rather than 17.

我们可以说，在整数类型中，有足够的空间让它承载一个布尔类型的副本，但在布尔类型中，没有足够的空间让它承载一个整数类型的副本。

When there are functions

f :: a -> b
g :: b -> a

such that

• f (g y) = y for all y :: b,

但不一定是 g (f x) = x 对于所有 x :: a，我们说 b 类型是 a 类型的retract。

我们上面的讨论表明，Bool 类型是 Int 类型的一个缩减。这种缩减与编程语言 C 中的缩减相同，整数 0 编码为 False，其他都编码为 True。

但是请注意，还有其他的方式可以让 Bool 类型住在 Int 类型里面，作为一个缩进：例如，我们可以把 False送到 13，把 True 送到 17，然后把大于 15 的东西送回 True，把其他东西送到 False。我们可以按照自己的意愿自由编码。

任务. 证明类型 Maybe a 是类型 [a] 的缩减。我们的想法是，Nothing 对应于空列表 []，Just x 对应于单元素列表 [x]。通过在这些类型之间编写来回函数，使其表现出 Maybe a 作为 [a] 的缩进，从而使这一想法变得精确。我们采用的教科书经常利用这种回缩，尽管没有明确说明。事实上，书中经常避免使用 Maybe a 类型，而使用 [a] 类型，只考虑列表 []（对应于无）和单子列表 [x]（对应于 Just x），并忽略长度为 2 或更大的列表。(书中这样做的原因是为了避免单体（在教授它们之前）而支持列表理解（在早期教授），因为在列表单体的特殊情况下，列表理解恰好完成了与单体的 "do notation" 相同的事情。所以在这种情况下，这种编码是为了教学目的而做的）。

如果我们有一个如上所述的类型缩减 (f,g)，那么：

• f is a surjection.

  This means that for every y :: b there is at least one x :: a with f x = y.

  For example, in the case of the booleans as a retract of the integers, this means that every boolean is coded by at least one integer.

• g is an injection.

  This means that for every x :: a there is at most one y :: b with g y = x.

  In the first example of the booleans as a retract of the integers, this is the case:

  • For x = 0 we have exactly one y with bool2Int y = x, namely y=False.
  • For x = 1 we have exactly one y with bool2Int y = x, namely y=True.
  • For x different from 0 and 1 we have no y with bool2Int y = x.

  So for every x there is at most one such y (i.e. exactly one or none).

Task. Define

data WorkingWeekDay = Mon' | Tue' | Wed' | Thu' | Fri'

我们给这些名字加上素数，因为没有素数的名字已经被用作上面定义的 WeekDay 类型的元素。证明 WorkingWeekDay 类型是 WeekDay 类型的缩减。任意选择将需要在一个方向上进行，比如说，语言 C 任意决定除 0 以外的任何整数编码为 true。

Puzzle. Consider the function

g :: Integer -> (Integer -> Bool)
g y = \x -> x == y

We can visualize g in the following table:

	...	-5	-4	...	-1	0	1	...	4	5	...
g(-5)=	...	True	False	...	False	False	False	...	False	False	...
g(-4)=	...	False	True	...	False	False	False	...	False	False	...
...
g(-1)=	...	False	False	...	True	False	False	...	False	False	...
g(0)=	...	False	False	...	False	True	False	...	False	False	...
g(1)=	...	False	False	...	False	False	True	...	False	False	...
...
g(4)=	...	False	False	...	False	False	False	...	True	False	...
g(5)=	...	False	False	...	False	False	False	...	False	True	...

也就是说，函数 g 将整数 y 编码为函数 h，使 h y = True，h x = False，用于 y 以外的 x。让你自己相信，函数 g 是一个注入。在这个意义上，Integer 类型生活在 Integer -> Bool 类型的函数中。你认为 g 有一个同伴 f : (Integer -> Bool) -> Integer，将函数 Integer -> Bool "decodes" 为整数，这样，对于整数 y 的任何代码 g y，我们得到的整数是 f (g y) = y？如果是，请给出这样一个 f 的 Haskell 定义，并说服自己，对于所有的整数 y，f (g y) = y。如果不是，为什么？这个问题相当棘手，"是"或"不是"的可能答案都不明显。

The Either type constructor

A video discussing the next few sections is available on Canvas.

它在序言中的定义如下：

data Either a b = Left a | Right b

Then we have

    Left  :: a -> Either a b
    Right :: b -> Either a b

For example:

    Left 17     :: Either Integer String
    Right "abd" :: Either Integer String

The idea is that the type Either a b is the disjoint union of the types a and b, where we tag the elements of a with Left and those of b with Right in the union type. An example of its use is given below.

The And type constructor, defined by ourselves

下面有一个在语言中预定的同构版本，我们很快就会看到：

data And a b = Both a b

这是一个有两个参数的类型构造函数，并且有一个元素构造函数 Both，它是一个函数

   Both :: a -> b -> And a b

For example, assuming we have defined types MainDish, Dessert, Drink,

data MainDish = Chicken | Pasta | Vegetarian
data Dessert = Cake | IceCream | Fruit
data Drink = Tea | Coffee | Beer

we can define:

type SaverMenu = Either (And MainDish Dessert) (And MainDish Drink)

which can be equivalently written

type SaverMenu = Either (MainDish `And` Dessert) (MainDish `And` Drink)

(Choose which form of definition you like better. Haskell accepts both.)

因此，在节约型菜单中可用的东西要么是一道主菜和一道甜点，要么是一道主菜和一种饮料。直观地讲，这应该是与以下情况同构的

type SaverMenu' = And MainDish (Either Dessert Drink)

意思是说，你可以吃一道主菜，也可以吃甜点或饮料。这一直觉通过同构关系得到了精确的体现

prime :: SaverMenu -> SaverMenu'
prime (Left (Both m d)) = Both m (Left  d)
prime (Right(Both m d)) = Both m (Right d)

unprime :: SaverMenu' -> SaverMenu
unprime (Both m (Left  d)) = Left (Both m d)
unprime (Both m (Right d)) = Right(Both m d)

因此，作为一个软件开发者，你可以选择 SaverMenu 作为你的实现，或者选择 SaverMenu。它们是不同的，但本质上是等同的。

我们实际上不需要定义 And，因为在 Haskell 中已经有了一个相当的类型构造器，即对的类型。我们有一个同构的方法，如下。

and2pair :: And a b -> (a,b)
and2pair (Both x y) = (x,y)

pair2and :: (a,b) -> And a b
pair2and (x,y) = Both x y

于是，我们有了进一步同构的拯救者菜单类型的版本：

type SaverMenu''  = Either (MainDish, Dessert) (MainDish, Drink)
type SaverMenu''' = (MainDish, Either Dessert Drink)

在书中查找对的类型（元组类型）并阅读相关内容。

Lists revisited

A video discussing the next few sections is available on Canvas.

掐指一算，清单的类型是由以下方面预先定义的

data [a] = [] | a : [a]  -- not quite a Haskell definition

它说一个 a 的列表要么是空的，要么是一个 a 类型的元素后面（用 : 表示）有一个 a 的列表。这是一个递归数据类型定义的例子。我们有以下类型的列表构造函数。

    []  :: [a]
    (:) :: a -> [a] -> [a]

尽管上述不完全是 Haskell 的定义在语义上是正确的，但在语法上却是错误的，因为 Haskell（很不幸）不接受这种语法定义。如果我们不关心语法，我们可以这样定义一个同构的版本：

data List a = Nil | Cons a (List a)

Then the types of the constructors are

   Nil  :: List a
   Cons :: a -> List a -> List a

For example, the native list [1,2,3] is written Cons 1 (Cons 2 (Cons 3 Nil)) in our isomorphic version of the type of lists. Let's define the isomorphism to make this clear:

nativelist2ourlist :: [a] -> List a
nativelist2ourlist []     = Nil
nativelist2ourlist (x:xs) = Cons x (nativelist2ourlist xs)

ourlist2nativelist :: List a -> [a]
ourlist2nativelist Nil         = []
ourlist2nativelist (Cons x xs) = x:ourlist2nativelist xs

注意，这些胁迫是递归定义的，与数据类型本身是递归定义的事实相对应。

在列表上实现一些基本操作 Implementing some basic operations on lists

让我们写出我们自己版本的列表连接（"append"）和前奏中的反向操作：

append :: List a -> List a -> List a
append Nil         ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

rev :: List a -> List a
rev Nil         = Nil
rev (Cons x xs) = rev xs `append` (Cons x Nil)

我们可以尝试通过比较它们与 Haskell 前奏中的列表连接和反转的实现来测试这些做法是否正确，使用 List a 和 [a] 之间的同构关系。事实上，我们希望

ourlist2nativelist (append (nativelist2ourlist xs) (nativelist2ourlist ys)) == xs ++ ys

and

ourlist2nativelist (rev (nativelist2ourlist xs)) == reverse xs

对于所有的本地列表 xs, ys :: [a] 应评估为 True。让我们测试一下这些属性：

> let xs = [1..5]
> let ys = [6..10]
> ourlist2nativelist (append (nativelist2ourlist xs) (nativelist2ourlist ys)) == xs ++ ys
True
> ourlist2nativelist (rev (nativelist2ourlist xs)) == reverse xs
True

当然，这里我们只在几个例子上做了测试，但一般来说是真的。(问题：你将如何证明这一点？)

尽管我们的定义在功能上是正确的，但我们对 rev 的实现存在一个更微妙的问题。通过检查代码，append xs ys 在 O(n) 时间内计算两个列表的连接，其中 n 是 xs 的长度，因为对 append 的每个递归调用都使 xs 的长度减少一个，而对 Cons 的调用是恒定时间。另一方面，根据同样的论点，rev 是 O(n²)，因为对 rev 的每个递归调用都会使 xs 的长度减少一个，而对 append 的每个调用都是 O(n)。

这不仅仅是一个理论上的问题，如果我们比较一下使用原生的 reverse 函数和上面的实现 rev 来反转一个合理的大列表，我们很快就会发现这个问题。

> let xs = [1..10^5]
> length (reverse xs)  -- this is fast (we return the length of the reversed list in order to keep the output small)
100000
> length (ourlist2nativelist (rev (nativelist2ourlist xs)))  -- this is really slow, so we give up and hit Control-C
  C-c C-cInterrupted.

有一个更有效的方法来实现反转，即引入一个带有额外参数的辅助函数：

fastrev :: List a -> List a
fastrev xs = revapp xs Nil
  where
    revapp :: List a -> List a -> List a
    revapp (Cons x xs) ys = revapp xs (Cons x ys)
    revapp Nil         ys = ys

可以把辅助函数 revapp 的第二个参数看成是一个堆栈，最初设置为空（Nil）。该函数递归地扫描来自第一个参数的输入，将每个元素推到堆栈（第二个参数）。当没有更多的输入元素时，堆栈被直接弹出到输出端，原始列表中的所有元素现在都是相反的顺序。

下面是一个关于如何工作的具体说明，展开 fastrev 和 revapp 的定义来反转一个四元素列表：

  fastrev (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))
= revapp (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))) Nil
= revapp (Cons 2 (Cons 3 (Cons 4 Nil))) (Cons 1 Nil)
= revapp (Cons 3 (Cons 4 Nil)) (Cons 2 (Cons 1 Nil))
= revapp (Cons 4 Nil) (Cons 3 (Cons 2 (Cons 1 Nil)))
= revapp Nil (Cons 4 (Cons 3 (Cons 2 (Cons 1 Nil))))
= Cons 4 (Cons 3 (Cons 2 (Cons 1 Nil)))

另一种思考函数 revapp 的方式是由它的名字提示的：给定两个列表 xs 和 ys，我们有 revapp xs ys 计算xs的反转 _ 与ys相加。不难看出，这个二元操作 revapp 比原来的一元反转操作更通用：后者可以通过取 ys = Nil 来恢复。另一方面，revapp 比我们原来的函数 rev 更有效率，它的第一个参数 xs 的长度只有 O(n)。

这种模式我们设法解决一个问题或通过用一个更普遍的、看起来更困难的问题来解决它在函数式编程中一次又一次地发生。

An aside on accumulators

我们在辅助函数 revapp 中使用的额外参数 ys 有时被称为 "累加器"，因为它累加了一个最终传递给输出的值。上面我们看到一个累加器是如何被用来把一个 O(n²) 的算法变成一个 O(n) 的列表反转算法的。对于一个更鲜明的例子，考虑计算斐波那契数 Fₙ 的问题。

维基百科中关于斐波那契数列的数学定义可以直接翻译成以下 Haskell 代码：

fib 0 = 0
fib 1 = 1
fib n = fib (n-1) + fib (n-2)

但是，尽管这个定义是正确的，但它的效率却极其低下!

如果我们尝试使用上述定义来计算，比如说前 32 个斐波那契数，我们已经可以看到这一点：

> :set +s -- ask ghci to print time and space usage
> [fib n | n <- [0..31]]
[0,1,1,2,3,5,8,13,21,34,55,89,144,233,377,610,987,1597,2584,4181,6765,10946,17711,28657,46368,75025,121393,196418,317811,514229,832040,1346269]
(10.23 secs, 4,086,282,024 bytes)

十多秒就能计算出 32 个斐波那契数!

事实上，fib n的运行时间大约是 O(2ⁿ)，因为递归情况下对 fib 进行了两次调用，而 n 只减少了 1 或 2。

这里有一个替代方案，使用一对累加器 x 和 y 来实现，效率更高：

fastfib n = fibAcc n 0 1
  where
    fibAcc 0 x y = x
    fibAcc 1 x y = y
    fibAcc n x y = fibAcc (n-1) y (x+y)

通过这种实现方式，我们在计算上没有任何问题，比如说，在几分之一秒内计算出前 100 个斐波那契数：

> [fastfib n | n <- [0..99]]
[0,1,1,2,3,5,8,13,21,34,55,89,144,233,377,610,987,1597,2584,4181,6765,10946,17711,28657,46368,75025,121393,196418,317811,514229,832040,1346269,2178309,3524578,5702887,9227465,14930352,24157817,39088169,63245986,102334155,165580141,267914296,433494437,701408733,1134903170,1836311903,2971215073,4807526976,7778742049,12586269025,20365011074,32951280099,53316291173,86267571272,139583862445,225851433717,365435296162,591286729879,956722026041,1548008755920,2504730781961,4052739537881,6557470319842,10610209857723,17167680177565,27777890035288,44945570212853,72723460248141,117669030460994,190392490709135,308061521170129,498454011879264,806515533049393,1304969544928657,2111485077978050,3416454622906707,5527939700884757,8944394323791464,14472334024676221,23416728348467685,37889062373143906,61305790721611591,99194853094755497,160500643816367088,259695496911122585,420196140727489673,679891637638612258,1100087778366101931,1779979416004714189,2880067194370816120,4660046610375530309,7540113804746346429,12200160415121876738,19740274219868223167,31940434634990099905,51680708854858323072,83621143489848422977,135301852344706746049,218922995834555169026]
(0.02 secs, 3,057,552 bytes)

同样，为了看清发生了什么，在一个具体的例子上展开定义是有帮助的：

  fastfib 7
= fibAcc 7 0 1
= fibAcc 6 1 1
= fibAcc 5 1 2
= fibAcc 4 2 3
= fibAcc 3 3 5
= fibAcc 2 5 8
= fibAcc 1 8 13
= 13

我们可以看到，这个使用一对累加器参数 x 和 y 的斐波那契数的功能实现，与人们在 Java 中计算斐波那契数的方式非常相似，都是在一个循环中更新一对变量 x 和 y：

static int fastfib(int n) {
  int x = 0, y = 1;
  while (n > 1) {
     int z = x+y;
     x = y;
     y = z;
     n = n-1;
  }
  return (n == 0 ? x : y);
}

除了对 fastfib 和 fibAcc 所做的事情的低层次看法外，还有一个更高层次的看法（正如我们之前在 revapp 的例子中看到的）。你能确定辅助函数 fibAcc n x y 在何种意义上比 fib n 计算了一个更普遍的函数吗？

Binary trees

A video discussing the next few sections is available on Canvas .

一个二叉树在一个类型 a 的元素上要么是空的，要么由一个根标记的 a 类型的元素组成，后面有两个二叉树，称为左子树和右子树：

data BT a = Empty | Fork a (BT a) (BT a)

• We have the empty tree, to be called Empty. We take the convention that empty trees are drawn as dangling leaves.

                              |

• Given two trees l and r and an element x::a, we have the new tree

                              x
                             / \
                            /   \
                           l     r

  written Fork x l r.

For example, the tree

                             8
                            / \
                           /   \
                          4     16
                         / \   / \
                        2        20
                       / \      /  \

is written, in this notation, as

btexample = Fork 8 (Fork 4 (Fork 2 Empty Empty) Empty) (Fork 16 Empty (Fork 20 Empty Empty))

我们可以要求 Haskell 通过如上派生的方式为我们做一些工作。

data BT a = Empty
          | Fork a (BT a) (BT a) deriving (Show, Read, Eq, Ord)

We have that

   Empty :: BT a
   Fork  :: a -> BT a -> BT a -> BT a

Puzzle. It should be clear what the automatically derived Show, Read and Eq do. But what do you think the order on trees derived with Ord should be? Hint. This is a non-trivial question. So examine it first for the type of lists. In that case, the automatically derived order is the lexicographic order, which is like the dictionary order.

Basic functions on binary trees

为了开始，让我们对树进行镜像，这样，例如从上面我们可以得到

                             8
                            / \
                           /   \
                          16    4
                         / \   / \
                        20        2
                       / \       / \

We do this as follows:

mirror :: BT a -> BT a
mirror Empty = Empty
mirror (Fork x l r) = Fork x (mirror r) (mirror l)

Running this on the above example we get

mirror btexample = Fork 8 (Fork 16 (Fork 20 Empty Empty) Empty) (Fork 4 Empty (Fork 2 Empty Empty))

This notation for trees is not very good for visualizing them, as you can see, but is very good for computation.

We define the size of a tree as its total number of nodes:

size :: BT a -> Integer
size Empty        = 0
size (Fork x l r) = 1 + size l + size r

由于我们考虑的是二叉树，其大小（即节点数）也等于叶子数减一：

leaves :: BT a -> Integer
leaves Empty        = 1
leaves (Fork x l r) = leaves l + leaves r

我们将树的高度定义为从根部开始的最长路径的长度，以节点数衡量：

height :: BT a -> Integer
height Empty        = 0
height (Fork x l r) = 1 + max (height l) (height r)

一个平衡的二叉树的高度大约是其大小的对数，而一个非常不平衡的二叉树，如

                            20
                           / \
                          16
                         / \
                        8
                       / \
                      4
                     / \
                    2
                   / \

btleft = Fork 20 (Fork 16 (Fork 8 (Fork 4 (Fork 2 Empty Empty) Empty) Empty) Empty) Empty

has height approximately equal to its size.

二叉树中的方向、地址和路径 Directions, addresses and paths in binary trees

A video discussing the next few sections is available on Canvas.

为了挑选二叉树的子树，我们依次向左或向右走，直到找到它。但是可能会给出一个错误的方向列表，这里称为地址，因此我们需要 Maybe 类型的输出。

data Direction = L | R deriving (Show)
type Address   = [Direction]

subtree :: Address -> BT a -> Maybe(BT a)
subtree []     t            = Just t
subtree (_:_)  Empty        = Nothing
subtree (L:ds) (Fork _ l _) = subtree ds l
subtree (R:ds) (Fork _ _ r) = subtree ds r

按照上述模式，我们可以定义一个函数来检查给定树中的地址是否有效：

isValid :: Address -> BT a -> Bool
isValid []     _            = True
isValid (_:_)  Empty        = False
isValid (L:ds) (Fork _ l _) = isValid ds l
isValid (R:ds) (Fork _ _ r) = isValid ds r

子树的有效地址列表可按如下方式计算：

validAddresses :: BT a -> [Address]
validAddresses Empty        = [[]]
validAddresses (Fork _ l r) = [[]]
                           ++ [L:ds | ds <- validAddresses l]
                           ++ [R:ds | ds <- validAddresses r]

列表理解总是可以被消除的。在这个例子中，它们变成了

validAddresses' :: BT a -> [Address]
validAddresses' Empty        = [[]]
validAddresses' (Fork _ l r) = [[]]
                            ++ (map (L:) (validAddresses' l))
                            ++ (map (R:) (validAddresses' r))

We expect that

    isValid ds t = ds `elem` (validAddresses t)

或者，换句话说，一个地址是有效的，当且仅当它是有效地址列表的一个元素。这在直觉上应该是很清楚的吧？语句，是的。但是，鉴于我们的定义，我认为事实并非如此。我想说，这需要一个令人信服的论证。在任何情况下，直觉是我们根据所学的令人信服的论证而形成的。

从根到叶的所有路径的列表有一个类似的定义：

btpaths :: BT a -> [[a]]
btpaths Empty        = [[]]
btpaths (Fork x l r) = [x:xs | xs <- btpaths l]
                    ++ [x:xs | xs <- btpaths r]

Proofs on binary trees by induction

If we have a property P of trees, and we want to show that P(t) holds for all trees t, we can do this by induction on trees as follows:

• Argue that P(Empty) holds.
• Argue that if P(l) and P(r) hold for given trees l and r, then it holds for P(Fork x l r) where x is arbitrary.

We are not going to emphasize proofs in this module, but we will indicate when some claims genuinely require proofs, and, moreover, we will try to be precise regarding the specifications of the programs we write.

经常有这样的情况，有人向我们展示了一个聪明的算法，我们感到很愚蠢，因为我们不理解它。但这种感觉是错误的。如果我们不理解一个算法，缺少的是一个证明。证明是一种解释。这就是证明的含义。为了理解一个算法，我们需要

• the algorithm itself,
• a precise description of what it is intended to do, and
• a convincing explanation that the algorithm does do what it is intended to do.

仅有方案是不够的。我们需要知道它们的目的是什么，而且我们想知道一个解释，证明它们完成了我们所承诺的。这个承诺被称为算法/程序的规范性。程序的正确性意味着 "承诺得到了实现"。试图证明承诺被实现的一种方法是对程序进行测试。但实际上，测试所能做的就是通过寻找反例来证明承诺没有被实现。当好的例子起作用时，我们就有某种证据证明该算法起作用了，但不是完全的信心，因为我们可能遗漏了那些给出错误输出的输入例子。只有通过令人信服的解释，也就是所谓的 proof，才能给予充分的信心。如果你曾经问过自己 "证明" 的真正含义，最终的答案是 "令人信服的论证"。

职能证明 Functional proofs

依赖类型语言Agda允许编写函数式程序和其正确性证明，其中证明本身被写成函数式程序。作为一个例子，这里有一个经过计算机检验的证明，即 Agda 中函数 isValid 和 validAddresses 之间的上述关系。这一点是不可考的，在此仅作说明之用。

二叉树中的遍历 Traversals in binary trees

A video discussing the next few sections is available on Canvas.

我们现在定义标准的内序和前序 traversals。

treeInOrder :: BT a -> [a]
treeInOrder Empty = []
treeInOrder (Fork x l r) = treeInOrder l ++ [x] ++ treeInOrder r

treePreOrder :: BT a -> [a]
treePreOrder Empty = []
treePreOrder (Fork x l r) = [x] ++ treePreOrder l ++ treePreOrder r

For instance, for the trees btexample and btleft considered above,

                             8
                            / \
     btexample =           /   \
                          4     16
                         / \   / \
                        2        20
                       / \      /  \

                            20
                           / \
                          16
                         / \
        btleft =        8
                       / \
                      4
                     / \
                    2
                   / \

we get:

> (treeInOrder btexample, treePreOrder btexample)
([2,4,8,16,20],[8,4,2,16,20])
> (treeInOrder btleft, treePreOrder btleft)
([2,4,8,16,20],[20,16,8,4,2])

广度优先遍历是比较棘手的。我们首先定义一个函数，给定一棵树，产生一个列表，其中有零层的节点（只是根），然后是第一层的节点（根的继承者），然后是第二层的节点，以此类推：

levels :: BT a -> [[a]]
levels Empty        = []
levels (Fork x l r) = [[x]] ++ zipappend (levels l) (levels r)
  where
    zipappend []       yss      = yss
    zipappend xss      []       = xss
    zipappend (xs:xss) (ys:yss) = (xs ++ ys) : zipappend xss yss

(Compare zipappend to the prelude function zipWith.) For example:

> levels btexample
[[8],[4,16],[2,20]]
> levels btleft
[[20],[16],[8],[4],[2]]

With this we can define

treeBreadthFirst :: BT a -> [a]
treeBreadthFirst = concat . levels

其中 . 代表函数组合（在我们的教科书中查找），序言函数 concat :: [[a]] -> [a] 连接一个列表。-> 连接一个列表，例如从 [[8],[4,16],[2,20] 得到 [8,4,16],[2,20]。关于广度优先搜索的进一步讨论，请参见被低估的 unfold（免费版本在作者的网页），但这对你们中的大多数人来说可能超出了你们目前的水平。

反转遍历（生成树）Inverting traversals (generating trees)

A video discussing the next few sections is available on Canvas.

许多不同的树可以有相同的（内序/前序/宽度优先）遍历，正如我们在上面看到的 btexample 和 btleft，它们有相同的内序遍历。换句话说，所有的函数

treeInOrder, treePreOrder, treeBreadthFirst :: BT a -> [a]

是非注入性的，因此是不可逆转的。尽管如此，一个有趣的、可操作的问题是尝试用给定的（内序/前序/宽度优先）遍历法构建二叉树，或者甚至用给定的遍历法生成所有可能的二叉树。

作为一个例子，下面将产生一个平衡的二叉树，给定其内序遍历（如果输入被排序，将是一个二叉搜索树）。

balancedTree :: [a] -> BT a
balancedTree [] = Empty
balancedTree xs = let (ys, x:zs) = splitAt (length xs `div` 2) xs in
                  Fork x (balancedTree ys) (balancedTree zs)

(前奏函数 splitAt 在给定的位置将一个列表分成两个列表)。这满足了以下公式

    treeInOrder (balancedTree xs) = xs

for all xs :: [a]. 在另一个方向，肯定不是的情况，即

    balancedTree (treeInOrder t) = t

for all t :: Bin a, for instance

balancedTree (treeInOrder btleft) = Fork 8 (Fork 4 (Fork 2 Empty Empty) Empty) (Fork 20 (Fork 16 Empty Empty) Empty)

which is not equal to btleft. 事实上，复合函数

balance :: BT a -> BT a
balance = balancedTree . treeInOrder

将 treeInOrder 应用于一棵树，然后将 balancedTree 应用于产生的列表，可以看作是对二叉树进行再平衡的操作。

现在，使用列表理解法，从上面的函数 balancedTree 到生成所有二叉树的函数，只需一小步，就能实现给定的内序遍历。

inOrderTree :: [a] -> [BT a]
inOrderTree [] = [Empty]
inOrderTree xs = [Fork x l r | i <- [0..length xs-1],
                               let (ys, x:zs) = splitAt i xs,
                               l <- inOrderTree ys, r <- inOrderTree zs]

这满足了以下属性

elem t (inOrderTree xs)

if and only if

treeInOrder t = xs

for all t :: BT a and xs :: [a]. For example, running

> inOrderTree [1..3]
[Fork 1 Empty (Fork 2 Empty (Fork 3 Empty Empty)),Fork 1 Empty (Fork 3 (Fork 2 Empty Empty) Empty),Fork 2 (Fork 1 Empty Empty) (Fork 3 Empty Empty),Fork 3 (Fork 1 Empty (Fork 2 Empty Empty)) Empty,Fork 3 (Fork 2 (Fork 1 Empty Empty) Empty) Empty]

成功计算出所有五棵二进制搜索树，其内序遍历为[1,2,3]：

   1
  / \
     2
    / \
       3
      / \
Fork 1 Empty (Fork 2 Empty (Fork 3 Empty Empty))

   1
  / \
     3
    / \
   2
  / \
Fork 1 Empty (Fork 3 (Fork 2 Empty Empty) Empty)

     2
    / \
   /   \
  1     3
 / \   / \
Fork 2 (Fork 1 Empty Empty) (Fork 3 Empty Empty)

    3
   / \
  1
 / \
    2
   / \
Fork 3 (Fork 1 Empty (Fork 2 Empty Empty)) Empty

      3
     / \
    2
   / \
  1
 / \
Fork 3 (Fork 2 (Fork 1 Empty Empty) Empty) Empty

任务：编写一个函数 preOrderTree :: [a] -> [BT a]，其属性为 elem t (preOrderTree xs)，当且仅当 treePreOrder t = xs 为所有 t :: Bin a和xs ::[a].

非常困难的任务：写一个函数 breadthFirstTree :: [a] -> [BT a]，其属性为 elem t (breadthFirstTree xs)，当且仅当 treeBreadthFirst t = xs 为所有 t :: Bin a和xs :: [a]. 解决方案)