ATSプログラミング入門

Hongwei Xi


ATS Trustful Software, Inc.

この本は Introduction to Programming in ATS の日本語訳です。 日本語訳の維持管理は JATS-UG - Japan ATS User Group が行なっています。 翻訳に参加するには ATS2公式マニュアルの日本語訳 を参照してください。

プログラミング言語としての ATS は豊かな構文と機能を両立しています。 この本では ATS の中心となる機能を読者に解説します。 それらは基本的な関数型プログラミング、単純な型、(再帰的に定義された) データ型、多相型、依存型、線形型、定理証明、定理証明によるプログラミング (PwTP)、そしてテンプレートを使ったプログラミングなどです。 一般的なプログラミングに馴染みのある読者を仮定してませんが、この本は相当のプログラミング経験のない読者には少し難しいかもしれません。

All rights are reserved. Permission is granted to print this document for personal use.


Dedication

Jinning、Zoe そして Chloe へ。

Table of Contents
前書き
I. 関数型プログラミングの基本
1. はじめる前に
実行可能なプログラム
1つのファイルで構成されたプログラムのひな形
Makefileのひな形
2. プログラミングの構成要素
式と値
名前と束縛
束縛のスコープ
評価のための環境
静的な意味論
プリミティブ型
タプルとタプル型
レコードとレコード型
条件式
シーケンス式 (逐次実行)
コード中のコメント
3. 関数
単純な抽象としての関数
関数のアリティ (arity)
関数インターフェイス
関数呼び出しの評価
再帰関数
再帰関数呼び出しの評価
例: コインチェンジ遊び
末尾呼出と末尾再帰
例: エイト・クイーンパズル
相互再帰関数
相互に定義された末尾再帰
無環境関数とクロージャ関数
高階関数
例: 二分探索遊び
例: 高階関数パズル
カリー化とアンカリー化
4. データ型
パターン
パターンマッチ
マッチ節とケース式
列挙データ型
再帰的に定義されたデータ型
網羅的なパターンマッチ
例: 2分探索木
例: 整数式の評価
5. パラメータ多相
関数テンプレート
多相関数
多相データ型
例: リストに対する関数テンプレート
例: リストのマージソート
II. 現実のプログラミングに対するサポート
6. 効果 (effect) を持つプログラミングの機能
例外
例: ブラウンツリーの判定
参照
例: カウンタの実装
配列
例: 順序をつけた置換 (Ordering Permutations)
行列
例: 定数Piの推量
単純な入力と出力
7. モジュール性
仕様としての型
ATS の静的/動的ファイル
総称テンプレート実装
特殊テンプレート実装
抽象型
例: 有理数パッケージ
例: ファンクタを用いた有理数パッケージ
8. C言語との相互呼び出し
外部のグローバル名
ATS における外部の型と値
ATS に外部コードを含める
ATS における外部関数呼び出し
安全ではないC言語スタイルのATSプログラミング
ATS の型をエクスポートしてC言語から使う
例: 静的に確保されたリストをコンストラクトする
III. 依存型を使ったプログラミング
9. 依存型入門
仕様に対する表現力の強化
型検査中での制約解決
例: 文字列処理
例: 配列の二分探索
再帰関数の停止性検査
例: 依存型を使ったデバッグ
10. データ型の改良
依存データ型
例: リストに対する関数テンプレート (再)
例: リストのマージソート (再)
パターンマッチの連続性
例: 関数的な赤黒木
11. ATS/LF を使った定理証明
データ命題 (dataprop) として関係をエンコードする
全域関数を使って証明を組み立てる
例: 乗法の分配法則
例: 乗法の交換法則
代数的なデータ種 (datasort)
例: ブラウンツリーの性質を確立する
プログラマ中心の定理証明
12. 定理証明によるプログラミング
非線形の制約を回避する
例: 安全な行列の添字演算
強化された正確性を使って明記する
例: もう一つの検証された階乗
例: 検証された高速な累乗
IV. 線形観と線形型を使ったプログラミング
13. 観 (view) と観型入門
ポインタを通じたメモリアクセスのための観
観と型を組み合わせた観型
左辺値と参照渡し
スタックに確保された値
ヒープに確保された線形クロージャ関数
14. 線形なデータ命題としてのデータ観 (dataview)
オプショナル観
選言的な観
線形配列のデータ観
線形文字列のデータ観
片方向リストのデータ観
観変化のための証明関数
15. 線形データ型としてのデータ観型 (dataviewtype)
線形オプショナル値
線形リスト
例: 線形リストのマージソート
例: 線形リストの挿入ソート
例: 線形リストのクイックソート
線形2分探索木
データ型からデータ観型への翻訳
16. 抽象観と観型 (viewtype)
単純な線形オブジェクト
メモリの確保と解放
例: 配列を用いたリングバッファ
ロックとアンロック
非同期 IPC のための線形チャネル
V. 関数テンプレートを使ったプログラミング
17. ジェネリックスから遅延束縛へ
テンプレート実装のジェネリックス
例: 数に対するジェネリックス演算
ファンクタの特殊形としてのテンプレート
例: ループ生成のためのテンプレート
テンプレートを用いた遅延束縛のサポート