ATS：用定理证明编程/语言基础

基本类型

ATS 中的基本类型基本上是 C 类型的一种表示形式。ATS 中的每种类型都可以映射到 C 中的类型。映射如下所示

ATS 类型	C 类型
void	void
bool	int
char	char
schar	signed char
uchar	unsigned char
int	int
uint	unsigned int
lint	long int
ulint	unsigned long int
llint	long long int
ullint	unsigned long long int
float	float
double	double
size_t	size_t
string	string

这些类型的映射可以在文件 ats_types.h 中找到。
请注意，类型文字的工作方式与 C 相同，因此 3.14 是一个双精度数，而 3.14F 是一个浮点数。

函数

函数由关键字 fn 声明。函数的一般格式为

fn functionName( ''param_1'': ''type_1'', ''param_2'': ''type_2'',..., ''param_n'': ''type_n'' ): ''return_type'' = ''function_body''

函数没有返回值语句，而是函数体是一个表达式，该表达式求值为返回值。例如，一个用来添加两个值的函数将类似于

fn add( operand1: int, operand2: int ) = int1 + int2

递归函数

一个调用自身的函数称为递归函数。递归函数与通用函数具有相同的结构，唯一的区别是关键字 fun 替换了关键字 fn。递归函数的一个例子是用来计算斐波那契值的函数

fun fibonacci( n: int ): int =
    if ( n > 2 ) then fibonacci( n - 1 ) + fibonacci( n - 2 ) else n

尾递归

递归的一种特殊情况是尾递归。当递归调用的返回值用作调用函数的返回值时，就会发生这种情况。例如

fun even( n: int ): bool =
    if ( n == 0 ) then true
    else if ( n == 1 ) then false
    else even( n - 2 )

函数 even 用于判断一个数字是否为偶数。even 的返回值可以是 true、false，或者由调用 even( n - 2 ) 返回的值。由于调用返回值在没有进一步处理的情况下被返回，因此对 even( n - 2 ) 的递归调用是一个尾递归调用。
尾递归尤其重要，因为它可以通过一种称为尾调用优化的方法转换为循环。这意味着由于函数调用不会导致性能损失，因此尾递归可以与 for 或 while 循环一样快。

使用累加器改进尾递归函数

递归函数提供了一种优雅的编程风格，但它们有一个问题：每次调用都会将一些数据放入堆栈中。这意味着，当递归函数多次调用自身时，可能会发生堆栈溢出异常。尾递归在理论上存在相同的问题，但是由于尾调用优化，该问题在实践中不会发生；尾递归函数不会发生堆栈溢出。
考虑到尾递归的优先地位，一个显而易见的问题是是否总是可以使用递归函数而不是非递归函数。事实证明，通过向递归函数添加额外的参数（称为累加器），任何算法都可以使用尾递归实现。这些参数的目的是累积来自先前调用的信息（因此得名），并将其传递到不同的递归调用中。
例如，考虑实现阶乘的代码

fun factorial( n: int ): int =
    if ( n == 1 ) then 1
    else n * factorial( n - 1 )

这是一个明显的阶乘实现，它也是递归的，但不是尾递归。为了创建一个尾递归版本，我们将一个累加器添加到我们的函数中；这个累加器将包含到目前为止计算出的阶乘的值

fun factorial2( n: int, accumulator: int ): int =
    if ( n == 1 ) then accumulator
    else factorial( n - 1, accumulator * n )

现在，因为我们需要我们的阶乘函数只有一个参数，所以我们添加一个额外的函数，它将成为我们的阶乘函数，来初始化累加器并启动递归

fn factorial( n: int ): int =
    factorial2( n - 1, accumulator * n )

借助累加器，任何非尾递归函数都可以转换为尾递归函数。

简单控制流：if - then - else

ATS 中的控制流与其他函数式编程语言一样，与遵循结构化编程的语言在实现方式上有所不同。但是，有一个经典的结构，它的结构在 ATS 中与在命令式语言中完全相同：if - then - else。一般结构为

if ''boolean_expression'' then
 ''expression1''
else
 ''expression2''

fn factorial( n: int ): int =
    factorial2( n - 1, accumulator * n )

绑定

绑定是一个常量值，它是使用表达式的结果定义的。它可以与 C/C++ 中的 const 或 Java 中的 final 相比较。ATS 中的绑定使用关键字 val 声明。绑定的示例可以是 val foo = 1 或 val bar = 2 * 2。名称绑定来源于我们将名称 foo 和 bar 绑定到表达式 1 和 2 * 2。绑定也可以使用其他绑定定义

val x = 10
val square = x * x

在这种情况下，x 显然会在 square 之前初始化。
请注意，声明的绑定没有类型。实际上，使用 val 声明的绑定将从其绑定的表达式中获取其类型。可以更加严格，并为绑定显式设置类型。例如，绑定 val pi = 3.14 定义了一个双精度数，因为表达式 3.14 默认情况下是一个双精度数。如果我们写 val pi = 3.14f，那么 pi 将是一个浮点数。可以通过 val pi: float = 3.14 来指定 pi 必须始终是一个浮点数。如果分配不兼容的类型，例如在 val pi: char = 3.14 中，将会发生编译错误。
一个类似但略有不同的情况是，将类型分配给表达式，而不是绑定。这可以通过编写类似 val pi = 3.14: float 来实现。在这种情况下，浮点类型被赋予表达式。因此，尽管最终我们的绑定始终是一个浮点数，但过程略有不同。

绑定范围

绑定在某些特定边界内可见。这些边界定义了绑定的范围。在范围内，绑定可以被声明、初始化和使用。
绑定范围的最高级别是顶层：在此级别，绑定不在函数内，它在文件中的所有点可见，从声明绑定点开始

fn area( radius: float): float = radius * radius * pi

val pi = 3.14

fn circumference( radius: float ): float = radius * 2 * pi

我们无法在 area 中使用 pi，因此我们的实现是一个错误；但我们可以从 circumference 中使用它。
在更低的级别，我们有局部绑定，它们在一段代码内定义。局部绑定可以用两种方式使用。
第一种方式是作为帮助来评估表达式。在这种情况下，绑定中使用的名称可用于构成其他表达式。在这种情况下的一般结构为

val ''expression_name'' = let
 val ''name_1'' = ''value_1'' and ''name_2'' = ''value_2'' and ... and ''name_n'' = ''value_n'' in ''expression_to_evaluate''
end

在这种情况下，我们有不同的名称 name_1，...，name_n 用于评估表达式 expression_to_evaluate。也就是说，绑定在 in 和 end 之间有效。例如

val area = let
    val pi = 3.14 and radius = 10 in pi * radius * radius
end

另一种具有类似结果的结构如下所示

val expression_name = expression_to_evaluate where {
    val name_1 = value_1 and name_2 = value_2 and ... and name_n = value_n
} end

在这种情况下，我们首先定义表达式，然后声明绑定。绑定在 '=' 和 where 之间有效。因此，上面的例子变为

val area = pi * radius * radius where {
    pi = 3.14 and radius = 10
} end

第二种方式是定义一个或多个顶层绑定

local
val ''name_1'' = ''value_1'' and ''name_2'' = ''value_2'' and ... and ''name_n'' = ''value_n''
in
val ''expression_name'' = ''expression_to_evaluate''
end

虽然局部绑定只能在 'in' 和 end 之间使用，但结果表达式的绑定是顶层绑定。因此，例如

local
val pi = 3.14 and radius = 10
in
val area = pi * radius * radius
val circumference = pi * 2 * radius
end