SATySFi v0.1.0に向けたラベルつきオプション引数の型システム

最終更新：

記事 SATySFi プログラミング言語 型システム

SATySFi v0.1.0に向けてオプション引数に関する言語設計を非互換に改めつつあるので，その紹介をします．

初出：

改造の動機

もともとSATySFi v0.0.xにもラベルなしオプション引数の機構は存在していて，以下のように ?: で与えることができました：

+section?:(`sec:sample`)?:(`Sample`){Sample}<
 （章の本文）
>

オプション引数にはラベルはなく，オプション引数列のうちで何番目に与えられたかによって識別されていました．上記の例だと，1番目のオプション引数は相互参照のための識別文字列であり，2番目のオプション引数はPDFのアウトラインでこの章のタイトルとしてどのような文字列を出すかの指定です．コマンドだけでなく，通常の函数でもオプション引数をとることができます：

let succ ?diff-opt n =
  match diff-opt with
  | Some(d) -> n + d
  | None    -> n + 1
in
(succ 42, succ ?:57 42)
  % --> (43, 99)

オプション引数がラベルをもたないような言語設計にしたのは，主にLaTeXでラベルなしのオプション引数に相当するようなインターフェイスが慣習的によく使われていることに触発されたものでした：

\parbox[c]{6em}{…}, $\sqrt[3]{2}$

しかし，オプション引数を使いたくなる場面は当初の言語設計時の想定より多かったこともあり，以下のような不便さが顕著に生じました：

  • 順番で識別する仕組みだと，どの指定を何番目にすべきかが読み書きするときに解りづらいことが多い．

  • オプション引数の列の中でより手前のものを省略し後方のものを与えるときは，手前のものを ?* で “明示的に省略” する必要があり，面倒である．

    +section?*?:(`Sample`){Sample}<
 （章の本文）
>

こうした面倒さを解消するために，オプション引数をラベルつきの定式化に変え，以下のように書けるようにしたいと考えました：

+section?(ref = `sec:sample`, outline = `Sample`){Sample}<
 （章の本文）
>

見ての通り，オプション引数部分を ?(label1 = arg1, …, labelN = argN) の形で記述します．オプション引数をひとつも指定しない場合は，?(…) 全体を省けます．通常の函数も以下のように定義・使用できます：

let increment ?(diff = diff-opt) n =
  match diff-opt with
  | Some(d) -> n + d
  | None    -> n + 1
  end
in
(increment 42, increment ?(diff = 57) 42)

この定式化には以下のような恩恵があります：

  • 引数にラベル名がつくので，単純に何に関する指定なのかが解りやすい．
  • 各引数の与え方は順不同なので，一部を省略する場合も ?* のようなぎこちない方法をとる必要がない．
  • 相変わらず静的に型がつき，想定していないラベル名を指定した場合や引数の型がおかしい場合は型エラーが出てくれる．

デフォルト値を与える場合は，もう少し簡潔に以下のようにも書けるようにするつもりです：

let increment ?(diff = d = 1) n =
  n + d
in
(increment 42, increment ?(diff = 57) 42)

型システムの詳細

函数型・函数抽象・函数適用の拡張

型の構文としては，函数型が通常の \(τ \to τ\) から以下のように拡張されます：

\[\begin{align*} τ \Coloneqq\ \cdots\ |\ ?(l : τ, …, l : τ)\ τ \to τ \end{align*}\]

従来の \(τ_1 \to τ_2\) は \(?()\ τ_1 \to τ_2\) と等価です．本当はもう少し一般性の高い形式であることを後で説明しますが，今はひとまずこの素直な形であると把握していてください．

（ちなみに従来のラベルなしオプション引数の場合は \(τ \mathrel{?\!\!\to} \cdots τ \mathrel{?\!\!\to} τ \to τ\) の形でした．）

函数抽象と函数適用の構文も以下のように拡張されます：

\[\begin{align*} e &\Coloneqq\ \cdots \\ &\ |\ \mathbf{fun}\ ?(l = x, …, l = x)\ x \to e \\ &\ |\ e\ ?(l = e, …, l = e)\ e \end{align*}\]

型の場合と同様に，\(\mathbf{fun}\ x \to e\) と \(e_1\ e_2\) はそれぞれ \(\mathbf{fun}\ ?()\ x \to e\) および \(e_1\ ?()\ e_2\) の糖衣構文です．実際には変数には型註釈をつけてよいですが，簡単のため省略しています．

函数適用の型つけ規則は以下のように単純です：

\[\begin{align*} \begin{array}{c} Γ, x_1 : \mathrm{option}\ τ_1, …, x_n : \mathrm{option}\ τ_n, x : τ' ⊢ e : τ \\\hline Γ ⊢ (\mathbf{fun}\ ?(l_1 = x_1, …, l_n = x_n)\ x \to e) :\ ?(l_1 : τ_1, …, l_n : τ_n)\ τ' \to τ \end{array} \end{align*}\]

