2024年八月月 发布的文章

通过Go示例理解函数式编程思维

本文永久链接 – https://tonybai.com/2024/08/11/understand-functional-programming-in-go

一个孩子要尝试10次、20次才肯接受一种新的食物,我们接受一种新的范式,大概不会比这个简单。– 郭晓刚 《函数式编程思维》译者

函数式编程(Functional Programming, 简称fp)是一种编程范式,与命令式编程(Imperative Programming)、面向对象编程(OOP)、泛型编程(Generics Programming)、逻辑编程(logic Programming)等是一类的概念。

注:尽管面向对象范式引入了新的编程思想和技术,但它本质上与命令式编程一样,都关注程序的状态和如何通过改变状态来控制程序的执行流程,因此,OOP仍然属于命令式编程的一个分支。OOP可以看作是命令式编程的一种扩展和补充,它增强了代码的模块化、复用性和可维护性。在接下来,我会统一使用命令式编程范式来指代它们。

但几十年的编程语言的演进和实践已经证明:函数式编程并非银弹,它有优势,更有不足。从编程社区的实际反映来看,纯函数式编程语言(比如:CLispHaskell、Scala、Clojure、Erlang等)始终处于小众地位。此外,即便很多主流命令式编程语言在近些年融入了一些函数式编程的语法特性,采用函数式风格的代码依旧比例极低,且不易被广泛接受。许多程序员在面对复杂的状态管理和副作用时,依然倾向于使用传统的命令式编程风格(包括OOP)。。

注:Go就原生提供了一些支持函数式范式编程的语法特性,比如:函数是一等公民(first-class)、高阶函数、闭包函数迭代器以及泛型等。

造成这种局面的原因众说纷纭,但我认为有如下几个:

首先从人类这个物种的大脑的认知和思维方式来看,命令式编程更接近于人类的自然思维方式,其逻辑与人类解决问题时的逻辑思维相似,即都是以步骤的形式理解问题,且有明确的控制流:命令式语言的控制结构(如条件语句、选择语句和循环)使得程序的执行路径清晰可见,符合人类的直觉理解,这也使得命令式语言更容易被人类大脑所掌握。

其次,命令式编程强调状态的变化,程序员可以直接看到和控制变量的变化,这与人类处理现实世界事物的方式相似。

在上面原因的驱使下,久而久之,程序员便形成习惯与传统,有了积淀,便可以促进命令式编程语言在教育和产业中的广泛应用,使得大多数程序员习惯于这种编程方式(间接挤压了函数式编程的使用空间)。进而使得命令式语言有更丰富的学习资源和社区支持,程序员也更容易找到帮助和示例。

也就是说,命令式编程范式占据主流的根本原因是人类的大脑本身就是命令式的,而不是函数式的。不过也有极少数大脑是函数式思维的,比如发明了TLA+这门形式化建模和验证语言Leslie Lamport老先生

那么问题来了!既然学习函数式编程思维是违反人类大脑直觉的,且较为困难,那为什么还是有很多人学习函数式编程思维,并在实际开发中应用函数式编程范式呢?关于这个问题,我们可以从两方面来看。

从主观上说,程序员经常有探索新技术和新范式的内在动力,这种好奇心驱使他们尝试函数式编程,也就是我们俗称的“玩腻了,尝尝鲜儿”。并且,许多程序员视学习函数式编程为一种智力挑战,一种来自舒适区之外的挑战,这种挑战能带来成就感和个人成长。此外,在竞争激烈的IT行业,掌握多种编程范式可以使得个人技能多样化,增加个人的职业竞争力。

从客观上看,函数式编程也确实能帮助程序员提高抽象思维和系统设计能力,这种能力的提升不仅限于函数式编程,还能应用到其他编程范式中。并且,函数式编程为程序员提供了一个新的解决问题的视角和方法,特别是在处理并发和并行计算、复杂数据转换和流处理方面。

学习函数式编程范式,并不是说抛弃命令式范式(或其他范式),而是融合,从主流编程语言对函数式编程的语法特性的支持也可窥见这般。

那么,到底什么是函数式编程范式?它与命令式范式对比又有怎么样的差异与优劣呢?在这篇文章中,我就来说说我的体会,并辅以Go示例来帮助大家理解。

1. 思维差异:命令式编程 vs. 函数式编程

在看过很多函数式编程的资料后(见文后的参考资料一节),我问了自己一个问题:面对同一个实际的问题,用命令式编程范式和用函数式编程范式的核心思维差异在哪里?为此,我基于现实世界的一个典型问题模型(数据输入 -> 数据处理 -> 处理结果输出),并根据自己的理解画了下面两幅图:


命令式编程范式的思维


函数式编程范式的思维

我们先来描述一下上面两幅图中的数据处理流程:

  • 命令式编程:通过I/O操作获取数据,然后解码为自定义类型进行处理,再编码为自定义类型以便I/O操作输出。处理过程中使用函数、带方法的类型和控制流结构(如for、if、switch等)。

  • 函数式编程:通过带有副作用的操作(如I/O操作)获取数据,然后解码数据放入通用数据结构(如列表、元组、映射)进行处理,再放入通用数据结构以便通过副作用操作输出。处理过程中会使用纯函数、高阶函数以及它们的函数组合。

基于上述流程的说明,我们可以看出两种范式核心关注点的差异:

  • 命令式编程范式:更关注类型的封装、类型间的耦合关系、行为集合的抽象(接口)以及对数据在类型实例间的传递的显式控制(if/for/switch)。
  • 函数式编程范式:弱化类型的概念,使用通用数据结构,专注于通过纯函数/高阶函数、不可变数据和函数组合来实现对数据的处理逻辑。“控制流”更加隐含,比如会通过递归、模式匹配和惰性求值等方式实现。建立专门的抽象来应对与真实世界交互时的带有副作用(side effect)的操作。

下面我们通过一个具体的问题来大致体会一下不同编程泛型在解决问题的实现上的思维差异。这个问题很简单:编写一个程序从input.txt文件中读取数字(每行一个数字),将每个数字乘以2,然后将结果写入output.txt文件中。

我们先来用命令式编程范式实现:

// fp-in-go/double/go/main.go

// NumberData represents the input data
type NumberData struct {
    numbers []int
}

// ProcessedData represents the processed output data
type ProcessedData struct {
    numbers []int
}

// NewNumberData creates and returns a new NumberData instance
func NewNumberData() *NumberData {
    return &NumberData{numbers: []int{}}
}

// AddNumber adds a number to NumberData
func (nd *NumberData) AddNumber(num int) {
    nd.numbers = append(nd.numbers, num)
}

// Process doubles all numbers in NumberData and returns ProcessedData
func (nd *NumberData) Process() ProcessedData {
    processed := ProcessedData{numbers: make([]int, len(nd.numbers))}
    for i, num := range nd.numbers {
        processed.numbers[i] = num * 2
    }
    return processed
}

// FileProcessor handles file operations and data processing
type FileProcessor struct {
    inputFile  string
    outputFile string
}

// NewFileProcessor creates and returns a new FileProcessor instance
func NewFileProcessor(input, output string) *FileProcessor {
    return &FileProcessor{
        inputFile:  input,
        outputFile: output,
    }
}

// ReadAndDeserialize reads data from input file and deserializes it into NumberData
func (fp *FileProcessor) ReadAndDeserialize() (*NumberData, error) {
    file, err := os.Open(fp.inputFile)
    if err != nil {
        return nil, fmt.Errorf("error opening input file: %w", err)
    }
    defer file.Close()

    data := NewNumberData()
    scanner := bufio.NewScanner(file)
    for scanner.Scan() {
        num, err := strconv.Atoi(scanner.Text())
        if err != nil {
            return nil, fmt.Errorf("error converting to number: %w", err)
        }
        data.AddNumber(num)
    }

    if err := scanner.Err(); err != nil {
        return nil, fmt.Errorf("error reading input file: %w", err)
    }

    return data, nil
}

// SerializeAndWrite serializes ProcessedData and writes it to output file
func (fp *FileProcessor) SerializeAndWrite(data ProcessedData) error {
    file, err := os.Create(fp.outputFile)
    if err != nil {
        return fmt.Errorf("error creating output file: %w", err)
    }
    defer file.Close()

    writer := bufio.NewWriter(file)
    defer writer.Flush()

    for _, num := range data.numbers {
        _, err := writer.WriteString(fmt.Sprintf("%d\n", num))
        if err != nil {
            return fmt.Errorf("error writing to output file: %w", err)
        }
    }

    return nil
}

