マクロツイーター

はてダから移行した記事の表示が崩れてますが、そのうちに直せればいいのに（えっ）

画期的な関数型組版言語を作ってみた（※ただし画期的）

TeX以外

夏！ 酷暑！ ゆきだるま☃︎！

チョット SATySFi を語ってみる

さて、ﾅﾝﾄｶ☃︎の日恒例の「本質的な問題を画期的なナニカで解決する」ネタですが、今年は関数型組版言語について考えてみました。

SATySFi のここがスゴイ！

関数型組版言語といえばやっぱり、SATySFi ですね。SATySFi がリリースされてから早くも半年が過ぎました。この間も、開発は着々と進められています。

SATySFi の開発目標は「TeX／LaTeX の“よりよい代替”となること」です。このため、TeX／LaTeX と同じマークアップ言語処理系を採用しつつ、TeX／LaTeX の“アレな点”を克服するための言語設計を採用しています。

  • TeX 言語は極めて“動的な”言語であるため、コードに不備があった場合に支離滅裂な動作が起こり、結果として意味不明なエラーが発生しやすい。LaTeX も結局 TeX 言語上のマクロに過ぎないため同様である。
    →SATySFi は強い表現力をもつ静的型付けを採用している。これにより、“明らかに意味を持たない”間違った記述が、コンパイルの早い段階に、的確な型エラーとして報告される。
  • TeX 言語は全ての実行制御を「トークン列上のマクロ展開」という形で行う。この方式はそもそも通常規模のプログラミングには向いておらず、何よりも世間で広く用いられている言語と大きく異なる思考を必要とする。このことが TeX 言語の習得（つまり LaTeX 上の機能開発）を著しく困難なものにしている。
    →SATySFi はマークアップとプログラミングの文法を明確に分離し、後者ではごく普通の外見の言語（ML 風の関数型言語）を採用している。

まとめると、SATySFi は「非アレな組版言語処理系」を目指しているわけです。

SATySFi のここがダメ！

このようにスバラシイ SATySFi ですが、私の個人的な見解としては、決定的な“弱点”を抱えてると考えています。その弱点とは

型システムが複雑すぎて、一般のヒト類にとって理解困難である

ということです。

もちろんこの“弱点”は「一般的にヒト類は複雑な型システムの理解が不得手である[要出展]」という性質に起因するものであるため、SATySFi 自体の問題ではありません。しかし、逆にいうと、原因が我々ヒト類のもつ生来的性質にあるからこそ、その改善の可能性が著しく限られてしまう、というのもまた確かです。

結局、理論上は的確な型エラーが提示されたとしても、ヒト類がそれが理解できないという事態が必然的に多発することになるでしょう。これは SATySFi の目標から考えて重大な問題であることは間違いありません。

型システムがアレになる、本質的理由

なぜ SATySFi の型システムは複雑なのでしょうか。実はこれは SATySFi が組版用途の言語であることに根源的な理由があります。

つまり、我々の表す文書が複雑な構造をもつがゆえに、SATySFi は複雑な型システムを持たざるを得ないわけです。すなわち、ここで述べた問題は、ある意味で「本質的に解決困難」といってよいでしょう。

本質的な問題、画期的な解決

では、このような「本質的に解決困難」はどう解決すればよいでしょうか。本ブログの読者なら、既にお判りのことだと思います。そう、

出力をゆきだるま☃︎に変えればよい

のです。型システムの複雑さの根源は文書構造の複雑さにあるのでした。従って、文書構造の複雑性を排除して、その内容を☃︎に統一することにすれば、型システムの単純化が実現できるのです。

型システムを極力単純にすることには大きな利点があります。それによって、静的型エラーが起こる可能性を排除することも可能となるためです。つまり、字句解析を通ったプログラムは常に型付け可能になるわけです。さらに、型付けが健全であれば、動的な型エラーが起こることもありません。結果的に、ユーザは言語の型システムについての知識を何も持たなくても済むことになります。すなわち、ヒト類に変更を課する必要性から解放されるわけです。

画期的な静的組版言語「scSATySFi」

そういうわけで、早速作ってみました。

Windows（64bit）の場合は、リリースのページにビルド済のバイナリ（scsatysfi.exe）が置いてあるので、それをダウンロードして適当な（実行パスの通った）ディレクトリに配置すればOKです。他の環境の場合は、README にある通り、Go をインストールして「go get」してください。

とにかく scSATySFi を使ってみる

インストールができたら、早速使ってみましょう。せっかくのﾅﾝﾄｶの日なので、☃︎を出力してみます。scSATySFi の文法は非常に単純で、☃︎を出力するには、単に☃︎(U+2603)を書くだけでOKです。LaTeX や SATySFi にあるような「文書構造を示すための記述」は一切ありません。

[essential.scty]
☃︎

では早速この文書ファイルをコンパイルしましょう。以下のコマンドを実行します。

scsatysfi essential.scty