“変数はそれぞれ函数抽象の内側からは \(τ_i\) 型ではなく \(\mathrm{option}\ τ_i\) 型に見える” ことだけ注意が必要ですが，基本的にはとても素直な規則です．

函数適用の規則も記述が若干ややこしいですが意味するところはわりと素直です：

\[\begin{align*} \begin{array}{c} Γ ⊢ e :\ ?(l_1 : τ_1, …, l_n : τ_n)\ τ' \to τ \\ Γ ⊢ e_k : τ_{j_k}\ (\text{for each}\ k ∈ \{1, …, m\}) \qquad Γ ⊢ e' : τ' \\\hline Γ ⊢ e\ ?(l_{j_1} = e_1, …, l_{j_m} = e_m)\ e' : τ \end{array} \end{align*}\]

こうした規則によりどのように型がつくか見るために，前述の increment の定義を再掲します：

let increment ?(diff = diff-opt) n =
  match diff-opt with
  | Some(d) -> n + d
  | None    -> n + 1
  end

これには以下のように型がつきます：

  • increment \(\ :\ ?(\mathtt{diff} : \mathrm{int})\ \mathrm{int} \to \mathrm{int}\)

多相性

基本的には前節で変更の概要はお伝えできたかと思いますが，実際には多少技巧的な工夫があり，或る種の多相性が実現されています．

多相性の必要性については，例えば次の例を考えるとわかりやすいです： 以下のような高階函数にはどんな型がつくべきでしょうか？

let use_optional f =
  f ?(foo = 42) 57 + 1

とりわけ，引数の f にはどんな型がつくべきでしょうか？ \(?(\mathtt{foo} : \mathrm{int})\ \mathrm{int} \to \mathrm{int}\) のような型を想定するかもしれませんが，例えば “foo のほかに bar のようなオプション引数も受け取れて，ここでは単に foo しか与えられないだけ” という函数も f として適格なはずです．こうしたことを表現するためにオプション引数に関する多相性が必要になってきます．

こうした多相性を表現するために，SATySFi v0.1.xのオプション引数では列多相 (row polymorphism) の一種 [1] を転用することにしました．オプション引数について同様の仕組みをとっている論文や実装を見たことがないためおそらく筆者の考案によるものだと思いますが，仕組みとしてはシンプルであってわりとすぐ思いつくようなものです（ただし，おそらく大丈夫だろうとは思っているものの型安全性などの正当性を既に証明しているわけではないです）．

これは直観としては1つの函数のとるオプション引数全体を列 (row) とみなすという方法です．列は一般的にはレコードの型つけに使う機構ですが，これをオプション引数の型つけにも転用し，函数の型は以下のような構文であると考えます：

\[\begin{align*} τ &\Coloneqq\ \cdots\ |\ ?(r)\ τ \to τ \\ r &\Coloneqq\ l : τ, r\ |\ \ast\ |\ ρ \end{align*}\]

\(r\) が列のメタ変数であり，\(ρ\) が列変数 (row variable) 全体を動くメタ変数です．\(\ast\) は空の列を，\(l : τ, r\) は列 \(r\) に \(l : τ\) を追加してできる列を表します．最初に掲げた函数型の拡張 \(?(l_1 : τ_1, …, l_n : τ_n)\ τ^{\prime} \to τ\) は，実際には \(?(\cdots)\) の内側が \(l_1 : τ_1, …, l_n : τ_n, \ast\) という列であったという一般化です．

こうした仕組みを使うと，前述の use_optional には以下のように型をつけることができます：

  • use_optional \(\ : ∀ρ \mathrel{::} \mathrm{Row}\ \{\mathtt{foo}\}.\ ?(\mathtt{foo} : \mathrm{int}, ρ)\ \mathrm{int} \to \mathrm{int}\)

ただし，ラベル集合 \(L\) に対して \(\mathrm{Row}\ L\) は “\(L\) の元のラベルを含まない列につくカインド” です．すなわち，上記の型での全称量化は “\(ρ\) が \(\mathtt{foo}\) をもたない列全体を動く” ということを意味します．こうして use_optional の第1引数 f は “\(\mathrm{int}\) 型のオプション引数をラベル \(\mathtt{foo}\) で受け取れるが，それ以外のオプション引数については自由であるような函数” であると扱うことができます．

こうした仕組みは既にv0.1.0に向けた実装ではおおよそ実現されており，少なくともいくらかの例に於いては問題なく使用できています．

まとめ

本稿ではSATySFi v0.1.xに向けて設計・実装したラベルつきオプション引数の仕組みについて概説し，それが列多相をベースとして実現した機構であることを紹介しました．

参考文献

  1. Benedict R. Gaster and Mark P. Jones. A polymorphic type system for extensible records and variants, 1996.