// Process orchestrates the entire data processing workflow
func (fp *FileProcessor) Process() error {
    // Read and deserialize input data
    inputData, err := fp.ReadAndDeserialize()
    if err != nil {
        return err
    }

    // Process data
    processedData := inputData.Process()

    // Serialize and write output data
    err = fp.SerializeAndWrite(processedData)
    if err != nil {
        return err
    }

    return nil
}

func main() {
    processor := NewFileProcessor("input.txt", "output.txt")
    if err := processor.Process(); err != nil {
        fmt.Fprintf(os.Stderr, "Error: %v\n", err)
        os.Exit(1)
    }
    fmt.Println("Processing completed successfully.")
}

这段代码十分容易理解,在这段代码中,我们建立了三个类型:NumberData、ProcessedData和FileProcessor。前两个分别代表解码后的输入数据和编码前的输出数据,FileProcessor则是封装了文件操作和数据处理的逻辑的自定义类型。这段代码将文件I/O、数据处理和主要流程控制分离到不同的方法中。在读取和写入过程中,数据经历了字符串 -> NumberData -> ProcessedData -> 字符串的转换过程,同时数据也是在不同类型的方法间传递和变换状态

接下来我们再来看看函数式范式版本,Go虽然提供了一些函数式编程的基础支持,比如一等公民的函数、支持高阶函数、闭包等,但一些像monad、monoid等高级概念还需要手工实现。IBM开源了一个Go的函数式编程基础库fp-go,这里就借用fp-go的便利实现上面的同等功能,我们看看风格上有何不同:

// fp-in-go/double/fp-go/main.go

package main

import (
    "bufio"
    "fmt"
    "os"
    "strconv"
    "strings"

    "github.com/IBM/fp-go/either"
    "github.com/IBM/fp-go/ioeither"
)

// 读取文件内容
func readFile(filename string) ioeither.IOEither[error, string] {
    return ioeither.TryCatchError(func() (string, error) {
        content, err := os.ReadFile(filename)
        return string(content), err
    })
}

// 将字符串转换为数字列表
func parseNumbers(content string) either.Either[error, []int] {
    numbers := []int{}
    scanner := bufio.NewScanner(strings.NewReader(content))
    for scanner.Scan() {
        num, err := strconv.Atoi(scanner.Text())
        if err != nil {
            return either.Left[[]int](err)
        }
        numbers = append(numbers, num)
    }
    return either.Right[error](numbers)
}

// 将数字乘以2
func multiplyBy2(numbers []int) []int {
    result := make([]int, len(numbers))
    for i, num := range numbers {
        result[i] = num * 2
    }
    return result
}

// 将结果写入文件
func writeFile(filename string, content string) ioeither.IOEither[error, string] {
    return ioeither.TryCatchError(func() (string, error) {
        return "", os.WriteFile(filename, []byte(content), 0644)
    })
}

func main() {
    program := ioeither.Chain(func(content string) ioeither.IOEither[error, string] {
        return ioeither.FromEither(
            either.Chain(func(numbers []int) either.Either[error, string] {
                multiplied := multiplyBy2(numbers)
                result := []string{}
                for _, num := range multiplied {
                    result = append(result, strconv.Itoa(num))
                }
                return either.Of[error](strings.Join(result, "\n"))
            })(parseNumbers(content)),
        )
    })(readFile("input.txt"))

    program = ioeither.Chain(func(content string) ioeither.IOEither[error, string] {
        return writeFile("output.txt", content)
    })(program)

    result := program()
    err := either.ToError(result)

    if err != nil {
        fmt.Println("Program failed:", err)
    } else {
        fmt.Println("Program completed successfully")
    }
}

相对于前面使用命令式范式风格的代码,这段函数式范式的代码理解起来就要难上不少。

不过,这段代码很好地诠释了函数式编程中的函数组合理念,我们看到函数被当作值来传递和使用。例如,在ioeither.Chain中,我们传递了匿名函数作为参数,这体现了函数式编程中函数作为一等公民的概念。multiplyBy2函数是一个纯函数的例子,它没有副作用,对于相同的输入总是产生相同的输出。这种纯函数更容易测试和推理。

代码中最明显的函数组合例子是在main函数中,我们使用ioeither.Chain来组合多个函数操作。并且在这里,我们将文件读取、内容处理和文件写入操作串联在一起,形成一个更大的操作。而ioeither.Chain和either.Chain又都是高阶函数的例子,它们接受其他函数作为参数并返回新的函数。Either和IOEither类型也是函数式编程中用于错误处理的主流方式,允许我们以更函数式的方式处理错误,将错误处理集成到函数组合中。

很多人好奇如果用纯函数式编程语言实现这个示例会是什么样子的,下面我就贴一段Haskell语言的代码,大家简单了解一下,这里就不对代码进行解释了:

// fp-in-go/double/fp-haskell/Main.hs

import System.IO
import Control.Monad (when)
import Text.Read (readMaybe)
import Data.Maybe (catMaybes)

-- Define a custom type for the result
data DoubledNumbers = DoubledNumbers { doubledNumbers :: [Int] } deriving (Show)

-- Function to read numbers from a file
readNumbers :: FilePath -> IO (Either String [Int])
readNumbers filePath = do
    content <- readFile filePath
    let numbers = catMaybes (map readMaybe (lines content))
    return $ if null numbers
             then Left "No valid numbers found."
             else Right numbers

-- Function to write result to a file
writeResult :: FilePath -> DoubledNumbers -> IO (Either String ())
writeResult filePath result = do
    let resultString = unlines (map show (doubledNumbers result))
    writeFile filePath resultString
    return $ Right ()

-- Function to double the numbers
doubleNumbers :: [Int] -> DoubledNumbers
doubleNumbers numbers = DoubledNumbers { doubledNumbers = map (* 2) numbers }

main :: IO ()
main = do
    -- Read numbers from input.txt
    readResult <- readNumbers "input.txt"
    case readResult of
        Left err -> putStrLn $ "Error: " ++ err
        Right numbers -> do
            let result = doubleNumbers numbers
            -- Write result to output.txt
            writeResultResult <- writeResult "output.txt" result
            case writeResultResult of
                Left err -> putStrLn $ "Error: " ++ err
                Right () -> putStrLn "Successfully written the result to output.txt."

注:安装ghc后,执行ghc –make Main就可以将上面Main.hs编译为一个可执行程序。更多关于haskell编译器的信息可以到haskell官网查看。

从上面的示例我们大致也能感受到两种范式在思维层面的差异,正如Robert Martin在《函数式设计》一书中说道的那样:函数式程序更倾向于铺设调节数据流转换的管道结构,而可变的命令式程序更倾向于迭代地处理一个个类型对象

我们很难在一个例子中体现出函数式编程的所有概念和思维特点,接下来,我们就来逐个说说函数式编程范式中的要素,你也可以对应前面的图中的内容,反复感受函数式编程的思维特点。

2. 函数式编程的要素

面向对象的编程通过封装不确定因素来使代码能被人理解,而函数式编程通过尽量减少不确定因素来使代码能被人理解。—— Michael Feathers 《修改代码的艺术》一书作者

函数式编程建立在几个核心要素之上,这些要素共同构成了函数式编程的基础。让我们逐一探讨这些要素。

2.1 纯函数 (Pure Functions)

纯函数是函数式编程的基石。一个纯函数具有以下特性:

  • 对于相同的输入,总是产生相同的输出;
  • 不会产生副作用(不会修改外部状态);
  • 不依赖外部状态。

例如,前面fp-go示例中的multiplyBy2就是一个纯函数:

func multiplyBy2(numbers []int) []int {
    result := make([]int, len(numbers))
    for i, num := range numbers {
        result[i] = num * 2
    }
    return result
}

这个函数总是为相同的输入返回相同的结果,并且不会修改任何外部状态。

2.2 不可变性 (Immutability)

Robert Martin在《函数式设计》一书为函数式编程下一个理想的定义:没有赋值语句的编程。实质是其强调了不可变性在函数式编程范式中的重要意义。在没有赋值语句的情况下,代码通常基于对原状态的计算而得到新的状态,而对原状态没有任何修改。

在Go语言中,由于不支持不可变变量(很多语言用val关键字来声明不可变变量,但Go并不支持),我们通常通过复制对象来实现不可变性,这可以帮助我们避免状态变化带来的复杂性,但也因为复制而增加了内存开销和性能成本。

// 定义一个不可变的结构体
type Point struct {
    x, y int
}

