ML programmer's guide to ATS translated into Japanese

Posted on December 23, 2013 / Tags: ats, translation

Table of contents


This article is a part of Theorem Prover Advent Calendar 2013 - Qiita [キータ].

Do you know about ATS language http://www.ats-lang.org/? It has both dependent type and linear type, and to be theorem prover also theorem prover. It supports a variety of programming paradigms that include:

Additionally, Hello World program binary compiled by ATS is very small as 23kB.

$ cat hello.dats
val _ = print ("Hello, world!\n")
implement main () = ()
$ atscc -o hello hello.dats
$ ./hello
Hello, world!
$ ldd hello | wc -l
3
$ nm hello | grep -c " U "
24
$ size hello
   text    data     bss     dec     hex filename
  21895     908     200   23003    59db hello

One compiled by Ajhc is 16kB, that is smaller than ATS’s. However, ATS also has good feature for embedded system.

$ cat Hello.hs
main = putStrLn "Hello, world!"
$ ajhc Hello.hs -o Hello
$ ./Hello
Hello, world!
$ ldd Hello | wc -l
3
$ nm Hello | grep -c " U "
19
$ size Hello
   text    data     bss     dec     hex filename
  14056    1337     528   15921    3e31 Hello

…While writing this article, Hongwei Xi said that ATS2 has move effective feature.

$ cat hello.dats
implement
main0 () = {
  val () = println! ("Hello world!")
}
$ patscc -o hello hello.dats
$ ./hello
Hello world!
$ ldd hello | wc -l
3
$ nm hello | grep -c " U "
6
$ size hello
   text    data     bss     dec     hex filename
   3473     724      32    4229    1085 hello

Furthermore, ATS is two times slower than C langugage at worst (on Computer Language Benchmarks Game). That is to say ATS is fast!

However, any infomation about the ATS lanugage aren’t found in Japan… At beginning, let’s try to translate ML programmer’s guide to ATS - liulk @ cs-people into Japanese, to become ATS kung-fu. De-gesso!


This blog post will not be refreshed, because I decided to put any translation about ATS into github repository. Please see https://github.com/jats-ug/translate/blob/master/Web/cs.likai.org/ats/ml-programmers-guide-to-ats.md.

MLプログラマ向けATS言語ガイド

このガイドではATS (Applied Type System) でのプログラミング作法を解説はしません。 それでも、熟練のMLプログラマであればすぐにATSの用語を理解してATSのコードを読み始めることができると思います。

ATSのすばらしき世界

ATSでは、3つの世界でプログラミングをすることを覚えておくと良いでしょう。

ATSの前身であるDependent MLでは、静的な世界からは依存型を通して動的な世界を見るしかありませんでした。 動的なそれぞれの式は静的な式によって指定された型を持っています。 静的な制約は静的な式の集合によって形成され、 型検査はそれらの制約が充足可能であるかどうか調べます。

ATSは依存型に加えて証明を使うことができ、 静的な世界をより強く動的な世界に関与させることができます。 プログラマが動的な式と対応する証明の項を混じり合って書くことができるのです。 証明はpropと呼ばれるclassical propositions(古典論理)や、 viewと呼ばれるlinear propositions(linear logic)(線形論理) のどちらかを取ります。

Prologに馴染んだ人にとっては、propを定義するのはPrologの述語を定義することとよく似ています。 しかし、型検査は自動的にその述語の解決をしてくれません。 プログラムを記述するのと同じように、証明も手動で書き下す必要があります。 証明の記述をすることで、ATSを証明器として使うことができます。

最後に、動的な世界と静的な世界の分離については 「動的な項の種は静的な種によって特徴づけられる」 と考えることもできます。

ノート: 線形論理(Linear Logic)について

線形論理は、弱化規則と縮約規則という構造規則を許可しないという点で古典論理と異なります。 弱化規則は事実(fact)を与えて未使用のままに放置させません。 縮約規則は事実を複数回使用することを許しません。 つまり、事実はきっちり一度だけしか使えないのです。

