SATySFiでad hoc多相

SATySFiは現代的な設計に基づく組版処理システムです．
組版を行うバックエンドへ指示が関数型プログラミングで行えることが最大の特徴です．
言語としてはOCamlやSMLに近い構文を持ち，少しでもML系の言語とかHaskellに触ったことがある人なら特に苦労することなく高度な組版処理をプログラムすることができると思います．
実際私は技術書典の記事をSATySFiで記述していますがレイアウトに不満がある時などにささっと自分の手で変更できる(すくなくともそれに抵抗をあまり感じない)のは大きな魅力だと思います．(LaTeXを使う時はひたすらStack Exchangeで自分と同じようなハマり方をしてる人を探すガチャをしています．虚無．)

ただし，あくまで組版処理がメインのため，プログラミング言語単体で見るとまだまだ不便なところもあります．たとえばSATySFiにはMLライクなモジュールシステムがありますがfunctorがありません．またHaskellライクな型クラスもありません．そのためad hoc多相的なことができず，同じような見た目だけど少し違うコードを頻繁に書かなければならないことが多いです．SATySFiの型システムは基本的には教科書的なML式の型システム + 組版用の機能が実装されているのみなので，この制限は今後SATySFiに言語拡張が入らない限りはどうしようもないかなと思っていました．しかし昨日たまたまType-Indexed Value (TIV)なる概念を知りこれがSATySFiにも応用できることに気づきました．TIVを用いるとSATySFiでもad hoc多相(っぽいこと)ができるようになります．この記事ではSATySFiでTIVをやるための方法についてざっと解説します．

(TIVを教えてくれた@eldesh先生(の本)に感謝 )

結局何ができるのか

ad hoc多相でよく使われる例としてshowがあります．
HaskellではShow型クラスとして実装されているものです．
これはさまざまの型の値を文字列型に変換します．
受け取った値を文字列に変換する方法がなければ型検査時にエラーになります．
今回実装するTIVを使うと例えば以下のようなコードでshowを実現することができます．

% register methods
Show.register int String.of-int
Show.register string Fn.id

% use methods
Show.apply int 42        % => `42`
Show.apply string `foo`  % => `foo`
Show.apply string 3      % => type error

ここで，intやstringはType.tという型の値です．(正確にはint Type.tのように適切な型パラメータをとります．)
それぞれの型に対してどのように文字列化を行うかを指定するのがShow.registerです．
int型の時は通常の10進のアラビア数字の表示によって文字列化を行い，string型の時はその値をそのまま返す，というルールにしています．
実際に文字列化を行うときはShow.applyを使います．Show.applyは文字列化を行う際に値そのものに加えてその値の型(を表す値)を受け取ります．この際，一番下の行のように値とその型(を表す値)にミスマッチがあれば型エラーになります．そのようなミスマッチがなければ型検査に通り，行末コメントで示してあるように整数値や文字列がさきほど指定したやり方で正しく文字列化されます．

今回のように型を明示的に渡さなければいけないのはどうしても外せない制限です．今後SATySFiにimplicit valueのような機能が追加されれば上のコード中のintやstringは書かなくても良くなります．あと，ここではlist intの文字列化などは例として挙げていません．一応listの文字列化も可能なのですが話がややこしくなるので載せていません．あと，ここでString.of-intやFn.idはSATySFiの標準ライブラリには存在しない関数ですが，これらは拙作のライブラリであるsatysfi-libに実装されているものです．このライブラリはSATySFiでもっと関数型プログラミングしようという意図で作っているものです．普通に便利なので是非使ってみてください．

準備

TIVをするにはいくつか準備が必要です．関数型言語の上で変なことをするのに慣れている人(GHC拡張とかが好きな人)には追っかけるのは難しくないと思います．

まず，PIsoというモジュールを用意します．
PIsoはpartial isoの気持ちで，'a 'b PIso.tは型'aと型'bの間に部分単射があることを表します．部分単射はドメインとコドメインを入れ替えても部分単射なことに注意してください．ここではそれぞれの向きの部分単射をinjectとprojectと呼んでいます．

先ほども言及しましたがSATySFiにはfunctorがないのでモジュールはただの名前空間以上の機能を持ちません．ここでわざわざモジュールにしているのは単に名前をわかりやすくするためです．

module PIso : sig
  type 'a 'b t
  val make : ('a -> 'b) -> ('b -> 'a) -> 'a 'b t
  val inject : 'a 'b t -> 'a -> 'b
  val project : 'a 'b t -> 'b -> 'a
end = struct
  type 'a 'b t = T of ('a -> 'b) * ('b -> 'a)
  let make i p = T (i, p)
  let inject (T (i, _)) = i
  let project (T (_, p)) = p
end

つぎにUnivというモジュールを用意します．
UnivはUniversal Typeの気持ちで，あらゆる型をUniv.tに埋め込むことができます．
埋め込みは型ごとに別々で，piso ()によって作成します．
ここで()を渡しているのはvalue restrictionがあるせいです．
埋め込みであることはpisoの戻り値の型'a t PIso.tによって表現されています．

あらゆる型の値を一つの同じ型Univ.tに埋め込んでいるのでだいぶ怪しいコードに見えますが，
実際参照型をうまくハックした実装になっています．
以降の話でこの実装の中身を理解している必要はありませんが，これだけでも面白いので読んでみるといいでしょう．

module Univ : sig
  type t
  val piso : unit -> 'a t PIso.t
end = struct
  type t = unit -> unit
  let piso () =
    let r = Ref.make None in
    let inject a =
      fun () -> (r <- Some a) in
    let project f =
      (r <- None) before
      (f ()) before
      (match !r with
      | Some(a) -> a 
      | None -> error `oops`) in
    PIso.make inject project
