代数数据类型.md

代数数据类型（ADT）

代数数据类型是复合类型，通常用于函数式编程。Scilla中包含以下ADT：每个ADT都被定义为一组构造函数。每个构造函数都采用固定类型的参数集。

布尔（Boolean）

使用Bool指定布尔值。BoolADT有两个构造函数：True并且False，无需带任何参数。因此，以下代码构造了一个表达为True的BoolADT ：

x = True

Option

与OCaml中的Option类似，Scilla中的OptionADT表示值x是否存在。Option 有两个构造函数None和Some。

• Some表示值存在。

  Some {'A} x构造一个表示存在类型为'A的值x的ADT 。以下代码用Some构造了一个带Int32类型参数的Option：

  x = Some {Int32} 10

• None代表没有任何值。

  None {'A}构造了一个表示没有类型为'A的值的ADT 。以下代码使用None构造了一个带Hash类型参数的Option ：

  x = None {Hash}

列表（List）

类似于其他函数式编程语言，ListADT提供了一种包含相同类型值的列表。 用List创建列表，其包含两个构造函数：

• Nil创造一个空List。它采用以下形式：Nil {'A}，并创建一个'A类型的空列表。
• Cons向现有列表添加元素。它采用以下形式：Cons {'A} h l 。'A是一个可以实例化任何类型的类型变量，h是在List 'A类型列表l头部的'A类型元素。

以下示例代码演示了如何构建Int32值列表。首先，我们先创建一个空列表Nil {Int32}。然后往列表插入列表项。最终构建的列表为[11 -> 10 -> 2 -> 1 -> NIL]。

let one = Int32 1 in
let two = Int32 2 in
let ten = Int32 10 in
let eleven = Int32 11 in

let nil = Nil {Int32} in
let l1 = Cons {Int32} one nil in
let l2 = Cons {Int32} two l1 in
let l3 = Cons {Int32} ten l2 in
  Cons {Int32} eleven l3

List提供了以下两种递归结构原函数。

• list_foldl: ('B -> 'A -> 'B) -> 'B -> (List 'A) -> 'B：对于任意类型的'A和'B，list_foldl通过应用迭代器'B -> 'A -> 'B函数，针对其中的元素及累加器'B，从左至右对List 'A进行递归处理。此累加器的初始值将成为list_foldl的参数。
• list_foldr: ('A -> 'B -> 'B) -> 'B -> (List 'A) -> 'B：与list_foldl处理方式基本一致，只不过是从右到左进行处理。

为了进一步说明List，我们展示了一个可以计算列表元素数量的例子list_foldl 。

let list_length =
  tfun 'A =>
  fun (l : List 'A) =>
    let folder = @list_foldl 'A Int32 in
    let init = Int32 0 in
    let iter =
      fun (h : 'A) =>
      fun (z : Int32) =>
        let one = Int32 1 in
          builtin add one z
     in
       folder iter init l

list_length定义一个函数，它接受一个List 'A类型的参数l，其中'A是参数类型（类型变量），参阅line 2。我们在line 4用类型为Int32的累加器实例化了'A类型的list_foldl列表。累加器初始值为0。每次列表l中每个元素的调用，都会使迭代器函数iter增加累加器。累加器的最终值将等于增量，即列表中的元素数量。

Scilla标准库中，``ListUtils库提供了常用的List`控件（包括`list_length`）。

Pair

PairADT用于包含不同类型的一对值。Pair变量是使用Pair指定的，并用Pair {'A 'B} a b来构造。其中'A和'B是类型变量，可被实例化到任意类型，a和b分别是'A和'B类型的变量。

下面是构造Int32类型值的Pair的示例。

let one = 1 in
let two = 2 in
let p = Pair {Int32 Int32} one two in
  ...

现在来说明下如何从Pair中提取第一个元素。下面的fst是Scilla标准库中的PairUtils已定义好的函数。

let fst =
  tfun 'A =>
  fun (p : Pair 'A 'A) =>
  match p with
  | Pair {'A 'A} a b =>
      a
  end

let p = Pair {Int32 Int32} one two in
let fst_int = @fst Int32 in
let a = fst_int p in
  ... (* a = one *) ...

Nat

Scilla提供了一个ADT来处理自然数。自然数Nat定义为Zero或Succ Nat（即自然数继承）。下面展示了一个OCaml中的Nat的定义：

type nat = Zero | Succ of nat

下面的折叠（结构递归）定义了Scilla的Nat ，其中'T是参数类型变量。

nat_fold : ('T -> Nat -> 'T) -> 'T -> Nat -> 'T

与List前面描述的折叠类似，Nat 折叠采用了一种初始化累加器（类型'T）、一个将Nat作为参数的函数和一种中间累加器（'T）的函数，并返回新的累加器值。这个迭代器函数类型为'T -> Nat -> 'T 。折叠遍历了所有自然数，执行迭代器函数后返回一个最终累加器。

更多ADT示例

为了更易理解如何使用ADT，我们将详细介绍两个示例。下面描述的两个函数都在Scilla标准库的ListUtils中。

列表：头部

下面的代码将提取List的第一项并将结果作为Option类型返回，即如果列表至少有一个元素则返回Some，否则返回None。这个测试用例输入了[ 1 -> 2 -> 3 -> NIL]并返回1。

let list_head =
  tfun 'A =>
  fun (l : List 'A) =>
    match l with
    | Cons h t =>
      Some h
    | Nil =>
      None
    end
in

let int_head = @list_head Int32 in

let one = Int32 1 in
let two = Int32 2 in
let three = Int32 3 in
let nil = Nil {Int32} in

let l1 = Cons {Int32} three nil in
let l2 = Cons {Int32} two l1 in
let l3 = Cons {Int32} one l2 in
int_head l3

在lines 14-21我们构建一个可以向list_head函数输入的列表。Line 12实例化含Int32类型的list_head函数，最后一行调用了实例化的list_head函数。

在line 2 tfun 'A指定了'A是函数的参数类型/变量，而line 3的fun指定l是List 'A类型的参数。也就是说，在lines 1-3中 我们指定一个list_head函数，这个函数可以为任意'A类型实例化并将其作为List 'A类型变量的参数。如果在line 5中匹配到了一个用Cons h t构造的List列表，其中h是列表头部，t是列表结尾，则会返回Some h作为列表头部。如果列表为空，则它在line 7匹配到了Nil并返回None，表示列表没有头部。

列表：存在

现在来描述一个函数，它给出了一个列表和一个断言函数。如果断言适用于列表的至少一个元素，则返回True。

let list_exists =
  tfun 'A =>
  fun (f : 'A -> Bool) =>
  fun (l : List 'A) =>
    let folder = @list_foldl 'A Bool in
    let init = False in
    let iter =
      fun (z : Bool) =>
      fun (h : 'A) =>
        let res = f h in
        match res with
        | True =>
          True
        | False =>
          z
        end
    in
      folder iter init l

let int_exists = @list_exists Int128 in
let f =
  fun (a : Int128) =>
    let three = Int128 3 in
    builtin lt a three

...
(* build list l3 similar to previous example *)
...

(* check if l3 has at least one element satisfying f *)
int_exists f l3

与前面的示例类似，'A是函数的一个类型变量。该函数接受两个参数：List 'A类型的列表l 和断言，即获取一个'A类型的列表元素并返回True或False，这表示了断言结果。

我们使用 list_foldl来遍历列表l的所有元素。 在line 5中，我们完成了列表类型为'A及累加器类型为Bool的list_foldl列表的实例化。累加器初始值为False（表示尚未有满足断言的元素）。在line 6定义的迭代器函数iter测试了当前列表元素，断言的参数h就是列表元素，然后返回更新了的累加器。如果在某个点找到True，则该值在剩余的折叠中保持不变。