viewはその意味では線形論理です。 一般にviewの証明は、リソースの所有の追跡やリソースの状態の更新に使われます。

拡張子

ATSで用いられるファイルはいくつかの拡張子を持っています。

.datsファイルと.satsファイルの特筆すべき違いは、関数と値のシグニチャ宣言です。

~~~ {.ocaml} (* .datsファイル *) extern val c: int extern fun foo (x:int): int fun bar (x: int): int = … ~~~

~~~ {.ocaml} (* .satsファイル ) val c: int fun foo (x:int): int ( foo関数の実体を宣言できません *) ~~~

けれども典型的には.satsファイルでは関数の型を定義して、.datsファイルに実装を書きます。 そのような場合、.datsファイルの実装には型注釈は不要です。

~~~ {.ocaml} (* .datsファイル *) implement baz (x) = … ~~~

~~~ {.ocaml} (* .satsファイル *) fun baz (x:int): int ~~~

重要なことですが、MLと異なり、ATSの型検査器はとても限定された型推論しか行ないません。 あなたは明示的に十分な型注釈を与える必要があります。 そうすればATSは型の導出できるようになるでしょう。

めくるめく静

ATSはMLに少し似ています。 型とデータ型を定義することができます。

(* ATS *)
typedef t = int
typedef pair (a:type, b:type) = '(a, b)
datatype option (a:type) =
  | Some(a) of a
  | None(a)
(* SML *)
type t = int
type ('a, 'b) pair = 'a * 'b
datatype 'a option =
    Some of 'a
  | None

上記のSMLコードでは、定義済みのint型があったとき、 新しいtという名前の型をint型の別名として定義しています。 また、いくつかの型変数をパラメータとして取るような型を別名として定義できます。 さらに型変数aをパラメータとして取るoptionというデータ型も定義しています。 これらの識別子はすべて静的な識別子です。 対して、動的な識別子というのは実行時の値になります。

一方ATSでは、データ型のコンストラクタに型変数を明示的に適用してやる必要があることに注意してください。 データ型に関する詳細な情報は Datatypes in the ATS tutorial を参照してくだっさい。 しかし、まずはこの章の残りを読んでからでも良いでしょう。

型宣言は静的な識別子を“type”という種の静的な式に割り付けます。 つまりtypedefはstadefの特殊形です。 次に示す2つの静的な宣言はほぼ同じです。

(* ATS (1) *)
(* sta t:type *)
typedef t = int
typedef pair (a:type, b:type) =
  '(a, b)
(* ATS (2) *)
(* sta t:_ *)
stadef t = int
stadef pair (a:type, b:type) =
  '(a, b)

この2つが違うのはtypedefがtが種“type”であることを保証するのに対して、 stadefは何も保証しないという点です。

型は、静的な式や静的な識別子が取り得る数多くの種の内の一つです。 他の種としては以下が挙げられます。

datasortを使うことで新しい種を定義できます。 sllist.dats の最初の数行はリストに似た種を定義する方法を示しています。 またsortdefを使えば種の別名を定義できます。 これはサブセット種と呼ばれる種にpiggy-backな制約をつけます。 prelude/sortdef.sats はその例です。 制約はシンプルなboolean種の式です。

type, view, propの種について、別名定義、abstract quantityの宣言、代数的データのコンストラクタの宣言をすることができます。

Static Type View Prop Viewtype
別名定義 stadef typedef viewdef propdef viewtypedef
Abstract sta abstype absview absprop absviewtype
代数的 (N/A) datatype dataview dataprop dataviewtype

type, view, prop, viewtypeはstatics(静的)の特殊形です。 つまり、typedef, viewdef, propdef, viewtypedefの代わりに単にstadefを使うことができます。 同様にabstractの宣言においてもabstype, absview, absprop, absviewtypeの代わりにstaを使うことができます。 けれどもdatasort, datatype, dataview, dataprop, dataviewtypeの間は交換することができません。 これらは新しい何かに対する代数的なコンストラクタを定義します。 (例: datatypeは新しい型のコンストラクタです。dataviewは新しいviewのコンストラクタです。などなど)

