Plutus 例子（TODO）

这里，我们看看一些常见的程序示例，让您更好地了解 Plutus 语言的工作原理。我们将实现 Peano 数字类型，cons 列表，二叉树，以及一些相关的常见功能。

首先，让我们定义 Peano 数字类型

data Nat = { Zero | Suc Nat }

（Peano）数字类型支持各种功能，当然有加法，乘法，阶乘和斐波那契这些，这些是程序的典型例子。

add : Nat -> Nat -> Nat {
  add Zero n = n ;
  add (Suc m) n = Suc (add m n)
}

mul : Nat -> Nat -> Nat {
  mul Zero _ = Zero ;
  mul (Suc m) n = add (mul m n) n
}

fac : Nat -> Nat {
  fac Zero = Suc Zero ;
  fac (Suc n) = mul (Suc n) (fac n)
}

fib : Nat -> Nat {
  fib Zero = Suc Zero ;
  fib (Suc Zero) = Suc Zero ;
  fib (Suc (Suc n)) = add (fib n) (fib (Suc n))
}

Cons 列表也是一种熟悉的类型：

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

这演示了参数类型的使用，其中 List a 有具有 a 元素类型的类型参数。举个例子，List Nat 是 Peano 数字类型的列表。

列表支持各种功能，例如 length, append 和 map:

length : forall a. List a -> Nat {
  length Nil = Zero ;
  length (Cons _ xs) = Suc (length xs)
}

append : forall a. List a -> List a -> List a {
  append Nil ys = ys ;
  append (Cons x xs) ys = Cons x (append xs ys)
}

map : forall a b. (a -> b) -> List a -> List b {
  map _ Nil = Nil ;
  map f (Cons x xs) = Cons (f x) (map f xs)
}

这里我们可以看到 Plutus 使用多态原则，这些函数适用于任何列表，不管元素类型如何，所以我们可以通过使用元素类型来抽象 forall。例如，length 对于任何 a，我们都有类型函数 List a -> Nat。

需要重点注意的是，在 Plutus 中，这个多态只存在于值的声明中，你在任何时候使用一个多态声明的值，类型变量的选择必须在 use site 固定。一般来说，你不能像在 System-F 中那样将这些声明视为给出多态值。相反，声明中的多态类型是相同定义的 infinite 家族的缩写，只在该类型变量的选择上有所不同。例如，我们可以像这样定义多个 length 函数。

lengthNat : List Nat -> Nat {
  lengthNat Nil = Zero ;
  lengthNat (Cons _ xs) = Suc (lengthNat xs)
}

lengthBool : List Bool -> Nat {
  lengtBool Nil = Zero ;
  lengthBool (Cons _ xs) = Suc (lengthBool xs)
}

lengthListNat : List (List Nat) -> Nat {
  lengthListNat Nil = Zero ;
  lengthListNat (Cons _ xs) = Suc (lengthListNat xs)
}

除了名字和 a 的不同外，它们都是相同的 a。这当然是多余的，所以我们可以使用上面给出的多态声明。但这个声明没有给我们具有 forall a. List a -> Nat 类型的值 length。相反，他给了我们整个 infinite 家族的定义，但有一个方便的缩写语法。这就是为什么使用这个多态声明需要在 use site 固定类型变量。

另一种常见的类型是在分支中有数据的二叉树类型：

data Tree a = { Leaf | Branch a (Tree a) (Tree a) }

这样的树支持 count, traversal 和 reverse 的功能：

count : forall a. Tree a -> Nat {
  count Leaf = Zero ;
  count (Branch _ l r) = Suc (add (count l) (count r))
}

traversal : forall a. Tree a -> List a {
  traversal Leaf = Nil ;
  traversal (Branch x l r) = Cons x (append (traversal l) (traversal r))
}

reverse : forall a. Tree a -> Tree a {
  reverse Leaf = Leaf ;
  reverse (Branch x l r) = Branch x (reverse r) (reverse l)
}