この記事は SATySFi Advent Calendar 2019 15日目の記事です.14日目はzptmtrさんによるSATySFiの組版結果をテストするでした.16日目はgfnさんです.
この記事ではSATySFiのライブラリであるところのsatysfi-baseを使うと組版処理がどのように記述できるようになるのかについてざっくり解説します.具体的な使い方については実際にリポジトリを参照してもらうこととして,この記事では設計思想やユースケース,モジュール一覧を軽く眺めて雰囲気を掴んでもらうことを狙いにします.
satysfi-baseとは
satysfi-base (つい数日前まではsatysfi-libという名前でした) はSATySFiの標準ライブラリを大幅に強化するライブラリです.要するに標準ライブラリの代替と言ってもいいようなものですが,あくまでSATySFi本体とは独立に開発されているものなのでこのライブラリを使うかどうかはユーザー次第です.
このようなライブラリを開発している背景として,SATySFi本体の標準ライブラリがそこまで強力とは言えないという事情があります.SATySFiは「関数型プログラミングで組版処理が記述できる」という点を特徴としており,このうち「組版処理」の部分はある程度ライブラリの機能が充実しているものの「関数型プログラミング」については実はライブラリのサポートは手厚くなく,たとえば「浮動小数点数型の等値性判定」や「回復可能なエラーを返しうる処理の型」などは標準では用意されていません.
そこでsatysfi-baseでは標準で用意されているモジュールを大幅に拡充させたり,新たな型やモジュールを追加したり,標準のAPIをよりモジュール化されたAPIとしてラップするなどして「関数型プログラミング」の側を支援することを目指しています.その一方で組版の側でもいくつかの機能追加を行なっており,たとえばsatysfi-baseに含まれるbase/typeset/derive
というパッケージでは形式的な証明を組版するためのDSLが提供されています.このパッケージについてはzptmtrさんによる次の記事が詳しいです: SATySFiで導出木を書くDSLをつくった.
㊗️ satysfi-base バージョン 1.0 リリース
実はこの記事の公開に合わせてsatysfi-baseのバージョン1.0.0をリリースしました 🎉 APIもかなり安定したはずなのである程度安心して使えるようになったかと思います.
またこのリリースに合わせてパッケージの名前をlibからbaseへ変更しました.1 以前からこのパッケージを使用されていて最新版に乗り換える方はご注意ください.
satysfi-baseのインストール方法
大変ありがたいことにzaginさんがsatyrographosのパッケージファイルを用意してくださったのでそれを使えば簡単にインストールできます.
satyrographosそのものの使い方はこちら: Satyrographos でパッケージの簡単インストール
$ opam install satysfi-base
一度インストールが完了してしまえば,satysfi-baseは@require
するだけで使えます.
@require: base/base
@require: base/debug
let _ = Debug.print `hello` in
finish
これをhello.saty
として保存してsatysfi hello.saty
というコマンドを実行してみると以下のような出力が得られます.
$ satysfi hello.saty
(中略)
---- ---- ---- ----
evaluating texts ...
hello
evaluation done.
---- ---- ---- ----
(中略)
$
設計思想
satysfi-baseのAPIを設計したときの基本的な考え方について軽く触れたいと思います.
モジュールを使う
satysfi-baseは可能な限りモジュールを多用するインターフェイスにしています.たとえば,文字列型string
に関するプリミティブとそれをラップするsatysfi-baseのインターフェイスは以下のような違いがあります.
% SATySFi
string-same `hello` `world`
arabic 42
show-float 3.14
% satysfi-base
String.equal `hello` `world`
String.of-int 42
String.of-float 3.14
このようにSATySFiのプリミティブ(あるいは標準ライブラリ)はモジュールをほとんど使わないインターフェイスになっています.これはSATySFiにモジュール機能が入ったのが比較的最近であるという歴史的事情が大きいと思われます.satysfi-baseではモジュールを使い既存の機能をラップすることで統一的なインターフェイスを提供しています.たとえば,値の等価性を判定する関数は型ごとに用意されたモジュールの中にequal
という名前で定義するというルールにしています.(演算子も用意されています)
String.equal `hello` `world`
Int.equal 42 57
Float.equal 3.14 42.195
他の言語の良いところを可能な限り真似る
インターフェイスの設計にあたって他の言語の設計を大いに参考にしています.具体的には,
- OCaml
- Rust
- F#
あたりを参考にしました.OCamlは命名規則全般の参考にしていて,たとえばString.of-int
などはOCamlの影響を受けています.他にも,OCamlの代替標準ライブラリであるJaneStreet Coreからも影響を受けています.RustはResultモジュールやOptionモジュールのインターフェイスの参考にしました.F#はパイプライン演算子|>
に関連する部分の参考にしました.satysfi-baseの多くの関数は|>
を使った場合にメソッド呼び出しに見えるように引数の順番を調整してあります.たとえば,「jpegファイルを特定のディレクトリから読み出してスケーリングを行いインラインボックス列を返す」という処理は以下のようにパイプラインで簡潔に記述できます.
let get-image ratio path =
path |> String.append `images/`
|> Image.of-jpeg
|> Inline.of-image (13.5cm |> Length.scale ratio)
ちなみに,このget-image
もpath |> get-image 0.45
のようにパイプラインを使うことを前提で引数の順番を定めています.
言語機能が足りていない部分も可能な限り補う
SATySFiは発展途上の言語です.そのため言語機能として提供されてることが自然ないくつかの機能が提供されていません.そのようなものについても可能な限りsatysfi-baseで同等の機能を実現するように心がけています.
特に不便なのが型クラスがない点です.一応,本気でやるのであればSATySFiでad hoc多相のような超絶技巧プログラミングに頼る解決方法もあるのですが,大変なだけであまり使い勝手がいいとは言えません.そこでsatysfi-baseでは以下のような規約を導入してなんちゃって型クラスを導入しています.(以下は疑似コード)
type 'a implicit = 'a
val Int.eq : (int Eq.t) implicit
let Int.eq = Eq.make (fun x y -> x == y)
val Map.make : ('k Eq.t) implicit -> 'k 'v Map.t
型クラスは単なるレコード型として定義します.この場合はEq.t
です.型クラスのインスタンスを定義するときはそのレコード型の値を作成するだけです.この際,その値がインスタンスであることを強調するためimplicit
という型オペレータをつけておきます.'a implicit
は'a
と同じ意味なので型として特別な意味を持つわけでは無く単にドキュメンテーションのためのものです.型クラスのインスタンスを要求する際は引数の型にimplicit
をつけておきます.この例ではMap.t
型の値を作る際に鍵のequalityが必要なので('k Eq.t) implicit
を引数として受け取っています.2
本来であればimplicitとしてマークされた引数をコンパイラが自動で埋めてくれるのが型クラスなのですが,SATySFiにそのような機能がないので「型クラスがあった場合どういう挙動になっているべきか」をimplicit
をつけることで表現しています.あくまで見かけ上のテクニックですが意外とわかりやすいです.
他にもsatysfi-baseでは式の遅延評価を行うオペレータ!!
など言語機能レベルで欲しくなるものをライブラリとして提供しています.
可能な限り直接的なインターフェイスにする
SATySFiのプリミティブや標準ライブラリは意図的にインターフェイスが複雑になっている部分があります.satysfi-baseでは「危険な操作の濫用をするのはユーザーの責任」という思想の下,多少濫用の危険があるオペレータであっても直接的なインターフェイスで提供しています.
-
短絡評価を行う演算子
&&&
,|||
の追加- SATySFiにはデフォルトでは短絡評価を行う演算子が存在しません.二つのbool値のandやorをとる演算子
&&
,||
はあるのですが必ず左右両方の引数が評価されます.これのおかげでSATySFiでは引数の評価順序がどの演算子でも同じになる(と思う)のでたしかに綺麗ではあるのですが普通のプログラミング言語に慣れている人間からするとかなり混乱します.そこでsatysfi-baseでは&&
と||
それぞれの短絡評価を行うバージョン&&&
と|||
を用意しています.これらはマクロ(stage-0 function)として定義されているので使う際は~
と&
を使う必要があります.
- SATySFiにはデフォルトでは短絡評価を行う演算子が存在しません.二つのbool値のandやorをとる演算子
if ~(&(i < String.length s) &&& &(Char.is-digit (s |> Char.at i)) then
...
else
...
-
オペレータ名の変更.たとえば
abort-with-message
はpanic
にエイリアスされています.- 以前SATySFiの作者に聞いたところ「そもそも実行時エラーを可能な限り減らすために型付き言語にしているので実行時エラーを吐く処理を濫用されてしまうのは目論見通りではない.そのため『気軽に使うべきではない』という意味を込めて長い名前にしている.」という旨のことをおっしゃっていました.satysfi-base的には「使える機能は全部使いやすくする」という方針なので
panic
という短い名前にしています.
- 以前SATySFiの作者に聞いたところ「そもそも実行時エラーを可能な限り減らすために型付き言語にしているので実行時エラーを吐く処理を濫用されてしまうのは目論見通りではない.そのため『気軽に使うべきではない』という意味を込めて長い名前にしている.」という旨のことをおっしゃっていました.satysfi-base的には「使える機能は全部使いやすくする」という方針なので
-
浮動小数点数の比較.標準で用意されていない
Float.(==)
やFloat.(<=)
を提供しています.- 浮動小数点数の演算の結果は誤差を含みうるのでそれらの結果の比較を正しく行うことは本質的には不可能である,というスタンスでSATySFiではfloat型の比較演算(
==
とか<=
とか)が提供されていないようです.そうは言っても使いたいものは使いたいのでsatysfi-baseではいろいろ頑張って自力でそれらを実装しています.
- 浮動小数点数の演算の結果は誤差を含みうるのでそれらの結果の比較を正しく行うことは本質的には不可能である,というスタンスでSATySFiではfloat型の比較演算(
-
可変セルを使いやすくする
- デフォルトのSATySFiでは可変セルの作成は
let-mutable
構文を通してのみ行えることになっていますがsatysfi-baseではRef.make
という関数を使って通常のプログラミングの作法で可変セルを作成できます.let-mutable
はミュータブルなセルの有効範囲を明示するためにこのようなインタフェースになっていると思われますが,OCamlのインタフェースに合わせて直接値を作れるようにしました.
- デフォルトのSATySFiでは可変セルの作成は
let-mutable r <- 42 in
...
let r = Ref.make 42 in
...
-
万能インラインコマンド
\eval
と\eval-const
の追加- SATySFiには通常のプログラムモードの名前空間に加えてインラインコマンド(とブロックコマンド)の名前空間があります.これらは時に便利ですが,目的のインラインボックス列を作成する関数を作成するたびにコマンドも同時に定義しなければならないという面倒さもあります.これを解決するためにsatysfi-baseでは
\eval
という万能コマンドを用意しています.これを使うと組版を行うちょっとした処理をインラインテキストの中に直に埋め込むことができます.
{ The quick brown fox \eval(Inline.mandatory-break); jumps over \eval-const(Inline.skip 1cm); the lazy dog. }
この例ぐらいだとインラインコマンドを用意した方が便利な気もしますが,実際にはもっと複雑だけど一回しか使わないような処理をその場で書くことができます.個人的にとても多用している機能です.
- SATySFiには通常のプログラムモードの名前空間に加えてインラインコマンド(とブロックコマンド)の名前空間があります.これらは時に便利ですが,目的のインラインボックス列を作成する関数を作成するたびにコマンドも同時に定義しなければならないという面倒さもあります.これを解決するためにsatysfi-baseでは
既存の機能を壊さない
satysfi-baseは標準ライブラリを置き換えるのでは無く共存できるように設計しています.たとえば,satysfi-baseの提供するlist-ext
はSATySFi標準で提供されているListモジュールに新しい関数を追加します.list-ext
は後方互換性を保っており,list-ext
によってListモジュールを使う既存のコードが壊れないようになっています.
@require: base/list-ext
List.find
List.take
...
個別のモジュールについて
以下ではsatysfi-baseで提供している個別のモジュール(のうち重要なもの)について解説します.細かなAPIに立ち入ると長くなりすぎるので必要に応じてソースコードを参照してください.
Char
SATySFiには一つの文字を表す型が存在しません.satysfi-baseではそれを補うためのCharモジュールが提供されています.Char.t
が一つの文字を表す型です.実装上の都合で他の多くの言語でサポートされている全ての機能が使えるわけではありません(たとえば文字からコードポイントを取り出せません)が,ほとんどの用途には困らないはずです.
使う際には@require: base/char
とします.
let a = Char.make `a` in %% make a new char representing `a`
let _ = Char.equal a (`abc` |> Char.at 0) in %% true
let _ = Char.is-digit (Char.newline) in %% false
List, Option, Color, Math
List, Option, Color, MathはいずれもSATySFiの標準ライブラリで提供されているモジュールですが,satysfi-baseではこれらのモジュールを拡充するための以下のようなパッケージを用意しています.
base/list-ext
base/option-ext
base/color-ext
base/typeset/math-ext
たとえば@require: base/list-ext
を呼ぶことでList.take
やList.find
のような関数型言語でよく目にする関数群がListモジュールに追加されます.Optionモジュールに追加されるAPIは概ねRustのAPIを模倣したものになっています(たとえばOption.unwrap-or
という関数が提供されています).ColorモジュールにはたとえばCSSカラー名をcolor型に変換するColor.of-css
が追加されます.数式コマンドを提供するMathモジュールには\bigsqcup
,\iff
などが追加されます.
Int, Float, Length, String
それぞれint
,float
,length
,string
型に関するモジュールです.特にFloatにはSATySFiでネイティブで提供されていないfloat間の等値性判定や大小比較などが実装されています.
文字列のフォーマットはStringモジュールではなくFormatモジュールで提供されています.
Format.format `Hello, {}!` [`wasabiz`]
%%=> `Hello, wasabiz!`
Result, Either
'a 'e result
は回復可能な'e
型のエラーを返しうる'a
型の計算を表す型です.Resultモジュールはresult型に関連する一連のAPIを提供しています.APIは概ねRustのものを模倣しています.
match tokens |> Parser.run syntax with
| Ok(_) -> Debug.print `success`
| Err(_) -> Debug.print `failure`
'a 'b either
はresultとほぼ同じで'a
型の値と'b
型の値のどちらかを返す計算の型ですが,'a
と'b
の間にバイアスがない場合に使用されることを想定しています.either型に関するAPIはEitherモジュールにまとめられています.
Map, Set
MapモジュールとSetモジュールはそれぞれ連想配列と集合を表す型とそれにまつわるAPIを提供しています.通常の言語とは異なり線形探索で実装されているので膨大な数のデータを扱うのには向いていません.このような実装になっているのはSATySFiで文字列の大小比較や定数時間でアクセス可能な(immutable)配列がプリミティブで用意されていないためです.
Eq, Ord
'a Eq.t
は'a
型の値の等価性を判定する述語のインスタンスです.'a Ord.t
は'a
型の値の上の全順序を表すインスタンスです.それぞれ型クラスとして使われることを想定しています.
Ref
Refモジュールには可変セルを表す'a ref
型を使うための一連のAPIが定義されています.可変セルはsatysfi-baseを使用するかしないかで使い勝手が大きく変わります.
たとえば以下のようなSATySFiのプログラムはRefモジュールを使って書き換えることができます.
let-mutable r <- 1 in
let () = (r <- 2) in
!r
let r = Ref.make 1 in
let () = r |> Ref.set 2 in
r |> Ref.get
あるいは可変セルの状態を一時的に変更するプログラムは以下のようにかけます.
let orig = !r in
let () = r <- 42 in
let ret = hogehoge in
let () = r <- orig in
ret
r |> Ref.set-temporarily 42 (fun () ->
hogehoge
)
Block, Inline, Pager, Image
ここまでは関数型プログラミングのためのモジュールでしたが,組版用のプリミティブについてもそれらをラップして使いやすくしたモジュールを用意しています.たとえばBlockモジュールはブロックボックス列に関する操作をまとめたモジュールです.同様にInlineモジュールはインラインボックス列,Pagerモジュールは改ページ,Imageモジュールは画像ファイルの読み込みに関するモジュールです.これらは標準のインターフェイスから大きく乖離したインターフェイスを持っています.
たとえば筆者らが書いた同人誌であるところのyabaitech.tokyo vol.3の扉を作るためのコードは以下のような感じ 3:
[
ctx-title |> (title |> Inline.of-string |> Block.centering);
Block.skip 30pt;
ctx-date |> (Format.format `{} @ {}` [date; venue] |> Inline.of-string |> Block.centering);
Block.skip 80pt;
ctx-doc |> ({本誌のPDFとソースコードのダウンロードはこちらから} |> Inline.read |> Block.centering);
ctx-doc |> (Image.of-pdf `QR_DL.pdf` 1 |> Inline.of-image 10cm |> Fn.const |> Block.centering);
Pager.clear;
] |> Block.concat
satysfi-baseの今後
satysfi-baseは開発者を募集しています.APIの拡充やドキュメント・テストの充実などやることがまだまだあります.興味がある方はぜひご連絡を!(コチラ → https://github.com/nyuichi/satysfi-base/issues/12)