view, prop, viewtypeについて、ここでは取り上げません。 ここでは型とシンプルな静的な式について注目しましょう。

静的な式は種によって検査される第一級の言語です。 いくつかの例を見てみましょう。

(* ATS *)
stadef nat_lt (i: int, limit: int) =
  0 <= i && i < limit

静的な関数であるnat_ltは、種boolが要求されればいつでも使うことができます。 例えば、実行時に数値の引数の範囲に制約をつけたい場合を考えましょう。

(* ATS *)
typedef NatLt (n: int) =
  [i: int | nat_lt (i, n)] int(i)

これで静的な関数 NatLt: int -> type を定義できました。 静的な数値nを与えれば、NatLtは 0 から n - 1 までの範囲を持つ数値型のサブセットとしての型を返します。 NatLtの実装はこう読めるでしょう。 「種intであり、nat_lt(i, n)が真で、int(i)型として生産されるのようなiが存在する。」

NatLt(n)型を使った関数は以下のようになるでしょう。

~~~ {.ocaml} (* ATS *) fun digit_of_num (i: NatLt(10)): char = … ~~~

ATS/Anariatsの中にビルトインされた多くの静的な演算子のシグニチャは prelude/basics_sta.sats で見ることができます。 stadefを使ってそのような演算子をオーバーロードできることに注意してください。 中置の二項演算子の結合性は prelude/fixity.sats で定義されています。

異型(Atypical)の複合型

最初の区別は、 固定サイズの型はシンプルにtypeで表わされ、 任意サイズの型はt@ypeで表わされるということです。 typeの値はポインタワードと同じサイズを持つという点でMLの値と似ています。 それはボックス化もしくはアンボックス化されています。 typeのボックス化された値はGCによって管理されたヒープの中に配置されます。 ボックス化された値のいくつかの例を見てみましょう。

type Expression Type
Tuple ’(e1, e2, … en) ’(t1, t2, … tn)
Record ’{lab1 = e1, lab2 = e2, … labn= en} ’{lab1 = t1, lab2= t2, … labn= tn}
List ’[e1, e2, … en] [n:int | n >= 0] list(t, n)

(* もしくは以下に相当 *)
List t

けれどもMLの型はシステムプログラミングにとってあまりにも非力です。 メモリレイアウトをフラットな構造でしか表現できないのですから。 ここでt@ypeの値が役に立ちます。 しばしば このようなメモリレイアウトはview(線形論理のリソース)とt@ypeを持つことがあります。 つまるところ、これがviewt@ypeと呼ばれます。 t@ypeはviewt@ypeの下位種であることに注意してください。 そのためviewt@ypeと書かれているところを単にt@ypeと書いても問題ありません。 それどころか、C言語と同じ意味を持つ静的な関数である sizeof(t) が存在し、 それは以下に示す静的なシグニチャを持っています。

~~~ {.ocaml} (* ATS *) sta sizeof: viewt@ype -> int ~~~

そしてこのsizeof静的関数はt@ypeにもviewt@ypeにも使えるのです

ボックス化タプル, レコード, リストはフラットなtypeとよく似ています。


type t@ype
Tuple ’(t1, t2, … tn) @(t1, t2, … tn)
Record ’{lab1 = t1, lab2 = t2, … labn= tn} @{lab1 = t1, lab2= t2, … labn= tn}
Sequence
(List/Array)
(* list *)
list(t, n)
( array )
@[t][n]

しかしフラットな値を構築することは少し異なります。 フラットな値はヒープ(ボックス化値と同じ)もしくはスタック(MLはスタックにデータ構造を確保しませんが)のどちらかに確保されます。 これについては別の記事 Manipulating flat memory でお話しします。