// 创建一个新的 Point,模拟不可变性
func NewPoint(x, y int) Point {
    return Point{x, y}
}

// 移动Point的方法,返回一个新的Point
func (p Point) Move(dx, dy int) Point {
    return NewPoint(p.x+dx, p.y+dy)
}

2.3 高阶函数 (Higher-Order Functions)与函数组合(Function Composition)

Go语言的一个内置特性让它具备了使用函数式编程范式的前提,那就是在Go中,函数是一等公民。这意味着函数可以像其他类型变量一样,被赋值、传参和返回。

而接受其他函数作为参数或返回函数的函数,被称为高阶函数,这也是函数式编程的基石,如下面的applyOperation函数就是一个高阶函数:

func applyOperation(x int, operation func(int) int) int {
    return operation(x)
}

func double(x int) int {
    return x * 2
}

result := applyOperation(5, double) // 结果为10

而有了对高阶函数的支持,我们才能运用函数式思维中的核心思维:函数组合,来铺设调节数据流转换的管道结构:

// fp-in-go/high-order-func/main.go

package main

import (
    "fmt"
)

// 定义一个类型为函数的别名
type IntTransformer func(int) int

// 将多个转换函数组合成一个管道
func pipe(value int, transformers ...IntTransformer) int {
    for _, transformer := range transformers {
        value = transformer(value)
    }
    return value
}

// 定义一些转换函数
func addOne(x int) int {
    return x + 1
}

func square(x int) int {
    return x * x
}

func main() {
    // 使用管道处理数据
    result := pipe(3, addOne, square)
    fmt.Println("Result:", result) // 输出 Result: 16
}

这个示例中的pipe函数接受一个初始值和多个转换函数,并将其串联执行。main函数调用pipe函数,将addOne和square两个转换函数连接起来并执行输出结果。

前面那个使用fp-go编写的示例中,使用ioeither.Chain构建的program也是一个函数调用组合。

此外,链式调用也是一种在日常开发中常见的函数组合的使用形式,它融合了命令式的类型和函数式编程的函数组合,特别适用于集合类型数据的处理,通过链式调用,可以以更简洁和直观的方式进行数据转换和处理。下面是一个基于泛型实现的通用的链式调用(filter -> map -> reduce)的示例:

// fp-in-go/func-composition/main.go

package main

import "fmt"

// Collection 接口定义了通用的集合操作
type Collection[T any] interface {
    Filter(predicate func(T) bool) Collection[T]
    Map(transform func(T) T) Collection[T]
    Reduce(initialValue T, reducer func(T, T) T) T
}

// SliceCollection 是基于切片的集合实现
type SliceCollection[T any] struct {
    data []T
}

// NewSliceCollection 创建一个新的 SliceCollection
func NewSliceCollection[T any](data []T) *SliceCollection[T] {
    return &SliceCollection[T]{data: data}
}

// Filter 实现了 Collection 接口的 Filter 方法
func (sc *SliceCollection[T]) Filter(predicate func(T) bool) Collection[T] {
    result := make([]T, 0)
    for _, item := range sc.data {
        if predicate(item) {
            result = append(result, item)
        }
    }
    return &SliceCollection[T]{data: result}
}

// Map 实现了 Collection 接口的 Map 方法
func (sc *SliceCollection[T]) Map(transform func(T) T) Collection[T] {
    result := make([]T, len(sc.data))
    for i, item := range sc.data {
        result[i] = transform(item)
    }
    return &SliceCollection[T]{data: result}
}

// Reduce 实现了 Collection 接口的 Reduce 方法
func (sc *SliceCollection[T]) Reduce(initialValue T, reducer func(T, T) T) T {
    result := initialValue
    for _, item := range sc.data {
        result = reducer(result, item)
    }
    return result
}

// SetCollection 是基于 map 的集合实现
type SetCollection[T comparable] struct {
    data map[T]struct{}
}

// NewSetCollection 创建一个新的 SetCollection
func NewSetCollection[T comparable]() *SetCollection[T] {
    return &SetCollection[T]{data: make(map[T]struct{})}
}

// Add 向 SetCollection 添加元素
func (sc *SetCollection[T]) Add(item T) {
    sc.data[item] = struct{}{}
}

// Filter 实现了 Collection 接口的 Filter 方法
func (sc *SetCollection[T]) Filter(predicate func(T) bool) Collection[T] {
    result := NewSetCollection[T]()
    for item := range sc.data {
        if predicate(item) {
            result.Add(item)
        }
    }
    return result
}

// Map 实现了 Collection 接口的 Map 方法
func (sc *SetCollection[T]) Map(transform func(T) T) Collection[T] {
    result := NewSetCollection[T]()
    for item := range sc.data {
        result.Add(transform(item))
    }
    return result
}

// Reduce 实现了 Collection 接口的 Reduce 方法
func (sc *SetCollection[T]) Reduce(initialValue T, reducer func(T, T) T) T {
    result := initialValue
    for item := range sc.data {
        result = reducer(result, item)
    }
    return result
}

// ToSlice 实现了 Collection 接口的 ToSlice 方法
func (sc *SetCollection[T]) ToSlice() []T {
    result := make([]T, 0, len(sc.data))
    for item := range sc.data {
        result = append(result, item)
    }
    return result
}

func main() {
    // 使用 SliceCollection
    numbers := NewSliceCollection([]int{1, 2, 3, 4, 5, 6, 7, 8, 9, 10})
    result := numbers.
        Filter(func(n int) bool { return n%2 == 0 }).
        Map(func(n int) int { return n * 2 }).
        Reduce(0, func(acc, n int) int { return acc + n })
    fmt.Println(result) // 输出: 60

    // 使用 SetCollection
    set := NewSetCollection[int]()
    for _, n := range []int{1, 2, 2, 3, 3, 3, 4, 5} {
        set.Add(n)
    }
    uniqueSum := set.
        Filter(func(n int) bool { return n > 2 }).
        Map(func(n int) int { return n * n }).
        Reduce(0, func(acc, n int) int { return acc + n })
    fmt.Println(uniqueSum) // 输出: 50 (3^2 + 4^2 + 5^2)
}

这段代码定义的泛型接口类型Collection包含三个方法:

  • Filter:根据条件过滤集合中的元素。
  • Map:对集合中的每个元素应用转换函数。
  • Reduce:对集合中的元素进行归约操作,比如求和。

其中Filtre、Map都是返回集合自身,这样便允许实现Collection接口的集合类型(如上面的SetCollection和SliceCollection)使用链式调用,代码看起来也十分易于理解。

2.4 递归(Recursion)

递归是函数式编程中常用的控制结构,常用来替代循环。例如下面是计算阶乘的函数实现:

func factorial(n int) int {
    if n <= 1 {
        return 1
    }
    return n * factorial(n-1)
}

递归的优点十分明显,代码简洁,易于理解(相对于循环),特别适合处理分解问题(如树结构、图遍历等)。但不足也很突出,比如可能导致栈溢出(尤其是对那些不支持尾递归优化的语言,比如Go),特别是对于较大的输入。此外,由于每次递归调用都需要创建新栈帧,维护栈状态,递归会有额外的性能开销。调试递归函数也可能比循环更复杂,因为需要跟踪多个函数调用。

2.5 惰性求值 (Lazy Evaluation)

惰性求值是指延迟计算表达式的值,直到真正需要它的时候。这样可以避免不必要的计算并有效管理内存,特别是在处理大集合或无限集合时。下面是用惰性求值实现迭代集合元素的示例:

注:Go原生并不支持惰性求值的语法,但我们可以使用闭包来模拟。

// fp-in-go/lazy-evaluation/lazy-range/main.go

package main

import "fmt"

func lazyRange(start, end int) func() (int, bool) {
    current := start
    return func() (int, bool) {
        if current >= end {
            return 0, false
        }
        result := current
        current++
        return result, true
    }
}
func main() {
    next := lazyRange(1, 5)
    for {
        value, hasNext := next()
        if !hasNext {
            break
        }
        fmt.Println(value)
    }
}

我们看到这段代码通过惰性求值方式生成从1到4的数字,避免了预先生成整个范围的集合元素,节省了内存,并避免了不必要的计算。

我们再来看一个用惰性求值生成前N个斐波那契数列的示例:

// fp-in-go/lazy-evaluation/fibonacci/main.go

package main

import (
    "fmt"
)

// Fibonacci 返回一个生成无限斐波那契数列的函数
func Fibonacci() func() int {
    a, b := 0, 1
    return func() int {
        a, b = b, a+b
        return a
    }
}