以下のような端末出力とともに、PDF ファイル essential.pdf が出力されました。

# scsatysfi essential.scty
 ---- ---- ---- ----
  target file: 'essential.pdf'
  dump file: 'essential.scsatysfi-aux' (won't be created)
  parsing 'essential.scty' ...
 ---- ---- ---- ----
  reading 'essential.scty' ...
  type check passed. (essential)
 ---- ---- ---- ----
  evaluating texts ...
  evaluation done.
 ---- ---- ---- ----
  writing pages ...
 ---- ---- ---- ----
  output written on 'essential.pdf'.

essential.pdf の中身を確認してみましょう。

完璧ですね！

チョット注意
  • scSATYsFi は静的型付き言語ですが、完全な型推論機能をもっているため、ユーザが型を明示的に書く必要は全くありません。実際、scSATySFi には型を明示する記法はありません。
  • もしかしたら（キーボードに「☃︎」のキーがないなどの不幸な理由で）文字「☃︎」の入力が難しい場合もあるでしょう。そのため、scSATySFi では「☃︎」を「8」で代用できるようになっています。（なお「⛄︎」(U+26C4)「⛇」(U+26C7)でも「☃︎」と等価になります。）それ以外の文字は scSATySFi の文法では現れないため、「☃︎」「⛄︎」「⛇」「8」および空白類文字（空白・水平タブ・改行）以外の文字が含まれると文法エラーとなります。((例外として、コメント開始文字である「🦆」が現れた場合、その行の残りの文字は無視されます。また「🦆」は「2」で代用できます。))
  • ☃︎がもっともっと入った文書を作ろうとして次のように書いたとします。 
    ☃︎ ☃︎ ☃︎ ☃︎ ☃︎
    この文書ファイルはコンパイルは通りますが、残念ながら出力される☃︎は常に一つだけになります。複数の☃︎を扱おうとすると、型システムが複雑になってヒト類の手に負えなくなってしまうからです。一つの文書で済ませるなんて横着をせずに、☃︎の文書をたくさん作りましょう。その方が素敵でしょう。
    ※実際には、「☃︎ ☃︎ ☃︎ ☃︎ ☃︎」は scSATySFi の式であり、それを評価した結果の値が☃︎になります。なので、出力は☃︎一つになるわけです。

scSATySFi のチョット理論的な話

既に述べた通り、scSATySFi ではユーザが型システムを理解する必要は全くないのですが、興味のある人のために、scSATySFi の型システムについて簡単に説明しておきます。

構文・型

型が 1 つしかないという、極限まで単純化した型システムになっています。

簡約規則

この簡約規則について、以下の性質が成立します。*1

  • すべての項が強正規化可能である。
  • Church-Rosser 性（合流性）をもつ。
型付け規則
     

この型付け規則について、以下の性質が成立します。

  • 全ての項は型付け可能である。つまり、静的型エラーが発生しない。
  • 任意の項について、型情報が全く与えられない状態から当該の項の型を推論できる。またその推論を効率的に（線形時間で）行うためのアルゴリズムが存在する。

この 2 つの性質があるため、ユーザはコード作成時・コンパイル時の何れにおいても、言語の型システムについて一切気にする必要がありません。

具象構文について

実は、適用演算については、結合則が成立します。*2

(☃︎ ☃︎) ☃︎ = ☃︎ (☃︎ ☃︎)

従って、一般に☃︎が複数ある式においては、式の値は括弧の位置によらず一定になります。例えば、次の 3 つの式はどれも同じ値をもちます。

(​(​(☃︎ ☃︎) ☃︎) ☃︎) ☃︎
(☃︎ ☃︎) (​(☃︎ ☃︎) ☃︎)
☃︎ (​(☃︎ (☃︎ ☃︎)) ☃︎)

このため、scSATySFi の具象構文においては、「演算の優先順位を表す括弧を常に省略する」という規則を採用しています。これにより、ユーザは☃︎以外の記号を一切書かなくて済みます。

☃︎ ☃︎ ☃︎ ☃︎ ☃︎

scSATySFi のチョット素敵な使い方

  • 文法を極力簡単にすることを優先させたため、出力の☃︎をカスタマイズする機能は敢えて省いています。ただし例外として、☃︎のマフラーの色に限っては、コマンド起動時のオプション“--muffler”で指定できます。
    scsatysfi --muffler="green!50!black" essential.scty
    ここで“--muffler”に指定する値は、LaTeX の xcolor パッケージの「色式」に従います。

まとめ

というわけで、「SATySFi の設計はスバラシイけど、実際に自分が使うのは難しそう……」と思っている人は、ぜひとも画期的な scSATySFi を試してみてください。scSATySFi で ☃︎な文書をどんどん作って、酷暑の夏を乗り切りましょう！

*1:煩雑さを避けるため、この記事では証明は一切省略します。

*2:括弧 ( ) は抽象構文における演算子の優先順位を示す補助記号です。