end

次に型を表す値を作ります．モジュールの名前はずばりTypeです．
型'aを表す'a Type.tは内部的にはstringと'a Univ.t PIso.tの組です．
stringの方はその型の名前を表しているだけで，実際に大事なのは'a Univ.t PIso.tの方です．
名前を登録しなければいけないのは，このあとType.tを鍵としたマップをつくるためです．
後々forsome 'a. 'a Type.tを鍵にとるようなマップが欲しくなるのですが，SATySFiではそのような型を持つマップがつくれないので'a Type.tの中の名前を鍵として代用します．

あと，type 'a t = 'a uとかかいう謎の文がありますが，これはSATySFiの型検査器のバグを回避するためのコードです．

module Type : sig
  type 'a t
  val make : string -> 'a t
  val name : 'a t -> string
  val piso : 'a t -> 'a Univ.t PIso.t
end = struct
  type 'a u = T of string * 'a Univ.t PIso.t
  type 'a t = 'a u
  let make name = T(name, Univ.piso ())
  let name (T(n, _)) = n
  let piso (T(_, i)) = i
end

最後に任意の値を表すAnyというモジュールをつくります．
これは見た目だけのために導入するモジュールで，実質的にはUnivと一緒です．
任意の値をAny.tにしたり，Any.tから任意の値を取り出すことができます．

module Any : sig
  type t
  val make : 'a Type.t -> 'a -> t
  val get : 'a Type.t -> t -> 'a
end = struct
  type u = Univ.t
  type t = u
  let make t a = PIso.inject (Type.piso t) a
  let get t x = PIso.project (Type.piso t) x
end

簡単なShowモジュール

ここまでの準備があるとad hoc多相を実現するShowモジュールが実装できます．
ただし冒頭で挙げた形にするにはもうワンステップ必要なので，その前に簡単な方のShowモジュールの実装を見せます．

tableは，気分としては('a -> string) Type.tから'a -> stringへのマップです．
ただしこのままだと型がおかしなことになるので鍵を('a -> string) Type.tから取り出した名前であるstringにし，値'a -> stringをAny.tにキャストしています．
先ほどまでで準備したTypeとAnyがうまく使われています．

module Show : sig
  val apply : ('a -> string) Type.t -> 'a -> string
  val register : ('a -> string) Type.t -> ('a -> string) -> unit
end = struct
  let table : (string * Any.t) list = Ref.make []
  let apply t =
    match List2.assoc String.equal (Type.name t) (Ref.get table) with
    | Some(_, v) -> Any.get t v
    | None -> error `ooops`
  let register t f =
    table |> Ref.set (List2.acons (Type.name t) (Any.make t f) (Ref.get table))
end

正式なShowモジュール

先ほどのShowモジュールはShow.applyに渡す型(を表す値)が冒頭と違っていました．
これを解決するには'a Type.tを受け取って('a -> string) Type.tに変換する方法があればよさそうです．
ここで大事なのが，Type.tの実装です．
Type.tはその値ごとに違う埋め込みを表すので同じ'a Type.tに対して同じ('a -> string) Type.tを割り当てないといけません．
そこで，先ほどと同じようにして擬似的に'a Type.tから('a -> string) Type.tへのマップを作ります．
ということでそれを実装したのが以下になります．

module Show : sig
  val apply : 'a Type.t -> 'a -> string
  val register : 'a Type.t -> ('a -> string) -> unit
end = struct
  type 'a t = 'a -> string
  let tt : ('a t) Type.t = Type.make ` `
  let table2 : (string * Any.t) list = Ref.make []
  let get t =
    match List2.assoc String.equal (Type.name t) (Ref.get table2) with
    | Some(_, v) -> Any.get tt v
    | None -> error `oooops`
  let add t =
    table2 |> Ref.set (List2.acons (Type.name t) (Any.make tt (Type.make `fuga`)) (Ref.get table2))

  let table : (string * Any.t) list = Ref.make []
  let apply t =
    let t = get t in
    match List2.assoc String.equal (Type.name t) (Ref.get table) with
    | Some(_, v) -> Any.get t v
    | None -> error `ooops`
  let register t f =
    let _ = add t in
    let t = get t in
    table |> Ref.set (List2.acons (Type.name t) (Any.make t f) (Ref.get table))
end

すこしわかりにくいですがgetとaddは以下のような型です．

val get : 'a Type.t -> ('a t) Type.t
val add : 'a Type.t -> unit

実際に動かす

実際に動かすとこんな感じです．めでたしめでたし．

let int = Type.make `int`
let string = Type.make `string`
let _ = Show.register int String.of-int
let _ = Show.register string Fn.id
let _ = Debug.log (Show.apply int 42) % => `42`
let _ = Debug.log (Show.apply string `foo`) % => `foo`
in
finish

ここまでの話を応用するとあらゆる型に対してad hocに振る舞う等価性判定の述語Equalとかもつくれます．たとえば，SATySFiで言えばFloatの等価性やStringの等価性，Lengthの等価性を同じコードで記述できるようになります．
一方，こういったShowやEqualを大げさに「型クラス」と呼ぶことにすると，型クラスを定義するたびに毎回似たようなモジュールを書き続けることになります．こればっかりはSATySFiにfunctorがないのでどうしようもありません．
TIVによる型クラスのエミュレーションは実用できなくもないですが，本当のところをいえばSATySFiがネイティブにこのような機能をサポートしてくれることが望ましいです．
実際，ここでは書かなかった('a list) Type.tや('a -> 'b) Type.tのような高カインドの場合は上記のコードにくわえてやることがそれなりに増えてしまいます．
これからのSATySFiのさらなる発展に期待しましょう．