Plutus 类型

本章包括了关于 Plutus 语言类型的参考。它使用了一些非正式的类型理论,希望对于阅读这个文件的每个人都易于理解。

Plutus 有一些内置类型(int, float, bytestrings) 和一个内置的类型操作符(functions)。其他类型由程序的作者定义,我们将一次讨论每一种类型。

Ints, Floats 和 Byte Strings

Int, FloatByteString 是原始类型,具有由一下语法指定的常量给出的构造函数形式。

<int> ::= "-"? <digit>+
<float> ::= "-"? <digit>+ <fractExponent>
<digit> = "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
<fractExponent> ::= <fraction> <exponent>? | <exponent>
<fraction> ::= "." <digit>+
<exponent> ::= ("e" | "E") ("-" | "+") <digit>+

<bytestring> ::= "#" <byte>*
<byte> ::= <nybble> <nybble>
<nybble> ::= <digit>
           | "a" | "b" | "c" | "d" | "e" | "f"
           | "A" | "B" | "C" | "D" | "E" | "F"

这些类型没有真正的 eliminator 形式,但是有一些内置操作可以应用于这些类型。我们编写的内置签名如下:f : (A,B) ⇀ C,表示 一个内置的名字 f 可以被应用于一个 A 和一个 B 产生一个 C。这些原始类型的内置函数如下,用 Haskell 函数实现:

addInt : (Int,Int) ⇀ Int
  implemented as `(+) :: Int -> Int -> Int`

subtractInt : (Int,Int) ⇀ Int
  implemented as `(-) :: Int -> Int -> Int`

multiplyInt : (Int,Int) ⇀ Int
  implemented as `(*) :: Int -> Int -> Int`

divideInt : (Int,Int) ⇀ Int
  implemented as `div :: Int -> Int -> Int`

remainderInt : (Int,Int) ⇀ Int
  implemented as `(%) :: Int -> Int -> Int`

lessThanInt : (Int,Int) ⇀ Bool
  implemented as `(<) :: Int -> Int -> Bool`

equalsInt : (Int,Int) ⇀ Bool
  implemented as `(==) :: Int -> Int -> Bool`

intToFloat : (Int) ⇀ Float
  implemented as `fromInteger . toInteger :: Int -> Float`

intToByteString : (Int) ⇀ ByteString
  implemented as `encode :: Int -> ByteString`

addFloat : (Float,Float) ⇀ Float
  implemented as `(+) :: Float -> Float -> Float`

subtractFloat : (Float,Float) ⇀ Float
  implemented as `(-) :: Float -> Float -> Float`

multiplyFloat : (Float,Float) ⇀ Float
  implemented as `(*) :: Float -> Float -> Float`

divideFloat : (Float,Float) ⇀ Float
  implemented as `(/) :: Float -> Float -> Float`

lessThanFloat : (Float,Float) ⇀ Bool
  implemented as `(<) :: Float -> Float -> Bool`

equalsFloat : (Float,Float) ⇀ Bool
  implemented as `(==) :: Float -> Float -> Bool`

ceiling : (Float) ⇀ Float
  implemented as `ceiling:: Float -> Float`

floor : (Float) ⇀ Float
  implemented as `floor :: Float -> Float`

round : (Float) ⇀ Float
  implemented as `round :: Float -> Float`

concatenate : (ByteString,ByteString) ⇀ ByteString
  implemented via `concat :: [ByteString] -> ByteString`

drop : (Int,ByteString) ⇀ ByteString
  implemented via `drop :: Integer -> ByteString -> ByteString`

take : (Int,ByteString) ⇀ ByteString
  implemented via `take :: Integer -> ByteString -> ByteString`

sha2_256 : (ByteString) ⇀ ByteString
  implemented via `hash : [Char8] -> Digest SHA256`

sha3_256 : (ByteString) ⇀ ByteString
  implemented via `hash : [Char8] -> Digest SHA3_256`

equalsByteString : (ByteString,ByteString) ⇀ Bool
  implemented as `(==) :: ByteString -> ByteString -> Bool`

通过在名称前加上前缀 !,将其完全加上参数,使用这些内置函数。例如,加2和3就是 !addInt 2 3

函数类型

给定任意 AB 类型,有一种函数类型 A -> B。要获得这种类型,我们可以使用 lambada 的形式,如下所述:如果 M 有类型 B,有一个变量类型为 A 的变量 x,那么 \x -> M 有类型 A -> B。我们可以使用一个具有函数类型的术语:如果 M 有类型 A -> BN 有类型 AM N 有类型 B。函数的计算是标准的 beta 递减:(\x -> M) N[N/x]M,即 MN 取代 x。在 Plutus 中,计算是立即执行的,因此 N 在替换之前获得结果。(TODO)

用户声明的类型

例如,当用户声明新的数据类型时

data Foo a = { Bar | Baz a }

这定义了一个新的类型构造函数,在这种情况下 Foo 具有以下推理规则:给定任意类型 A, Foo A 也是一种类型。

它也带有构造函数的推理规则,如下:BarFoo A 类型,对于 A 的任意选项,如果 M 有类型 A, 那么 Baz M 也有类型 Foo A

用户声明类型的 eliminator 表单是 case 结构,用于所有类型。案例分析和 Haskell 一样,例如我们可以写做

case foo of { Bar -> 0 | Baz x -> x }

分析 Foo Int 元素的类型,需计算 Int。与 Haskell 有一点不同:我们可以同时分析多个 term,将他们(及其相应的模式)以 | 分割:

case foo0 | foo1 of { Bar | Bar -> 0 ; Baz x | Baz y -> !addInt x y }

案例分析不是必须的。也就是说,可能会有缺失的模式。任何失败的匹配都会导致整个程序运行失败,并导致事务被视为无效。

Int, FloatByteString 也可以为模式;例如,我们可以这种方式来定义阶乘函数:

facInt : Int -> Int {
  facInt n = case n of {
    0 -> 1 ;
    _ -> !multiplyInt n (!subtractInt n 1)
  }
}