func main() {
    fib := Fibonacci()
    for i := 0; i < 10; i++ { // 打印前10个斐波那契数
        fmt.Println(fib())
    }
}

我们看到Fibonacci函数返回一个闭包,每次调用时生成下一个斐波那契数,这样我们在需要时生成下一个斐波那契数,而无需生成所有。

虽然函数式编程强调纯函数和不可变性,但在实际应用中,我们不可避免地需要处理副作用,如I/O操作、数据库交互等。接下来,我们就来看看在函数式编程范式中是如何处理带有副作用的操作的。

3. 函数式编程对副作用操作的处理

3.1 理解副作用

在函数式编程中,副作用是指函数或表达式在执行过程中对其周围环境产生的任何可观察到的变化。这些变化包括但不限于:

  • 修改全局变量或静态局部变量
  • 修改函数参数
  • 执行I/O操作(读写文件、网络通信等)
  • 抛出异常或错误
  • 调用其他具有副作用的函数

副作用使得程序的行为变得难以预测和测试,因为函数的输出不仅依赖于其输入,还依赖于程序的状态和外部环境。函数式编程通过最小化副作用来提高程序的可预测性和可测试性。

3.2 Monad: 函数式编程中处理副作用的核心抽象

在函数式编程中,Monad是一种用于处理副作用的核心抽象。它提供了一种结构化的方式来处理计算中的状态、异常、输入输出等副作用,使得程序更加模块化和可组合。

在范畴论中,Monad被定义为一个自函子(endofunctor)加上两个自然变换(有点抽象了):

  • return (也称为unit):将一个值封装到Monad中。
  • bind (也称为flatMap或>>=):将一个Monad中的值应用到一个函数中,并返回一个新的Monad。

注:要入门范畴论,可以参考《Category Theory for Programmers》这本书。

Monad可以通过以下策略来处理副作用:

  • 延迟执行:将副作用操作封装在Monad中,但不立即执行,这样可以将副作用推迟到程序的边缘。
  • 显式表示:使副作用成为类型系统的一部分,迫使开发者显式地处理这些效果。
  • 组合性:提供了一种方式来组合包含副作用的操作,而不破坏函数的纯粹性。
  • 错误处理:提供了一种统一的方式来处理可能失败的操作。
  • 状态管理:允许在一系列操作中传递和修改状态,而不需要使用可变变量。

在实际应用中,我们可以根据具体需求选择使用不同的Monad实现。每种Monad都有其适用场景,比如:

  • 使用Option(Maybe) Monad处理可能缺失的值,避免空指针异常。
  • 使用Result(Either) Monad 处理可能失败的操作,提供更丰富的错误信息。
  • 使用IO Monad封装所有的I/O操作,将副作用推迟到程序的边缘。

接下来,我们就结合Go示例来逐一探讨这三种Monad实现。

3.3 Option (Maybe)

Option 用于表示一个值可能存在或不存在,避免了使用null或undefined带来的问题。

// fp-in-go/side-effect/option/main.go

package main

import "fmt"

type Option[T any] struct {
    value   T
    present bool
}

func Some[T any](x T) Option[T] {
    return Option[T]{value: x, present: true}
}

func None[T any]() Option[T] {
    return Option[T]{present: false}
}

func (o Option[T]) Bind(f func(T) Option[T]) Option[T] {
    if !o.present {
        return None[T]()
    }
    return f(o.value)
}

// 使用示例
func safeDivide(a, b int) Option[int] {
    if b == 0 {
        return None[int]()
    }
    return Some(a / b)
}

func main() {
    result := Some(10).Bind(func(x int) Option[int] {
        return safeDivide(x, 2)
    })
    fmt.Println(result) // {5 true}

    result = Some(10).Bind(func(x int) Option[int] {
        return safeDivide(x, 0)
    })
    fmt.Println(result) // {0 false}
}

这段示例程序定义了一个Option结构体:包含一个值和一个表示值是否存在的布尔变量。Some和None函数是Option的创建函数,Some函数:返回一个包含值的Option。None函数返回一个不包含值的Option。Bind方法对Option中的值应用一个函数,如果值不存在则返回None。

3.4 Result (Either)

Result可用于处理可能产生错误的操作,它比Option提供了更多的信息,它可以可以携带错误信息。

// fp-in-go/side-effect/result/main.go

package main

import (
    "fmt"
    "os"
    "strings"
)

type Result[T any] struct {
    value T
    err   error
    isOk  bool
}

func Ok[T any](value T) Result[T] {
    return Result[T]{value: value, isOk: true}
}

func Err[T any](err error) Result[T] {
    return Result[T]{err: err, isOk: false}
}

func (r Result[T]) Bind(f func(T) Result[T]) Result[T] {
    if !r.isOk {
        return Err[T](r.err)
    }
    return f(r.value)
}

// 使用示例
func readFile(filename string) Result[string] {
    content, err := os.ReadFile(filename)
    if err != nil {
        return Err[string](err)
    }
    return Ok(string(content))
}

func processContent(content string) Result[string] {
    // 处理内容...
    return Ok(strings.ToUpper(content))
}

func main() {
    result := readFile("input.txt").Bind(processContent)
    fmt.Println(result) // {HELLO, GOLANG <nil> true}
    result = readFile("input1.txt").Bind(processContent)
    fmt.Println(result) // { 0xc0000a0420 false}
}

这段示例程序定义了一个Result结构体:包含一个值、一个错误信息和一个表示操作是否成功的布尔变量。Ok和Err函数是Result的创建函数,Ok函数返回一个成功的Result。Err函数返回一个失败的Result。Bind方法对成功的Result中的值应用一个函数,如果操作失败则返回错误。

在示例中,我们分别用读取input.txt和不存在的input1.txt来演示成功和错误的两个情况,具体输出结果见上面代码中的注释。

3.5 IO Monad

IO Monad用于封装所有的带有副作用的输入/输出操作,使得这些操作在类型系统中可见,并且可以被推迟执行。

// fp-in-go/side-effect/io-monad/main.go

package main

import (
    "fmt"
    "os"
    "strings"
)

// IO represents an IO operation that, when run, produces a value of type any or an error
type IO struct {
    run func() (any, error)
}

// NewIO creates a new IO monad
func NewIO(f func() (any, error)) IO {
    return IO{run: f}
}

// Bind chains IO operations, allowing for type changes
func (io IO) Bind(f func(any) IO) IO {
    return NewIO(func() (any, error) {
        v, err := io.run()
        if err != nil {
            return nil, err
        }
        return f(v).run()
    })
}

// Map transforms the value inside IO
func (io IO) Map(f func(any) any) IO {
    return io.Bind(func(v any) IO {
        return NewIO(func() (any, error) {
            return f(v), nil
        })
    })
}

// Pure lifts a value into the IO context
func Pure(x any) IO {
    return NewIO(func() (any, error) { return x, nil })
}

// ReadFile is an IO operation that reads a file
func ReadFile(filename string) IO {
    return NewIO(func() (any, error) {
        content, err := os.ReadFile(filename)
        if err != nil {
            return nil, fmt.Errorf("failed to read file: %w", err)
        }
        return string(content), nil
    })
}

// WriteFile is an IO operation that writes to a file
func WriteFile(filename string, content string) IO {
    return NewIO(func() (any, error) {
        err := os.WriteFile(filename, []byte(content), 0644)
        if err != nil {
            return nil, fmt.Errorf("failed to write file: %w", err)
        }
        return true, nil
    })
}

// Print is an IO operation that prints to stdout
func Print(x any) IO {
    return NewIO(func() (any, error) {
        fmt.Println(x)
        return x, nil
    })
}

func main() {
    // Example: Read a file, transform its content, and write it back
    program := ReadFile("input.txt").
        Map(func(v any) any {
            return strings.ToUpper(v.(string))
        }).
        Bind(func(v any) IO {
            return WriteFile("output.txt", v.(string))
        }).
        Bind(func(v any) IO {
            success := v.(bool)
            if success {
                return Pure("File processed successfully")
            }
            return Pure("Failed to process file")
        }).
        Bind(func(v any) IO {
            return Print(v)
        })

    // Run the IO operation
    result, err := program.run()
    if err != nil {
        fmt.Printf("An error occurred: %v\n", err)
    } else {
        fmt.Printf("Program completed: %s\n", result)
    }
}

