HN 日本語サマリー

← 一覧へ戻る
プログラミング

ATSでのプログラミング入門

Introduction to Programming in ATS (ats-lang.sourceforge.net)

76 pointsby ibobev9 コメント

要約

ATSは構文と機能が豊富なプログラミング言語であり、この書籍は基本的な関数型プログラミング、型システム、定理証明、テンプレートベースのプログラミングなど、その中核的な機能を解説します。プログラミング経験がない読者も想定していますが、経験者にとっては内容が濃いものとなるでしょう。

全文翻訳

ATSでのプログラミング入門

Hongwei Xi

ATS Trustful Software, Inc.

Copyright © 2010-201? Hongwei Xi

プログラミング言語として、ATSは構文が豊富で機能も豊富です。この書籍は、読者にATSのいくつかのコア機能を紹介します。これには、基本的な関数型プログラミング、単純型、(再帰的に定義された)データ型、多相型、依存型、線形型、定理証明、定理証明を用いたプログラミング（PwTP）、およびテンプレートベースのプログラミングが含まれます。読者はプログラミング全般に精通している必要はありませんが、かなりのプログラミング経験がない読者にとっては、この書籍はかなり密度の高いものになるでしょう。

すべての権利は留保されています。個人的な使用のためにこのドキュメントを印刷する許可が与えられます。

献辞

Jinning, Zoe, Chloeへ。

目次

前書き

I. 基本的な関数型プログラミング

  1. 開始のための準備

実行中のプログラム

単一ファイルプログラムのテンプレート

Makefileテンプレート

  1. プログラミングの要素

式と値

名前と束縛

束縛のスコープ

評価のための環境

静的意味論

プリミティブ型

タプルとタプル型

レコードとレコード型

条件式

シーケンス式

コード内のコメント

  1. 関数

抽象化の単純な形式としての関数

関数の項数

関数インターフェース

関数呼び出しの評価

再帰関数

再帰関数呼び出しの評価

例: コインチェンジ問題

末尾呼び出しと末尾再帰

例: 8クイーン問題

相互再帰関数

相互定義された末尾再帰

環境なし関数とクロージャ関数

高階関数

例: 二分探索

例: 高階関数パズル

カリー化と非カリー化

  1. データ型

パターン

パターンマッチング

マッチング節とcase式

列挙型データ型

再帰的に定義されたデータ型

パターンマッチングの網羅性

例: 二分探索木

例: 整数式の評価

  1. パラメトリック多相性

関数テンプレート

多相関数

多相データ型

例: リスト上の関数テンプレート

例: リストのマージソート

II. 実用的なプログラミングのためのサポート

  1. 副作用のあるプログラミング機能

例外

例: ブラウン木 (Braun Tree) のテスト

参照

例: カウンターの実装

配列

例: 置換の順序付け

行列

例: 円周率の推定

単純な入出力

  1. モジュール性

仕様の形式としての型

静的ATSファイルと動的ATSファイル

汎用テンプレート実装

特定テンプレート実装

抽象型

例: 有理数パッケージ

例: 有理数のファンクタパッケージ

  1. C言語との相互作用

外部グローバル名

ATSにおける外部型と値

ATSへの外部コードの包含

ATSからの外部関数呼び出し

ATSでの安全でないCスタイルプログラミング

C言語で使用するためのATSでの型の公開

例: 静的に割り当てられたリストの構築

III. 依存型を用いたプログラミング

  1. 依存型入門

仕様のための表現力の強化

型チェック中の制約ソルバー

例: 文字列処理

例: 配列上の二分探索

再帰関数の終端チェック

例: デバッグのための依存型

  1. データ型の洗練

依存データ型

例: リスト上の関数テンプレート (再訪)

例: リストのマージソート (再訪)

パターンマッチングの逐次性

例: 関数型赤黒木

  1. ATS/LFにおける定理証明

関係性のデータプロップとしてのエンコーディング

総関数としての証明の構築

例: 乗法の分配法則

例: 乗法の可換性

代数的データソート

例: ブラウン木上の性質の確立

プログラマー中心の定理証明

  1. 定理証明を用いたプログラミング

非線形制約の回避

例: 安全な行列添え字

より精密な仕様記述

例: 別の検証済み階乗関数

例: 検証済みの高速べき乗計算

IV. ビューとビュー型を用いたプログラミング

  1. ビューとビュー型入門

ポインタ経由のメモリアクセスビュー

ビューと型の組み合わせとしてのビュー型

左辺値と参照渡し

スタック割り当て変数

ヒープ割り当て線形クロージャ関数

  1. データビューとしての線形データプロップ

オプションビュー

選言ビュー

線形配列のためのデータビュー

線形文字列のためのデータビュー

単方向連結リストのためのデータビュー

ビュー変更のための証明関数

  1. データビュー型としての線形データ型

線形オプショナル値

線形リスト

例: 線形リストのマージソート

例: 線形リストの挿入ソート

例: 線形リストのクイックソート

線形二分探索木

データ型からデータビュー型への移行

  1. 抽象ビューとビュー型

単純な線形オブジェクト

メモリ割り当てと解放

例: 配列ベースの循環バッファ

ロックとアンロック

非同期IPCのための線形チャネル

V. 関数テンプレートを用いたプログラミング

  1. 汎用性から遅延バインディングへ

テンプレート実装の汎用性

例: 数値に対する汎用操作

ファンクタの特殊な形式としてのテンプレート

例: ループ構築のためのテンプレート

遅延バインディングのためのテンプレートベースのサポート

次へ
前書き