ラベルつきオプション引数の型システム

概要

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]{6zw}{…}, $\sqrt[3]{2}$

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

• 順番で識別する仕組みだと，どの指定を何番目にすべきかが読み書きするときに解りづらいことが多い．
• オプション引数の列の中でより手前のものを省略し後方のものを与えるときは，手前のものを ?* で “明示的に省略” する必要があり，面倒である．
  • 例えば以下のような具合：

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

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

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

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

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

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

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

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

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

型システムの詳細

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

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

τ ::=
  …
  | ?(l : τ, …, l : τ) τ -> τ

本当はもう少し一般性の高い形式であることを後で説明しますが，今はひとまずこの素直な形であると把握していてください．

（ちなみに従来のラベルなしオプション引数の場合は τ ?-> … τ ?-> τ -> τ の形でした．）

函数抽象と函数適用の構文も（型註釈をつけてよいことや糖衣構文を簡単のため省略すると）以下のように拡張されます：

e ::=
  …
  | fun ?(l = x, …, l = x) x -> e
  | e ?(l = e, …, l = e) e

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

Γ, x_1 : option τ_1, …, x_n : option τ_n, x : τ' ⊢ e : τ
-----------------------------------------------------------------------------
Γ ⊢ fun ?(l_1 = x_1, …, l_n = x_n) x -> e : ?(l_1 : τ_1, …, l_n : τ_n) τ' -> τ

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

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

Γ ⊢ e : ?(l_1 : τ_1, …, l_n : τ_n) τ' -> τ
Γ ⊢ e_k : τ_(j_k)  (for each k ∈ {1, …, m})
Γ ⊢ e' : τ'
-----------------------------------------------
Γ ⊢ e ?(l_(j_1) = e_1, …, l_(j_m) = e_m) e' : τ

多相性

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

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

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

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

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

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

τ ::=
  …
  | ?(r) τ -> τ

r ::=
  | l : τ, r
  | *
  | ρ

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

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

use_optional : ∀ρ :: Row {foo}. ?(foo : int, ρ) int -> int

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

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

まとめ

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

参考文献

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