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