这个示例提供了一个非泛型版本的IO Monad的Go实现,它允许我们链式组合带有副作用的IO操作,同时保持了一定程度的类型安全(尽管需要类型断言)。在实际使用中,你完全不用自己实现IO Monad,可以直接使用IBM/fp-go中的ioeither,就像本文初那个示例那样。

4. 小结

到这里,关于函数式编程思维的入门介绍就告一段落了!

通过上面的介绍,我们看到函数式编程提供了一种不同于传统命令式编程的思维方式。它强调不可变性、纯函数和函数的组合,为数据流的处理搭建管道,这些特性使得代码更易于理解、测试和并行化。然而,函数式编程也带来了一些挑战,如处理副作用和状态管理的复杂性和难于理解。

学习函数式编程不仅可以扩展我们的编程技能,还能帮助我们以新的方式思考问题和设计解决方案。正如《函数式编程思维》一书中译者所说,接受一种新的编程范式可能需要时间和耐心,但最终会带来新的见解和能力。

在实际应用中,纯粹的函数式编程并不常见,更常见的是将函数式编程的概念和技术与其他编程范式(主要就是命令式范式)相结合。

Go语言虽然不是一个纯函数式语言,但它提供了足够的特性来支持函数式编程风格,如一等公民的函数、闭包和高阶函数等。

最后要记住,编程范式是工具,而不是教条。好的程序员应该能够根据具体问题和场景,灵活地选择和组合不同的编程范式,以创造出最优雅、高效的解决方案。

本文涉及的源码可以在这里下载 – https://github.com/bigwhite/experiments/blob/master/fp-in-go

本文部分源代码由Claude 3.5 sonnet和GPT-4o生成。

5. 参考资料


Gopher部落知识星球在2024年将继续致力于打造一个高品质的Go语言学习和交流平台。我们将继续提供优质的Go技术文章首发和阅读体验。同时,我们也会加强代码质量和最佳实践的分享,包括如何编写简洁、可读、可测试的Go代码。此外,我们还会加强星友之间的交流和互动。欢迎大家踊跃提问,分享心得,讨论技术。我会在第一时间进行解答和交流。我衷心希望Gopher部落可以成为大家学习、进步、交流的港湾。让我相聚在Gopher部落,享受coding的快乐! 欢迎大家踊跃加入!

img{512x368}
img{512x368}

img{512x368}
img{512x368}

著名云主机服务厂商DigitalOcean发布最新的主机计划,入门级Droplet配置升级为:1 core CPU、1G内存、25G高速SSD,价格5$/月。有使用DigitalOcean需求的朋友,可以打开这个链接地址:https://m.do.co/c/bff6eed92687 开启你的DO主机之路。

Gopher Daily(Gopher每日新闻) – https://gopherdaily.tonybai.com

我的联系方式:

  • 微博(暂不可用):https://weibo.com/bigwhite20xx
  • 微博2:https://weibo.com/u/6484441286
  • 博客:tonybai.com
  • github: https://github.com/bigwhite
  • Gopher Daily归档 – https://github.com/bigwhite/gopherdaily

商务合作方式:撰稿、出书、培训、在线课程、合伙创业、咨询、广告合作。

使用TLA+形式化验证Go并发程序

本文永久链接 – https://tonybai.com/2024/08/05/formally-verify-concurrent-go-programs-using-tla-plus

Writing is nature’s way of letting you know how sloppy your thinking is – Guindon

在2024年6月份举办的GopherCon Europe Berlin 2024上,一个叫Raghav Roy的印度程序员(听口音判断的)分享了Using Formal Reasoning to Build Concurrent Go Systems,介绍了如何使用形式化验证工具TLA+来验证Go并发程序的设计正确性。

TLA+是2013年图灵奖获得者、美国计算机科学家和数学家、分布式系统奠基性大神、Paxos算法Latex的缔造者Leslie B. Lamport设计的一种针对数字系统(Digital Systems)的高级(high-level)建模语言,TLA+诞生于1999年,一直低调演进至今。

TLA+不仅可以对系统建模,还可以与模型验证工具,比如:TLC model checker,结合使用,对被建模系统的行为进行全面的验证。我们可以将TLA+看成一种专门用于数字系统建模和验证的DSL语言

注:TLA是Temporal Logic of Actions的首字母缩写,Temporal Logic,即时序逻辑,是一种用于描述和推理系统行为随时间变化的逻辑框架,由Arthur Prior在1950年代后期引入逻辑学。在后面对TLA+的进一步介绍中,大家可能就会逐渐理解为什么Lamport给这门语言命名为TLA+了。

这不是我第一次接触TLA+,去年就花过一些时间了解过TLA+的资料,可能是因为姿势不够正确,没有在本博客留下只言片语,而这次我打算写点有关TLA+的东西。

1. 为什么需要TLA+

从1999年Lamport发表的论文“Specifying Concurrent Systems with TLA+”以及他2014年在微软的演讲“Thinking Above the Code”中 ,我们大致可以得到Lamport在20多年前设计TLA+的朴素的动机:期望程序员能像科学家一样思考,在编码之前用一种精确的形式化的语言写出目标系统的spec,这个过程类似于建筑架构师在建筑施工之前编制建筑的蓝图(blueprint)

为什么要编写目标系统的spec呢?

综合来自Lamport的相关资料,大致可以梳理出以下两点:

  • 从程序员的角度来看,在开始编码之前,先在抽象的层面思考系统行为,而不是过早地陷入编程语言的具体语法中。并且先写下规格说明,可以帮助程序员明确需求,认知系统,发现潜在问题,并为后续的编码和维护提供指导。
  • 从系统复杂性的角度来看,对于日益复杂的并发和分布式系统,仅靠直觉思考很难保证正确性,传统的测试方法也已经不足以发现所有问题。这时候写spec(规格说明)并用配套的检查工具进行验证就变得非常必要。

那为什么要新设计TLA+来写spec呢,而不是使用像C++这类编程语言,或是其他已存在的形式化语言来编写spec呢?

Lamport给出的理由有以下几个:

  • 编程语言的局限性:像C++这样的编程语言主要是为了实现而设计的,而不是为了spec。它们往往过于关注实现细节,而不是高层次的系统行为,缺乏描述并发和分布式系统所需的抽象能力,不适合表达系统的时序性质和不变量。

  • 已有形式化语言的不足:当时存在的其他形式化语言大多存在要么过于学术化,难以在实际工程中应用,要么难以自然地表达并发和分布式系统的特性等问题;并且缺少工具支持,不具备spec验证功能。

  • 数学建模的局限:纯粹的数学公式虽然精确,但对非数学背景的工程师来说难以理解和使用,缺乏工具支持,难以自动化验证,难以直接映射到系统设计和实现。

Lamport设计的TLA+是建立在坚实的数学基础之上,这使得它能够支持严格的数学推理和证明与自动化验证工具(如TLC模型检查器)无缝集成。TLA+被设计为在高度抽象的层面描述系统,不会像编程语言那样受实现细节的束缚。此外,结合时序逻辑和状态机,TLA+可以描述并发和分布式系统,并在设计层面验证系统的正确性。

根据Lamport的不完全统计,TLA+在Intel、Amazon、Microsoft等大厂都有应用,一些知名的算法以及开源项目也使用TLA+进行了形式化验证,比如Raft算法的作者就给出了Raft算法的TLA+ spec,国内分布式数据库厂商pingcap也在项目中使用TLA+对raft算法以及分布式事务做了形式化的验证

在这些应用案例中,AWS的案例是典型代表。AWS也将应用TLA+过程中积累的经验以paper的形式发表了,其论文集合也被Lamport放置在其个人主页上了。从这些论文内容来看,AWS对TLA+的评价是很正面的:AWS使用TLA+对10个大型复杂的真实系统进行建模和验证,的确发现了多个难以通过其他方法发现的微妙错误。同时,通过精确描述设计,TLA+迫使工程师更清晰地思考,消除了“看似合理的含糊之处”。此外,AWS工程师认为TLA+ spec也是一种很好的文档形式,可以提供精确、简洁、可测试的设计描述,有助于新人快速理解系统。

铺垫了这么多,TLA+究竟是什么?它是如何在高级抽象层面对分布式系统和并发系统进行描述和验证的?接下来,我们就来看一下。

2. Lamport对TLA+的定义

在Lamport的论文、书籍以及一些演讲资料中,他是这么定义TLA+的:A language for high-level modeling digital systems。对于这个定义,我们可以“分段”来理解一下。

  • Digital System

