Japan ATS User Group (JATS-UG)は、日本における ATS言語の利用促進と、日本語での情報交換を目的としたユーザーグループです。主な活動として ATS言語に関するドキュメントを公開しています。

ATS言語とは

やわらかい説明

ATS言語のプログラムは大きく3つの要素から成り立っています。動的な世界(Dynamics)、静的な世界(Statics)、証明の世界(Proofs)です。動的な世界は通常のプログラミング言語と同じ実際に実行されるロジックです。動的な世界はATSコンパイラによってC言語に変換され、GCCによって実行バイナリになります。静的な世界はHaskellやOCamlのような型推論を持つ言語における型のことです。静的な世界は実行時エラーを防ぐ目的で、型の力で動的な世界を制約します。証明の世界は依存型(Prop)と線形型(View)に分類できます。依存型はCoqのような証明器として使うことができ、動的な世界のロジックに証明を与えることができます。線形型はリソースを取り扱うことができ、例えばGCに頼らない動的な世界によるメモリ領域の管理を安全に行なうことができます。動的な世界はコンパイルされて実行バイナリになりましたが、静的な世界と証明の世界はATSによるコンパイル時に評価(型検査)され、実行バイナリにはなりません。しかし、静的な世界と証明の世界の検査に失敗すると、動的な世界のコンパイルも中止されます。これが「静的な世界と証明の世界は動的な世界を制約する」という意味です。

この制約による安全性の担保はプログラマの力に頼っています。もしプログラマが動的な世界だけを使ってATSプログラミングを行なったら、C言語と同等の安全性しか手に入りません。プログラマが静的な世界と証明の世界を駆使して制約を強めれば強めるほど、動的な世界の安全性は強固なものになります。これはプログラマを中心にすえたプログラムの検証方法で、定理証明によるプログラミング(PwTP)と呼ばれます。

少し脱線しますが、上図ではATSの動的な世界はC言語へと変換されています。しかしこのATSのコンパイル結果の対象はC言語に限りません。現時点ではC言語バックエンドの他に JavaScriptやPython をC言語の代わりにバックエンドとして使うことができます。さらにATSプログラムをJavaScriptに変換できることで、ATSプログラムをWebブラウザ上で動作させることさえできます。

硬い説明