フラットなメモリを初期化しないこともできます。 “t?”という注釈は未初期化のメモリの型を表わしています。 そしてそのサイズはt型と同じです。 例えば、未初期化のintは“int?”と書きます。(章末のノートを見てください) しかし、型t1とt2について sizeof(t1) == sizeof(t2) であったとしても、 コンパイラはt1?とt2?を異なる型として扱います。

最後に、ときどきtype(およびviewtype)やt@ype(およびviewt@ype)の後ろに ‘+’と’-‘という注釈を目にすることがあるでしょう。’+‘はそのパラメータが共変性であることを意味し、’-’はそのパラメータが反変性であることを意味しています。 注釈がない場合には、パラメータは不変性です。 これは静的な式の型に対して下位種を作るのに役に立ちます。 共変性は良く使われますが、反変性を使うことはまれです。

ノート: intの型はフラット

読者をおどろかせるかもしれませんが、ATSにといてintはt@ypeです。 64ビットマシンのC言語型であるintとlongを考えてみると、 intは32ビット、longは64ビット、そしてポインタは64ビットです。 intはポインタと同じサイズではありません。 同様に、ATSではlongもまたt@ypeです。 16ビットマシンの場合、intは16ビット、longは32ビット、ポインタは16ビットであるからです。

落ち着かない関数たち

ATSでの関数の型の詳細は注意深く調査するべきでしょう。 その簡単な構成はMLと似ていて、シンプルなものです。

(* ATS (.sats) *)
fun function_name (x1: t1, ..., xn: tn): t' =
  "c_name"

~~~ {.ocaml} (* SML (signature) ) val function_name: (t1 … * tn) -> t’ ~~~

C言語に変換すると、function_nameはc_nameという名前になることに注意してください。 もっともこれは任意ですが。 これは以下のように使われます。

  1. 既存のC言語関数をATSにインポートして、ATSの型をつける
  2. ATSで実装された関数をC言語側へエクスポートする

これはいくつかの重要な帰結を持ちます。

依存型にガードとアサートを追加すれば、以下のようになります。

(* ATS (.sats) *)
fun function_name
    {forall quantifiers | guards} (x1: t1, ..., xn: tn):
    [exists quantifiers | asserts] t' =
  "c_name"

ガードはforall量化子の項で書くことができる種boolの静的な式です。 アサートはforallとexists量化子の項で書くことができる種boolの静的な式です。 なおかつ、t1 … tn はforall量化子の項で書くことができる種typeの静的な式です。 そしてt’はforallとexists量化子の項で書くことができる種typeの静的な式です。

証明の項をさらに追加してみましょう。

