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

基本型別

函式

遞迴函式

尾遞迴

使用累加器改進尾遞迴函式

簡單控制流：if - then - else

繫結

綁定範圍

簡單控制流：`if - then - else`