什么是TLA+眼中的数字系统(Digital System)?Lamport认为数字系统包括算法(Algorithms)、程序(Programs)和计算机系统(Computer system),它们有一个共同特点,那就是可以抽象为一个按离散事件序列(sequence of discrete events)进行持续执行和演进的物理系统,这是TLA+后续描述(specify)数字系统的基础。随着多核和云计算的兴起,并发程序和分布式的关键(critical)系统成为了TLA+的主要描述对象,这样的系统最复杂,最难正确实现,价值也最高,值得使用TLA+对其进行形式化的验证。

  • High Level

TLA+面向设计层面,在代码实现层面之上,实施于编写任何实现代码之前。此外,High Level也意味着可以忽略那些系统中不是很关键(less-critical)的部分以及低层次的实现细节。

去除细节进行简化的过程就是抽象(Abstraction),它是工程领域最重要的环节。抽象可以让我们理解复杂的系统,如果不了解系统,我们就无法对系统进行正确的建模并实现它。

而使用TLA+编写系统spec其实就是一个学习对系统进行抽象的过程,学会抽象思考,可以帮助工程师提高设计能力。

  • Modeling

TLA+是通过描述系统的行为(behavior)来对数字系统进行建模的。那么什么是系统的行为呢?如下图所示:


此图由claude sonnet 3.5根据我的prompt生成

行为被Lamport定义为一系列的状态(Sequence of States),这些状态仍然按顺序排列,表示系统随时间的演变。而状态本身则是对变量的赋值。状态之间的转换由动作(action)描述,而系统的正确性由属性(properties)指定。

这种方法特别适合建模并发和分布式系统,因为它允许我们精确地描述系统的所有可能行为,包括不同组件之间的交互和可能的竞争条件,如下图所示:

在TLA+中,属性(properties)是用来描述系统应该满足的条件或特性,它们在验证系统行为的正确性方面起着关键作用。我们所说的系统工作正常就是指这些在执行过程中的属性都得到了满足。

在TLA+中,有两类属性是我们特别需要关注的,一类是安全属性(Safety Properties),一类则是活性属性(Liveness Properties)。前者确保“坏事永远不会发生”,比如使用不变量在并发系统中确保两个进程不会同时进入临界区;后者则是确保“好事最终会发生”,在分布式系统中的最终一致性(eventual consistency)是一个活性属性,它保证系统最终会达到一致的状态。TLA+允许我们精确地指定这些属性,然后使用TLC模型检查器来验证系统是否满足这些属性。这种方法特别适合于复杂的并发和分布式系统,因为它能够发现在传统测试中难以发现的微妙错误。

注:关于TLA+可以用来形式化描述(specify)和验证(check)数字系统的底层数学理论,可以参考Lamport老爷子那本最新尚未完成的书籍A Science of Concurrent Programs(2024.6.7版)

接下来,我们就来看看TLA+究竟如何编写。不过直接介绍TLA+语法比较抽象和枯燥,在我读过的TLA+语法资料中,Lamport在The TLA+ Video Course第二讲中将一个C示例程序一步一步像数学推导一样转换为TLA+语法的讲解对我帮助非常大,我觉得有必要将这个示例放到这篇文章中。

3. 从C代码到TLA+:转换步骤详解

Lamport的这个过程展示了如何从一个具体的编程语言实现(以C代码为例)逐步抽象到一个数学化的、更加通用的系统描述。每一步都增加了抽象级别,最终得到一个可以用于形式化验证的TLA+规范(spec)。以下是这个演进过程的主要阶段:

3.1 初始C程序分析

下面是这个示例的原始C代码:

int i;
void main() {
    i = someNumber();
    i = i + 1;
}

这不是一个并发程序,它只有一个执行路线(execution),前面说过,一个行为(execution)是一个状态序列,我们就来定义这个状态序列以及它们之间的转换关系。

我们先识别出程序的状态变量:i以及引入的控制状态变量(PC),PC变量来表示程序的执行位置。接下来我们就来描述一个可以代码该程序所有状态的“状态机”。

3.2 状态机描述

该程序可以划分为三个状态:

  • 初始状态:i = 0, PC = “start”
  • 中间状态:i in {0, 1, …, 1000}(这里限定了someNumber函数返回的数值范围), PC = “middle”
  • 结束状态:i = i + 1, PC = “done”

下面用自然语言描述一下上述状态的转换关系:

if current value of pc equals "start"
    then next value of i in {0, 1, ..., 1000}
         next value of pc equals "middle"
    else if current value of pc equals "middle"
            then next value of i equals current value of i + 1
                 next value of pc equals "done"
            else no next values

接下来,我们就来将上述对于状态转换的描述变换一下,尽量用数学来表示。

3.3 转换为数学表示

这里的转换分为几步,我们逐一来看。

  • 换掉”current value of”
if pc equals "start"
    then next value of i in {0, 1, ..., 1000}
         next value of pc equals "middle"
    else if pc equals "middle"
            then next value of i equals i + 1
                 next value of pc equals "done"
            else no next values

替换后,pc即the current value of pc,i即current value of i。

  • 换掉”next value of”

我们用i’换掉”next value of i”, 用pc’换掉”next value of pc”,结果如下:

if pc equals "start"
    then i' in {0, 1, ..., 1000}
         pc' equals "middle"
    else if pc equals "middle"
            then i' equals i + 1
                 pc' equals "done"
            else no next values
  • 用”=”符号换掉equals

替换的结果如下:

if pc = "start"
    then i' in {0, 1, ..., 1000}
         pc' = "middle"
    else if pc = "middle"
            then i' = i + 1
                 pc' = "done"
            else no next values
  • 将in换为数学符号∈
if pc = "start"
    then i' ∈ {0, 1, ..., 1000}
         pc' = "middle"
    else if pc = "middle"
            then i' = i + 1
                 pc' = "done"
            else no next values

3.4 TLA+语法转换

  • 将集合表示换为正式的数学符号

{0, 1, …, 1000}并非数学表示集合的方式,替换后,结果如下:

if pc = "start"
    then i' ∈ 0..1000
         pc' = "middle"
    else if pc = "middle"
            then i' = i + 1
                 pc' = "done"
            else no next values

这里0..1000使用了TLA+的集合表示语法。

  • 转换为单一公式(formula)

将C代码转换为上面的最新代码后,你不要再按照C的语义去理解上述转换后的代码了。新代码并非是像C那样为了进行好一些计算而编写的一些指令,新代码是一个关于i、pc、i’和pc’的公式(formula),这是理解从C带TLA+的最为关键的环节,即上述这段代码整体就是一个公式

上述代码的意思并非if pc = “start”为真,然后执行then部分,否则执行else部分。其真正含义是如果pc = “start”为真,那么上述整个公式将等于then这个公式的值,否则整个公式将等于else公式的值。

不过我们看到在上面的then子句中存在两个独立的公式,以第一个then为例,两个独立公式分别为i’ ∈ 0..1000和pc’ = “middle”。这两个独立的公式之间是and的关系,我们需要将其转换为一个公式。TLA+中使用”/\”表示and连接,下面是使用”/\”将公式连接后的结果:

if pc = "start"
    then (i' ∈ 0..1000) /\
         (pc' = "middle")
    else if pc = "middle"
            then (i' = i + 1) /\
                 (pc' = "done")
            else no next values
  • 改造else公式

问题来了! 当存在某个状态,使得整个公式等于最后一个else公式的值时,我们发现这个值为”no next values”,而前面的then、else if then公式的值都为布尔值TRUE或FALSE。这里最后的ELSE公式,它的值应该为FALSE,无论i、pc、i’和pc’的值为什么,因此这里直接将其改造为FALSE:

if pc = "start"
    then (i' ∈ 0..1000) /\
         (pc' = "middle")
    else if pc = "middle"
            then (i' = i + 1) /\
                 (pc' = "done")
            else FALSE
  • TLA+的关键字为大写且TLA+源码为ASCII码

if、then、else 这些都是TLA+的关键字,而TLA+的关键字通常为大写,并且TLA+源码为ASCII码,∈需换成\in。这样改变后的结果如下:

IF pc = "start"
    THEN (i' \in 0..1000) /\
         (pc' = "middle")
    ELSE IF pc = "middle"
            THEN (i' = i + 1) /\
                 (pc' = "done")
            ELSE FALSE

到这里,我们就得到了一个美化后的的TLA+公式了!

3.5 干掉if else

前面说过,我们将C代码改造为了一个公式,但公式中依然有if else总是感觉有些格格不入,是不是可以干掉if else呢!我们来试一下!