(* ATS (.sats) *)
fun function_name
    {forall quantifiers | guards} (pf1: prop1, ..., pfp: propp | x1: t1, ..., xn: tn):
    [exists quantifiers | asserts] (prop'1, ..., prop'q | t') =
  "c_name"

アンカリー化された引数は、証明の変数とプログラムの変数の2つの部分に分断されたことに注意してください。 証明の変数はコンパイルが完了すると削除されます。 プログラムの変数はコンパイルされてもそのまま残ります。

最後になりますが、ATSはタグとして副作用を追跡するためにアロー型を使います。

(* ATS (.sats) *)
fun function_name
    {forall quantifiers | guards} (pf1: prop1, ..., pfp: propp | x1: t1, ..., xn: tn)
  :<tag1, ..., tagk>
    [exists quantifiers | asserts] (prop'1, ..., prop'q | t') =
  "c_name"

もし関数の型を静的な式として書きたければ、 (これまで見てきた関数のシグニチャに反していますが) 型の表現は以下のようになるでしょう。

~~~ {.ocaml} (* ATS (static expression) *) {forall…} (prop1, …, propp | t1, …, tn) -<tag1, …, tagk> [exists…] (prop’1, …, prop’q | t’) ~~~

タグ付きのアロー型

ATSにおけるアロー型は“-<>”のような見た目をしています。 アロー型は -<tag1, …, tagk> のような形で装飾されます。 関数の様々な種を区別するために、現時点でATSは次のようなタグを解釈します。

同様に次のタグは副作用の追跡に用いられます。

副作用の有無を示すための表現である0や1の接尾辞を、関数の種を区別するタグに加えて付けることができます。 例えば cloref1 は、MLのようにGC対象となるクロージャであり、 副作用(例外発生など)を持っているというタグになります。

stdio.h から例を

ATSにおける典型的な関数の宣言はどのような見た目になるのでしょうか? ここでは、次のプロトタイプ宣言を持つ標準Cライブラリを例に取りましょう。

~~~ {.c} char fgets(char s, int size, FILE *stream); ~~~

manページには 「fgets()はstreamから最大で size - 1 個の文字を読み込み、sが指すバッファに格納する。 ’\0’が一つバッファの中の最後の文字の後に書き込まれる。」 とあり、さらに 「fgets()は、成功するとsを返し、エラーや1文字も読み込んでいないのにファイルの終わりになった場合に NULL を返す。」 とあります。

ATSでの宣言を見てみましょう。コメントをたくさん入れてみました。

(* fgets_vはfgetsの結果である成功か失敗を表わします。
 *)
dataview fgets_v (sz:int, addr, addr) =
  | (* 成功した場合、lアドレスは長さnの文字列を格納している
     * サイズszの文字列バッファでしょう。
     *)
    {n:nat | n < sz} {l:addr | l <> null}
      fgets_v_succ(sz, l, l) of strbuf(sz, n) @ l

  | (* 失敗した場合、lアドレスは単にサイズszの空箱のはずです *)
    {l:addr}
      fgets_v_fail(sz, l, null) of bytes(sz) @ l

fun fgets
    (* countは読み込むバイト数です。
     * それはバッファのサイズであるsz以内でなければなりません。
     *)
    {count, sz:int | 0 < count; count <= sz}

    (* fmはファイルモードのための静的な種です。 *)
    {m:fm}

    (* lはバッファのアドレスを示す依存型です。 *)
    {l:addr}

    ( (* ファイルモードが読み出しアクセスを含んでいることの証明。 *)
      pf_mod: file_mode_lte(m, r),
      (* szバイトの列がlに存在することに対する線形論理の証明。 *)
      pf_buf: bytes(sz) @ l
    | (* lアドレスによって指示されるポインタを引数に取る。 *)
      s: ptr(l),
      (* 読み込む最大のバイト数を引数に取る。  *)
      size: int(count),
      (* モードmによってオープンされたFILE構造体への参照を引数に取る。 *)
      stream: &FILE(m)
    )
  :<>
    (* l'は返値のポインタを指示します。 *)
    [l':addr]

    ( (* pf_bufは消費され、ここでl'に一致する変化を形成します。 *)
      (* pf_buf is consumed, and this determines what it turns into
       * according to l'.
       *)
      fgets_v(sz, l, l')
    | (* l'で示すポインタを返します。 *)
      ptr(l')
    ) =
  "fgets"

この例はATS/Anariatsの libc/SATS/stdio.sats を元にしています。 わずかな修正と多くのコメントによる注釈が加えてあります。 はじめて見る人には明確には思えないかもしれません。 いくつかポイントがあります。

参考のために、上記のコードからコメントを削除したものを載せておきます。

dataview fgets_v (sz:int, addr, addr) =
  | {n:nat | n < sz} {l:addr | l <> null}
      fgets_v_succ(sz, l, l) of strbuf(sz, n) @ l
  | {l:addr}
      fgets_v_fail(sz, l, null) of bytes(sz) @ l

fun fgets
    {n, sz:int | 0 < n; n <= sz} {m:fm} {l:addr} (
      pf_mod: file_mode_lte(m, r), pf_buf: bytes(sz) @ l
    | s: ptr(l), size: int(n), stream: &FILE(m))
  :<>
    [l':addr] (fgets_v(sz, l, l') | ptr(l')) =
  "fgets"

この文書のTODO

blog comments powered by Disqus