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, appendmap:

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, traversalreverse 的功能:

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)
}