我们先用A、B替换掉then语句中的两个公式:

IF pc = "start"
    THEN A
    ELSE IF pc = "middle"
            THEN B
            ELSE FALSE

如果整个公式为TRUE,需要(pc = “start”)和A都为TRUE,或(pc = “middle”)和B都为TRUE。TLA+引入一个操作符\/表示or,这样整个公式为TRUE的逻辑就可以表示为:

   ((pc = "start") /\ A)
\/ ((pc = "middle") /\ B)

好了,现在我们再把A和B换回到原先的公式:

   ((pc = "start") /\
    (i' \in 0..1000) /\
    (pc' = "middle"))
\/ ((pc = "middle") /\
    (i' = i+1 ) /\
    (pc' = "done"))

你是不是感觉不够美观啊!TLA+提供了下面等价的、更美观的形式:

\/ /\ pc = "start"
   /\ i' \in 0..1000
   /\ pc' = "middle"
\/ /\ pc = "middle"
   /\ i' = i+1
   /\ pc' = "done"

这种形式完全去掉了括号,并可以像列表一样表达公式!并且无论是/\还是\/都是可交换的(commutative),顺序不影响公式的最终结果。

3.6 完整的TLA+ spec

从数学层面,上面C代码将被拆分为两个公式,一个是初始状态公式,一个是下个状态的公式:

初始状态公式:(i = 0) /\ (pc = "start")
下一状态公式:
              \/ /\ pc = "start"
                 /\ i' \in 0..1000
                 /\ pc' = "middle"
              \/ /\ pc = "middle"
                 /\ i' = i+1
                 /\ pc' = "done"

但对于一个完整的TLA+ spec来说,还需要额外补充些内容:

---- MODULE SimpleProgram ----

EXTENDS Integers
VARIABLES i, pc

Init == (pc = "start") /\ (i = 0)
Next == \/ /\ pc = "start"
           /\ i' \in 0..1000
           /\ pc' = "middle"
        \/ /\ pc = "middle"
           /\ i' = i + 1
           /\ pc' = "done"
====

一个完整的TLA+ spec是放在一个module中的,上面例子中module为SimpleProgram。TLA toolkit要求tla文件名要与module名相同,这样上面代码对应的tla文件应为SimpleProgram.tla。

EXTENDS会导入TLA+内置的标准module,这里的Integers就提供了基础的算术运算符,比如+和..。

VARIABLES声明了状态变量,比如这里的i和pc。变量加上’即表示该变量的下一个状态的值。

接下来便是公式的定义。Init和Next并非固定公式名字,你可以选择任意名字,但使用Init和Next是惯用法。

“====”用于标识一个module的Body内容的结束。

对于上面简单的C程序,这样的spec是可以的。但在实际使用中,spec中的Next一般会很长,一个好的实践是对其进行拆分。比如这里我们就将Next拆分为两个子公式:Pick和Add1:

---- MODULE SimpleProgram ----

EXTENDS Integers
VARIABLES i, pc

Init == (pc = "start") /\ (i = 0)
Pick == /\ pc = "start"
        /\ i' \in 0..1000
        /\ pc' = "middle"
Add1 == /\ pc = "middle"
        /\ i' = i + 1
        /\ pc' = "done"
Next == Pick \/ Add1
====

4. 使用TLA+ Toolkit验证spec

Lamport提供了TLA+的Module Checker,我们可以从其主页提供的工具包下载链接下载TLA+ Toolkit。

先将上面的TLA+ spec存入一个名为SimpleProgram.tla的文件。然后打开TLA+ Toolkit,选择File -> Open spec -> Add New Spec…,然后选择你本地的SimpleProgram.tla即可加载该spec:

之后,我们可以点击菜单项“TLC Model Checker” -> New Model,便可以为该tla建立一个model配置(去掉deadlock),运行check后,你能看到下面结果:

我们看到model check一共检查了2003个不同的状态。

注:TLA+还提供了一个Visual Studio Code的扩展,也可以用来specify和check model。

5. 使用TLA+验证Go并发程序

Go语言因其强大的并发编程能力而备受青睐。然而,Go的并发方案虽然简单,但也并非银弹。随着并发程序复杂性的增加,开发者常常面临着难以发现和调试的错误,如死锁和竞态条件。这些问题不仅影响程序的正确性,还可能导致严重的系统故障。对于Go开发的并发系统的关键部分,采用TLA+进行形式化的验证是一个不错的提高系统正确性和可靠性的方法。

接下来,我们就建立一个生产者和消费者的Go示例,然后使用TLA+为其建模并check。理论上应该是先有设计思路,再TLA+验证设计,再进行代码实现,这里的Go代码主要是为了“描述”该并发程序的需求和行为逻辑。

// go-and-tla-plus/producer-consumer/main.go
package main

import (
    "fmt"
    "sync"
)

func producer(ch chan<- int, wg *sync.WaitGroup) {
    defer wg.Done()
    for i := 0; i < 5; i++ {
        ch <- i
    }
    close(ch)
}

func consumer(ch <-chan int, wg *sync.WaitGroup) {
    defer wg.Done()
    for num := range ch {
        fmt.Println("Consumed:", num)
    }
}

func main() {
    ch := make(chan int)
    var wg sync.WaitGroup
    wg.Add(2)

    go producer(ch, &wg)
    go consumer(ch, &wg)

    wg.Wait()
}

任何Go初学者都可以很容易读懂上面的程序逻辑:Producer生产0到4四个数,每生成一个就通过unbuffered channel发出,consumer从channel接收数字并消费。Producer生产完毕后,关闭channel。Consumer消费完所有数字后,退出,程序终止。

下面是使用TLA+编写的ProducerConsumer的完整Spec:

// go-and-tla-plus/producer-consumer/ProducerConsumer.tla

---- MODULE ProducerConsumer ----
EXTENDS Integers, Sequences

VARIABLES
    ch,           \* 通道内容
    produced,     \* 已生产的消息数
    consumed,     \* 已消费的消息数
    closed        \* 通道是否关闭

TypeOK ==
    /\ ch \in Seq(0..4)
    /\ produced \in 0..5
    /\ consumed \in 0..5
    /\ closed \in BOOLEAN

Init ==
    /\ ch = <<>>
    /\ produced = 0
    /\ consumed = 0
    /\ closed = FALSE

Produce ==
    /\ produced < 5
    /\ ch = <<>>
    /\ ~closed
    /\ ch' = Append(ch, produced)
    /\ produced' = produced + 1
    /\ UNCHANGED <<consumed, closed>>

Close ==
    /\ produced = 5
    /\ ch = <<>>
    /\ ~closed
    /\ closed' = TRUE
    /\ UNCHANGED <<ch, produced, consumed>>

Consume ==
    /\ ch /= <<>>
    /\ ch' = Tail(ch)
    /\ consumed' = consumed + 1
    /\ UNCHANGED <<produced, closed>>

Next ==
    \/ Produce
    \/ Close
    \/ Consume

Fairness ==
    /\ SF_<<ch, produced, closed>>(Produce)
    /\ SF_<<produced, closed>>(Close)
    /\ SF_<<ch>>(Consume)

Spec == Init /\ [][Next]_<<ch, produced, consumed, closed>> /\ Fairness

THEOREM Spec => []TypeOK

ChannelEventuallyEmpty == <>(ch = <<>>)
AllMessagesProduced == <>(produced = 5)
ChannelEventuallyClosed == <>(closed = TRUE)
AllMessagesConsumed == <>(consumed = 5)

====

这个Spec不算长,但也不短,你可能看不大懂,没关系,接下来我们就来说说从main.go到ProducerConsumer.tla的建模过程,并重点解释一下上述TLA+代码中的重要语法。

针对main.go中体现出来的Producer和Consumer的逻辑,我们首先需要识别关键组件:生产者、消费者和一个通道(channel),然后我们需要确定状态变量,包括:通道内容(ch)、已生产消息数(produced)、已消费消息数(consumed)、通道是否关闭(closed)。

接下来,我们就要定义action,即导致状态变化的step,包括Produce、Consume和Close。

最后,我们需要设置初始状态Init和下一个状态Next,并定义安全属性(TypeOK)和一些活性属性(如AllMessagesConsumed等)

现在,我们结合上述TLA+的代码,来说一下上述这些逻辑是如何在TLA+中实现的:

---- MODULE ProducerConsumer ----

这一行定义了模块名称,模块名称与文件名字(ProducerConsumer.tla)要一致,否则TLA+ Toolkit在Open Spec时会报错。