(以下の説明はATS本家トップページ http://www.ats-lang.org/ の翻訳です。)

ATSとは何ですか？

ATS言語は静的型付けのプログラミング言語で、形式的な仕様で統一されています。 Applied Type Systemフレームワークを基礎とする表現力豊かな型システムを持ち、またそれは言語の名前にもなっています。具体的には依存型と線形型をATSでは使うことができます。

ATS2 (ATS/Postiats) の今の実装は ATS1 (ATS/Anairiats) で設計され、そのコード行数は150K行強です。 ATSは時間効率と空間効率についてC/C++言語と同じくらい効率的です。また多様なプログラミングパラダイムをサポートしています。

関数型プログラミング: ATSのコアはMLの影響を受けた即時評価(call-by-value)の関数型言語です。 ATSにおける線形型は主にC言語と比較しても遜色ない効率の関数型プログラムを書くことに利用されますが、同様にC言語と比較しても遜色なく小さなフットプリントを実現するためにも利用されます。
命令型プログラミング: ATSの命令型プログラミングに対するユニークなアプローチは 定理証明によるプログラミング(PwTP) のパラダイムを基礎としています。 ATSの型システムは他の言語では危険であると考えられている多くの機能を安全に提供します。 (例えば、明示的なポインタ演算や明示的なメモリの取得/解放などです) これはATSを使った高品質な低レイヤーのシステムプログラミングを可能にします。
並列プログラミング: ATSはマルチスレッドプログラミングをサポートしていて、安全にpthreadを使えます。リソースに対する追跡と安全な操作に線形型を利用することで、マルチコアアーキティクチャを生かした信頼性の高いプログラムを作成できます。
モジュラープログラミング: ATSのモジュールシステムはModula-3の影響を大きく受けています。それはシンプルで総称的で、同時に大規模なプログラミングをサポートするのに効果的です。

その上に、ATSはATS/LFというサブシステムを含んでいます。これは全域関数を使って構築された証明について、対話的な定理証明をサポートします。これによってATSは、プログラミングと定理証明を構文によって組み合わせて、プログラムの検証に対してプログラマ中心のアプローチを提供します。さらにATS/LFは、メタな性質の証明と一緒に(論理体系や型システムのような)様々な形式的体系をエンコードするための論理フレームワーク(logical framework (LF))としての役目を果たします。

ATSは何に向いているのか

ATSは現実的なプログラミングの正確さを強化できます。
ATSは改良に基づくソフトウェア開発を促進します。
ATSでは効率的な関数型プログラミングをすることができます。にもかかわらず生のアンボックス化されたデータ表現を直接操作できます。
ATSの線形型を使うことでプログラムのメモリのフットプリントを削減できます。
ATSでは証明器を使うことでプログラマがプログラムの安全性と効率を向上させることができます。
ATSを使えばOSのkernelのような低レイヤーのコードを安全に書くことができます。
ATSは型理論を教えたり、高品質なソフトウェアを構築する際の型の力と可能性を教えるのを助けます。

ATSの学習に際しての提案

ATSは (C++のように) 機能豊富です。 MLをベースにした関数型プログラミングとC言語をベースにした命令型プログラミングの知識はATSの学習に役立つでしょう。一般に、ATSにおいて多くの馴染みのないプログラミングの概念と機能に出会うことに予期しておくべきです。またそれらを学習するのに長い時間がかかることを覚悟してください。うまくいけば、大きく複雑なシステムを最小のデバッグで実装することを楽しめる、自信に満ちたプログラマになれるでしょう。

最初の一歩

なにはともあれ使ってみましょう。インストール手順については公式wiki も参考にしてください。

1. ダウンロード

http://sourceforge.net/projects/ats2-lang/files/ と http://sourceforge.net/projects/ats2-lang-contrib/files/ から最新バージョンのATS2-PostiatsとATS2-Postiats-contribをダウンロードしてください。

2. インストール

Linuxの場合

ここではDebian GNU/Linuxを例に説明します。はじめに、ATS2のインストールに必要なパッケージをインストールします。

$ sudo apt-get install gcc libgc-dev libgmp-dev make

次に、先程ダウンロードしたATS2-PostiatsとATS2-Postiats-contribを解凍し、環境変数を設定します。

$ tar xf ATS2-Postiats-X.Y.Z.tgz
$ export PATSHOME=`pwd`/ATS2-Postiats-X.Y.Z
$ export PATH=${PATSHOME}/bin:${PATH}
$ tar xf ATS2-Postiats-contrib-X.Y.Z.tgz
$ export PATSHOMERELOC=`pwd`/ATS2-Postiats-contrib-X.Y.Z

最後に、ATSコンパイラをコンパイルします。

$ cd ${PATSHOME}
$ ./configure
$ make

Windowsの場合

ATS2をWindowsにインストールするにはCygwinが必要です。はじめに、次のリストに挙げたパッケージをsetup-x86.exeもしくはsetup-x86_64.exeを使ってインストールします。

gcc-core
libgc-devel
libgmp-devel
make

次にCygwinコンソール上で、先程ダウンロードしたATS2-PostiatsとATS2-Postiats-contribを解凍し、環境変数を設定します。

$ tar xf ATS2-Postiats-X.Y.Z.tgz
$ export PATSHOME=`pwd`/ATS2-Postiats-X.Y.Z
$ export PATH=${PATSHOME}/bin:${PATH}
$ tar xf ATS2-Postiats-contrib-X.Y.Z.tgz
$ export PATSHOMERELOC=`pwd`/ATS2-Postiats-contrib-X.Y.Z

最後に、ATSコンパイラをコンパイルします。

$ cd ${PATSHOME}
$ ./configure
$ make

Mac OS Xの場合

はじめに、Homebrewを使って、ATS2のインストールに必要なパッケージをインストールします。

$ brew install gmp bdw-gc

次に、先程ダウンロードしたATS2-PostiatsとATS2-Postiats-contribを解凍し、環境変数を設定します。

$ tar xf ATS2-Postiats-X.Y.Z.tgz
$ export PATSHOME=`pwd`/ATS2-Postiats-X.Y.Z
$ export PATH=${PATSHOME}/bin:${PATH}
$ tar xf ATS2-Postiats-contrib-X.Y.Z.tgz
$ export PATSHOMERELOC=`pwd`/ATS2-Postiats-contrib-X.Y.Z

最後に、ATSコンパイラをコンパイルします。

$ cd ${PATSHOME}
$ ./configure
$ make GCFLAG=-D_ATS_NGC

3. コンパイル

Hello Worldプログラムをコンパイルして動かしましょう。

$ vi hello.dats
implement main0 () = println! ("Hello world!")
$ patscc -o hello hello.dats
$ ls
hello  hello.dats  hello_dats.c
$ ./hello
Hello world!

ドキュメント

JATS-UGではATS言語に関するドキュメントを公開しています。

翻訳

ATS言語に関する英語記事の翻訳を行なっています。主な翻訳文書へのリンクを紹介します。より詳しくは https://github.com/jats-ug/translate 以下の文書を参考にしてください。また、翻訳作業に参加していただけるボランティアも募集しています。

ATS公式ドキュメントの翻訳

3つの文書 ATSプログラミング入門, ATSプログラミングチュートリアル, Effective ATS を翻訳/公開しています。特に「ATSプログラミング入門」はATS言語のユーザにとって、もっとも詳しいマニュアルです。これらの文書の詳細は翻訳リポジトリを参照してください。

WebにあるATS言語に関する記事の翻訳

公式サイト以外にも有用な情報がWeb上にはあります。特に MLプログラマ向けATS言語ガイドはATS言語の概要についてうまく解説しています。またATSユーザである Chris Doubleさんのブログ (BLUISH CODER)も参考になります。しかしこのブログの記事はATS2ではなく主にATS1を解説しています。これらの記事の詳細は翻訳リポジトリを参照してください。

ATS言語に関する論文の翻訳

ATSはApplied Type Systemという比較的新しい型理論を基礎としています。この型理論の初出論文が Applied Type System (Extended Abstract) です。その他の論文については翻訳リポジトリを参照してください。

JATS-UGによる文書

ATS言語への敷居を下げることを目的にして、翻訳文書よりも入門向けの文書をいくつか公開しています。

ATS Programming Foundations - OCamlの著名な入門書であるプログラミングの基礎を題材とした入門書です
禅問答的に #ATS2 の型理論を説明してみたよ - 他の言語と比較して理解しにくいATS言語の型システムを直感的に解説しています

ATSに関連するプレゼン資料も以下にまとめています。