EXTENDS Integers, Sequences

这行会导入整数和序列模块,以使用相关运算符。

VARIABLES
    ch,           \* 通道内容
    produced,     \* 已生产的消息数
    consumed,     \* 已消费的消息数
    closed        \* 通道是否关闭

这里使用VARIBALES关键字定义了四个状态变量,整个TLA+程序的函数逻辑就围绕这四个变量进行,TLC Model check也是基于这些状态变量对TLA+ module进行验证。

TypeOK ==
    /\ ch \in Seq(0..4)
    /\ produced \in 0..5
    /\ consumed \in 0..5
    /\ closed \in BOOLEAN

定义不变量,确保变量状态在系统的所有行为过程中始终保持在合理范围内,该TypeOK不变量即是整个程序的安全属性。

Init ==
    /\ ch = <<>>
    /\ produced = 0
    /\ consumed = 0
    /\ closed = FALSE

这是初始状态的公式,对应了四个变量的初始值。

Produce ==
    /\ produced < 5
    /\ ch = <<>>
    /\ ~closed
    /\ ch' = Append(ch, produced)
    /\ produced' = produced + 1
    /\ UNCHANGED <<consumed, closed>>

这里定义了生产操作的公式,只有在produced < 5,ch为空且closed不为true时,才会生产下一个数字。这里设定ch为空作为前提条件,主要是为了体现Channel的unbuffered的性质。

Close ==
    /\ produced = 5
    /\ ch = <<>>
    /\ ~closed
    /\ closed' = TRUE
    /\ UNCHANGED <<ch, produced, consumed>>

这里定义了关闭操作的公式,这里的ch = <<>>子公式的目的是等消费完之后再关闭channel,当然这里与Go的机制略有差异。

Consume ==
    /\ ch /= <<>>
    /\ ch' = Tail(ch)
    /\ consumed' = consumed + 1
    /\ UNCHANGED <<produced, closed>>

这里定义了消费操作的公式,只有channel不为空,才进行消费。

Next ==
    \/ Produce
    \/ Close
    \/ Consume

这里基于三个操作公式定义了下一个状态(Next)的公式,使用\/运算符将这三个操作连接起来,表示下一步可以执行其中任意一个操作。

Fairness ==
    /\ SF_<<ch, produced, closed>>(Produce)
    /\ SF_<<produced, closed>>(Close)
    /\ SF_<<ch>>(Consume)

这里定义了公平性条件,确保各操作最终会被执行。

Spec == Init /\ [][Next]_<<ch, produced, consumed, closed>> /\ Fairness

这里定义了整个并发程序的规范,包括初始条件Init和下一步动作约束以及Fairness条件。/\连接的第二段Next表示系统的每一步都必须符合Next定义的可能动作,并且不会改变 <<ch, produced, consumed, closed>> 元组中变量之外的其他变量。Fairness 表示系统必须满足前面定义的 Fairness 条件。

THEOREM Spec => []TypeOK

这是一个定理,表示如果系统满足Spec规范,则一定会满足TypeOK这个不变量。其中的”=>”是蕴含的意思,A => B表示如果A为真,那么B必然为真。用一个例子可以解释这点,如果x > 3为真,那么 x > 1 必为真,我们可以将其写为:x > 3 => x > 1。

ChannelEventuallyEmpty == <>(ch = <<>>)
AllMessagesProduced == <>(produced = 5)
ChannelEventuallyClosed == <>(closed = TRUE)
AllMessagesConsumed == <>(consumed = 5)

这里定义了四个活性属性,用于在TLC Model check时验证最终状态使用,其中:ChannelEventuallyEmpty表示最终消息队列 ch 一定会为空;AllMessagesProduced表示最终一定会生产5条消息;ChannelEventuallyClosed表示最终消息队列一定会被关闭;AllMessagesConsumed表示最终一定会消费5条消息。

接下来,我们可以使用前面提到的TLA+ Toolbox来check该spec,下面是model的设置和model check的结果:


model设置


check结果

注:在VSCode中使用TLA+插件的Checker对上述tla进行check,会出现不满足活性属性的error结果。

6. 小结

在这篇文章中,我们从Lamport提供的C语言代码示例出发,一步步介绍了如何将其转换为TLA+ spec,并使用TLA+ Toolkit进行验证。然后我们又以一个Go语言的生产者-消费者并发程序为例,展示了如何使用TLA+对其进行建模和验证。

不过我必须承认,TLA+这种形式化验证语言是极小众的。对大多数程序员来说,可能没什么实际帮助。即便是在大厂,真正使用TLA+对分布式系统进行形式化验证的案例也很少。

但是,我认为TLA+仍然有其独特的价值:

  • 它迫使我们用更抽象和精确的方式思考系统设计,有助于发现潜在的问题。
  • 对于一些关键的分布式系统组件,使用TLA+进行验证可以极大地提高可靠性。
  • 学习TLA+的过程本身就是一次提升系统设计能力的过程。

当然,形式化方法并非万能。比如它无法解决性能退化等问题,也不能验证代码是否正确实现了设计。我们应该将其视为系统设计和验证的补充工具,而不是替代品。

总之,虽然TLA+可能不适合所有人,但对于那些构建复杂分布式系统的工程师来说,它仍然是一个值得学习和使用的强大工具。我希望这篇文章能为大家了解和入门TLA+提供一些帮助。

本文涉及的源码可以在这里下载 – https://github.com/bigwhite/experiments/blob/master/go-and-tla-plus

本文部分源代码由claude 3.5 sonnet生成。

7. 参考资料


Gopher部落知识星球在2024年将继续致力于打造一个高品质的Go语言学习和交流平台。我们将继续提供优质的Go技术文章首发和阅读体验。同时,我们也会加强代码质量和最佳实践的分享,包括如何编写简洁、可读、可测试的Go代码。此外,我们还会加强星友之间的交流和互动。欢迎大家踊跃提问,分享心得,讨论技术。我会在第一时间进行解答和交流。我衷心希望Gopher部落可以成为大家学习、进步、交流的港湾。让我相聚在Gopher部落,享受coding的快乐! 欢迎大家踊跃加入!

img{512x368}
img{512x368}

img{512x368}
img{512x368}

著名云主机服务厂商DigitalOcean发布最新的主机计划,入门级Droplet配置升级为:1 core CPU、1G内存、25G高速SSD,价格5$/月。有使用DigitalOcean需求的朋友,可以打开这个链接地址:https://m.do.co/c/bff6eed92687 开启你的DO主机之路。

Gopher Daily(Gopher每日新闻) – https://gopherdaily.tonybai.com

我的联系方式:

  • 微博(暂不可用):https://weibo.com/bigwhite20xx
  • 微博2:https://weibo.com/u/6484441286
  • 博客:tonybai.com
  • github: https://github.com/bigwhite
  • Gopher Daily归档 – https://github.com/bigwhite/gopherdaily

商务合作方式:撰稿、出书、培训、在线课程、合伙创业、咨询、广告合作。

如发现本站页面被黑,比如:挂载广告、挖矿等恶意代码,请朋友们及时联系我。十分感谢! Go语言第一课 Go语言精进之路1 Go语言精进之路2 Go语言编程指南
商务合作请联系bigwhite.cn AT aliyun.com

欢迎使用邮件订阅我的博客

输入邮箱订阅本站,只要有新文章发布,就会第一时间发送邮件通知你哦!

这里是 Tony Bai的个人Blog,欢迎访问、订阅和留言! 订阅Feed请点击上面图片

如果您觉得这里的文章对您有帮助,请扫描上方二维码进行捐赠 ,加油后的Tony Bai将会为您呈现更多精彩的文章,谢谢!

如果您希望通过微信捐赠,请用微信客户端扫描下方赞赏码:

如果您希望通过比特币或以太币捐赠,可以扫描下方二维码:

比特币:

以太币:

如果您喜欢通过微信浏览本站内容,可以扫描下方二维码,订阅本站官方微信订阅号“iamtonybai”;点击二维码,可直达本人官方微博主页^_^:
本站Powered by Digital Ocean VPS。
选择Digital Ocean VPS主机,即可获得10美元现金充值,可 免费使用两个月哟! 著名主机提供商Linode 10$优惠码:linode10,在 这里注册即可免费获 得。阿里云推荐码: 1WFZ0V立享9折!


View Tony Bai's profile on LinkedIn
DigitalOcean Referral Badge

文章

评论

  • 正在加载...

分类

标签

归档



View My Stats